When did you start talking to formal verification researchers?
Because, you know, I totally have not wanted to do a PhD under any of these guys, or anything like that...
When did you start talking to formal verification researchers?
Many months ago. Subscribe to the MIRI blog! :)
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.