|
|
|
|
|
|
by el_pollo_diablo
453 days ago
|
|
|
> seL4 is the only microkernel that has a proof of correctness ProvenCore (https://provenrun.com/provencore/) has a proof that covers correctness (memory safety, and more generally absence of UB, termination, etc.), functional properties (e.g. the fork() system call is a refinement of an abstract "clone" operation of abstract machines), and security properties (memory isolation). |
|
|