The Breakthrough

There are a few properties that make seL4 perfect for robots and drones: it can only do what it’s designed to do, its code can’t be changed, and its memory and data transfers can’t be read without permission, according to New Scientist.  But the real key is that you can check the code mathematically — a hash can tell you that your kernel is still securte.

The Implications

If seL4 is a big jump in low-level computer security, we could see it employed widely in militaries, in important infrastructure like the power grid and even in our cars. Still — security is all about “trust but verify” — we need to verify that this kernel is actually secure, even if it says it can verify itself.


Share This Article