L4 microkernels: The lessons from 20 years of research and deployment
ts.data61.csiro.au
L4 microkernels: The lessons from 20 years of research and deployment
1–10 of 99 posts
Re: L4 microkernels: The lessons from 20 years of research and deployment
#2I'm having really big expectations on seL4. The modularity of a microkernel with the security of formal methods is something that would give hope of solving some really fundamental problems with the "IoT scene". I.e. having good security out of the box (which is horrible in IoT as of now), while still maintaining good flexibility regarding platforms (which will become more and more of a problem in the future when IoT devices start actually proliferating).
Edit: oh, and you can still run seL4 as hypervisor and run Linux on top of it to get the usual Embedded Linux stack where your CPU has enough juice. And still keep the critical systems safe behind seL4's capability system. Best of both worlds? Dunno, hopefully seL4 will be there someday in production quality.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#3I'm having really big expectations on seL4. The modularity of a microkernel with the security of formal methods is something that would give hope of solving some really fundamental problems with the "IoT scene". I.e. having good security out of the box (which is horrible in IoT as of now), while still maintaining good flexibility regarding platforms (which will become more and more of a problem in the future when IoT…
L4 is great, but it doesn't solve application security problems. L4 by itself doesn't do much, and whatever you build on top of it --- if you're not yourself using formal methods, which very few real product teams do --- isn't going to inherit its security.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#4I'm having really big expectations on seL4. The modularity of a microkernel with the security of formal methods is something that would give hope of solving some really fundamental problems with the "IoT scene". I.e. having good security out of the box (which is horrible in IoT as of now), while still maintaining good flexibility regarding platforms (which will become more and more of a problem in the future when IoT…
L4 is great, but it doesn't solve application security problems. L4 by itself doesn't do much, and whatever you build on top of it --- if you're not yourself using formal methods, which very few real product teams do --- isn't going to inherit its security.
Sure, it's not a panacea. But at least it gives a much better foundation than what we usually are having now.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#5Earlier quoted context omitted.
L4 is great, but it doesn't solve application security problems. L4 by itself doesn't do much, and whatever you build on top of it --- if you're not yourself using formal methods, which very few real product teams do --- isn't going to inherit its security.
Sure, it's not a panacea. But at least it gives a much better foundation than what we usually are having now.
How many of the exploits for IoT devices are related to the kernel? I have the impression that it's mostly poor protocols with default passwords and zero consideration for security that are the problem.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#6I'm having really big expectations on seL4. The modularity of a microkernel with the security of formal methods is something that would give hope of solving some really fundamental problems with the "IoT scene". I.e. having good security out of the box (which is horrible in IoT as of now), while still maintaining good flexibility regarding platforms (which will become more and more of a problem in the future when IoT…
L4 is great, but it doesn't solve application security problems. L4 by itself doesn't do much, and whatever you build on top of it --- if you're not yourself using formal methods, which very few real product teams do --- isn't going to inherit its security.
But it does give you a proven isolation boundary. We've been arguing for software sandboxes for ages, but their impact has been lessened since our OSs fall pretty readily to skilled adversaries. As a computing industry we've put our trust in VMs as another isolation boundary, but the regular advisories from Xen show that this isn't really as solid boundary as we would like.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#7Earlier quoted context omitted.
Sure, it's not a panacea. But at least it gives a much better foundation than what we usually are having now.
How many of the exploits for IoT devices are related to the kernel? I have the impression that it's mostly poor protocols with default passwords and zero consideration for security that are the problem.
The issue you raise is highly relevant — it's like having an IoT powerplug which is, indeed, UL-rated not to burst into flames and explode. That's great, but that doesn't mean that the software running on it won't send every packet on your home LAN to a router in Russia.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#8Earlier quoted context omitted.
Sure, it's not a panacea. But at least it gives a much better foundation than what we usually are having now.
How many of the exploits for IoT devices are related to the kernel? I have the impression that it's mostly poor protocols with default passwords and zero consideration for security that are the problem.
I won't pretend to having any kind of statistics on the matter.
But the whole point is that usually in embedded systems, there is no separation between "application" and "kernel", at least on the low-end of CPU power scale. To be able to isolate application level problems from kernel would already be a huge boon.
As a highly publicized anecdote, the Jeep hack of Miller and Valaseck was done by attacking through wireless, and replacing the CAN driver code to suit their needs. Not possible with proper isolation between critical system drivers and application layer.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#9I'm having really big expectations on seL4. The modularity of a microkernel with the security of formal methods is something that would give hope of solving some really fundamental problems with the "IoT scene". I.e. having good security out of the box (which is horrible in IoT as of now), while still maintaining good flexibility regarding platforms (which will become more and more of a problem in the future when IoT…
L4 is great, but it doesn't solve application security problems. L4 by itself doesn't do much, and whatever you build on top of it --- if you're not yourself using formal methods, which very few real product teams do --- isn't going to inherit its security.
True, seL4 verification doesn't solve the application level security problem but it makes it more approachable in several ways.
- No longer need the verification of application make assumptions about the semantics of the operating system. Instead, concrete and verified semantics are available. This makes application specification and verification easier, and safer. Fortunately, verification is cumulative
- The seL4 project has driven the state-of-the-art of verification tool forwards by a considerable degree.
- The seL4 project has lead the thinking about proof engineering [1], the emerging field that that is to verification what software engineering is to programming, addressing the question how to develop, maintain and evolve large-scale proofs.
- The existence of something like seL4 also puts pressure on CPU manufactures to provide usable formal specifications to their customers, so that we can verify against rigorous CPU specs. CPU manufacturers have been loath to do this (for various reasons).
The full verification of seL4 came a lot earlier (by about a decade) than I thought possible.
[1] G. Klein, Proof Engineering Considered Essential.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#10If the goal is to provide a verifiably correct kernel, why not build that kernel in something like OCAML so you can leverage a better type system and use the existing verification infrastructure in that language?