5 ms·
> The evolution of seL4 is continuing within NICTA, and it is the basis of ongoing research activities here at NICTA. However, it is also the subject of commerc
by gdp 17y ago
> The evolution of seL4 is continuing within NICTA, and it is the basis of ongoing research activities here at NICTA. However, it is also the subject of commercialisation activities, and thus is currently proprietary
Darn. I wanted to have a play with it.
That is a really cool achievement. Bring on bigger formally-verified projects!
- 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.
- skorgu 17y agoI'd love to see a non-commercial hobbyist license, either source or binary; that should let them commercialize it and let us play.