|
|
|
|
|
|
by jesse_m
2289 days ago
|
|
|
I think one of the big things here is that the refinement proofs from the models for isolation, IPC fast path, capability access control, and scheduling to C source to binary are strongest when the kernel is built with a particular configuration on particular hardware. When all of these are satisfied and you are on a trusted platform, you have very very strong guarantees that what is modeled is what you get. But it's not like this is hidden. They have make it pretty clear what the verified platforms and configurations are[1]. You should take a look at the verification chain though[1]. It is fairly extensive. It's not like they proved just a small part of a system in a general way. 1: https://docs.sel4.systems/Hardware/ 2: https://github.com/seL4/l4v |
|
|