4 ms·
> Darn. I wanted to have a play with it. Just in case - perhaps you will also enjoy playing with the non-verified L4? http://l4ka.org/ http://l4ka.org/ http:
by jsrn 17y ago
> Darn. I wanted to have a play with it.
Just in case - perhaps you will also enjoy playing with the non-verified L4?
http://l4ka.org/ http://l4ka.org/
http://l4ka.org/download/ http://l4ka.org/download/
- skorgu 17y agoI'm sure this is unanswerable for (perfectly valid) IP reasons but I wonder what the differences between L4 and seL4 are? Is there a functionality difference in either direction?
- gdp 17y agoMy assumption would be that the main difference is the formal proof, and whatever changes were necessary in order to permit formal verification (i.e. they may have changed behaviour in order to make the implementation actually meet the abstract specification). But I agree it would be very interesting to find out what the differences are, and whether substantial changes were required in order to do this kind of formal verification.
- wmf 17y agoseL4 and L4Sec are capability-based and thus quite different from regular L4. I always found capability systems much easier to understand than L4's message registers and flexpages.