3 ms·
Correctness via formal verification - at least in the core of sel4.
by vilvo 2y ago
Correctness via formal verification - at least in the core of sel4.
- monocasa 2y agoGenode can also run on sel4.
- nickpsecurity 2y agoAre its TCB and integration similarly verified? If not formally-verified, are they in a safe language or statically analyzed to block common errors?
- monocasa 2y agoI mean, LionOS appears to (with the exception of sel4 itself) be mainly written in unverified C without heavy static analysis. So LionOS and Genode appear to be about equal in that regard.