Re: [Xen-devel] [qubes-devel] Re: Critique of the Xen Security Process

[Radoslaw Szkodzinski <astralstorm@xxxxxxxxx>]

As usual. Security, performance, convenience, price. Pick any mixture.

As is usual for most software, developer convenience trumps most other
considerations. I include ease of generating nice papers and jobs
under developer convenience.
Big players are much more concerned about performance, which saves
money on machines you need to buy. (Note the resources poured into
tmem, which is very iffy from security standpoint.)
Even if there was a sudden security drive for Xen, it's a huge and
probably fruitless task. Xen is not designed top down so you get no
nice overview to check main assumptions. This is also why Xen is
written in C and assembly, not in anything easier to use.

Likewise security-oriented microkernels such as seL4 push drivers to
"userspace" making it convenient for their developers, at the cost of
performance and security, since they are now Somebody Else's Problem.
Surprisingly, seL4 seems to be the only active and working
non-research project that happens to have security as main aim, and
they don't even implement many of features that are "required" for
modern secure design, say, IOMMU...
They want you to write your drivers as automated proofs instead.
Meaning cheap developers will not be able to even lift a finger in
writing those, since you need to learn Isabelle DSL and understand
what is required in order to write a working driver with a good API,
then also understand and model features of underlying hardware. This
requires good mathematical background, as in actual CS, not just
writing code.

What seL4 folks are actually doing (have done, even) is writing a
potent compiler between both C and theorem proving language, plus a
set of theorems describing assumptions made on underlying hardware and
security features. Very simple, just some 250k lines of theorems to
prove correctness of 7k lines of C code.

Good luck trying to port Qubes to their architecture. It's not
impossible, but it is quite a task. So many theorems to wade through
and understand, not to mention a whole new programming language.
You'd get to add well defined isolation primitives to their theorem
prover, then write a parallel proof to capDL kernel (ouch) or extend
capDL with such isolation features and requisite APIs.
Again, developer convenience suffers and have too high barrier of
entry, and you won't get any code written or it will get too expensive
in terms of time, skill and therefore money.

As to other attempts...
Python code? Forget about it, Python is thoroughly undefined behavior
with no truly defined memory model. :) Even C++11 is better there.

Rust? Rust mechanisms are undefined in terms of timing, which will
result in unbounded execution time (hangs) when actual hardware is
involved - there is no way to describe timing behavior of hardware in
it in such a way that these properties are verified at higher layers.
They attempt concurrency but the primitives are not bound to actual
real time and hardware. There is no library for bare metal
programming. Memory allocations are assumed to never fail - and many
other things as well. (Does this sound like some other "never fails"
software we're depending upon?)

Trying to write a secure kernel in an unsafe language is akin to
trying to bail a sinking ship with a spoon. It can theoretically be
done, just not in practice. And actual low-level and safe languages
are surprisingly rare.

Best regards,
R.

_______________________________________________
Xen-devel mailing list
Xen-devel@xxxxxxxxxxxxx
http://lists.xen.org/xen-devel