This is true but I can see her point of view as someone with a product that is based on the open source core. There have been a lot of very drastic changes that would cause someone with a product to have to do a significant amount of re-engineering. Also how many different toolstacks have their been?
I also see both sides but Joanna definitely has some very good points chris On Mon, Nov 9, 2015 at 9:46 PM, Radoslaw Szkodzinski <astralst...@gmail.com> wrote: > 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@lists.xen.org > http://lists.xen.org/xen-devel >
_______________________________________________ Xen-devel mailing list Xen-devel@lists.xen.org http://lists.xen.org/xen-devel
