[deleted]
L4 microkernels: The lessons from 20 years of research and deployment
11–20 of 99 posts
Re: L4 microkernels: The lessons from 20 years of research and deployment
#12Earlier 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.
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.
Are selL4 capabilities transferable?
Re: L4 microkernels: The lessons from 20 years of research and deployment
#13Where can I get the source for these to look at them? I'd like to know why they are all so long.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#14If 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?
I think you would also have to verify resulting binary, compiler, libraries...
It seems more manageable to verify a few KB of assembly or C
Re: L4 microkernels: The lessons from 20 years of research and deployment
#15Earlier 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.
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 p…
What's your sense of the number of IoT vulnerabilities that are due to misconstrued OS semantics? Mine --- and I've done a bit of work here, but not that much --- is that there aren't that many.
Really I think it depends on what you're doing. If the work you're doing is fundamentally kernel work --- if it's all about interacting with the security boundaries of the hardware (not just "interacting with hardware", like getting the bits from an RF codec, but manipulating hardware shared by attackers, like the iPhone SEP) then L4 is a pretty huge security win.
Otherwise: the problem you have isn't your OS, but the programming language you're using to build with.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#16Earlier 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.
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.
First, it depends on how you use it. L4 is pretty close to a "libOS". You can built sandboxes on it, or you can build something more like a monolithic OS on it.
Second, in IoT devices, sandboxing is a lot less interesting, because there aren't that many use cases for sandboxed sensor inputs (you're not RFing or button-pushing whole PDF documents).
I like L4! A lot! But I would be very wary of an IoT device claiming to have inherited security from it.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#17Where can I get the source for these to look at them? I'd like to know why they are all so long.
Here's the famous verified one: https://github.com/seL4/seL4
Re: L4 microkernels: The lessons from 20 years of research and deployment
#18Earlier quoted context omitted.
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 wirel…
What does separation between kernel and application really matter for single-function devices, like most IoT things are?
Re: L4 microkernels: The lessons from 20 years of research and deployment
#19Earlier quoted context omitted.
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 p…
What's your sense of the number of IoT vulnerabilities that are due to misconstrued OS semantics? Mine --- and I've done a bit of work here, but not that much --- is that there aren't that many. Really I think it depends on what you're doing. If the work you're doing is fundamentally kernel work --- if it's all about interacting with the security boundaries of the hardware (not just "interacting with hardware", like…
I'm happy to believe that almost all IoT vulnerabilities are application level problems.
The beginning availability of verified kernels and compilers makes it much more worthwhile to invest in formal approaches for application level vulnerabilities.
Re: L4 microkernels: The lessons from 20 years of research and deployment
#20Earlier quoted context omitted.
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 p…
What's your sense of the number of IoT vulnerabilities that are due to misconstrued OS semantics? Mine --- and I've done a bit of work here, but not that much --- is that there aren't that many. Really I think it depends on what you're doing. If the work you're doing is fundamentally kernel work --- if it's all about interacting with the security boundaries of the hardware (not just "interacting with hardware", like…
'Not that many' is not really acceptable for many applications, and I'm not talking only about IoT, but self-driving cars, surgery robots, rockets, etc.