seL4 is the world's first (and only?) operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. In 34 days it is going open source:
Now if only we could get a provably-correct implementation of the Amoeba operating system kernel on top of this, it'd be the perfect base for a boxed AI software stack.
Keep in mind, these things are only proven to work as specified. There is no guarantee that the specification itself is secure. Or that there is no side channel attack possible. Or other stuff.
Correct. But what it achieves is a massive compression in the size of the attack surface. In as much as you trust the proof system, you know that the code matches the specification, so the only bugs which can exist are those in the specification itself.
seL4 is the world's first (and only?) operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. In 34 days it is going open source:
http://sel4.systems/
Now if only we could get a provably-correct implementation of the Amoeba operating system kernel on top of this, it'd be the perfect base for a boxed AI software stack.