5 ms·
What's the difference with this https://sel4.systems/ https://sel4.systems/?
by vander_elst 10y ago
What's the difference with this https://sel4.systems/ https://sel4.systems/?
- no_protocol 10y agoI searched the conference paper for "sel4" and this result seems relevant to your question: A comparison of the performance of seL4 and mC2 is not straightforward since the verified mC2 kernel runs on a multicore x86 platform, while the verified seL4 kernel runs on ARMv6 and ARMv7 hardware and only supports single-core
- indolering 10y agoMulticore is on the seL4 roadmap[0], albeit the proof is listed as TBD. 0: http://sel4.systems/Info/Roadmap/ http://sel4.systems/Info/Roadmap/
- nickpsecurity 10y agoThe main difference is the verification/design method. seL4 does the abstract machine in Haskell, model in HOL, and final code in C. Both Haskell and C are shown equivalent. It took a ton of work. They also have to use these two tools for expressing all kinds of solutions they're not ideal for. CertiKOS is using a DSL approach if it's same as paper I'm remembering. They design languages or proving techniques ideal to the type of thing they're working on: memory management, I/O, etc. They prove each individual component as easily as they can. Then they have some way of modeling the system as a whole and/or integrating those. Too early to judge but they seem more productive than L4 project was due to tooling benefits.
- indolering 10y agoAccording to one of the talks I watched, they are moving towards using more domain-specific languages.
- nickpsecurity 10y agoThat's ambiguous. Are you talking about seL4 or CertiKOS people?
- indolering 10y agoThe seL4 team, they have taken this approach with their drivers and ext2 implementation. Apparently it is part of a more general strategy [0]. [0] https://archive.fosdem.org/2015/schedule/event/sel4/ https://archive.fosdem.org/2015/schedule/event/sel4/
- nickpsecurity 10y agoOk. Good they're doubling down on it.