L4 microkernels: The lessons from 20 years of research and deployment • Hacker News Board

Re: L4 microkernels: The lessons from 20 years of research and deployment

#21

Post by DashRattlesnake » Tue, Sep 20, 2016, 3:29 PM UTC

mafribe wrote: post #9

tptacek wrote: post #3

Earlier 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…

> The full verification of seL4 came a lot earlier (by about a decade) than I thought possible.

Is it a full verification yet? I am by no means an expert, but IIRC, they were still using a simplified model MMU in their proofs.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#22

Post by mtgx » Tue, Sep 20, 2016, 3:32 PM UTC

adrianN wrote: post #5

shandor wrote: post #4

Earlier 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.

Only because that's still the low hanging fruit. Why would most hackers bother with kernel exploits, when hundreds of thousands of routers use their manufacturer's default password?

Re: L4 microkernels: The lessons from 20 years of research and deployment

#23

Post by ynniv » Tue, Sep 20, 2016, 3:52 PM UTC

TheMagicHorsey wrote: post #10

If 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?

sel4 was specified in Haskell and then converted to C

Re: L4 microkernels: The lessons from 20 years of research and deployment

#24

Post by nanolith » Tue, Sep 20, 2016, 3:56 PM UTC

tptacek wrote: post #15

mafribe wrote: post #9

Earlier 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…

If done well, formal verification of kernel level services and how these use runtime protection built in hardware can absolutely reduce the attack surface of application level code. The key is to move critical services that attackers would wish to exploit into a formally verified sandbox. That is the real power of systems like seL4, even though seL4 isn't itself really geared toward the sort of chipsets commonly used in consumer grade IoT products. However, a system _like_ seL4 can absolutely improve application level security, as long as the application is constrained by the architecture of the OS.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#25

Post by oconnore » Tue, Sep 20, 2016, 3:57 PM UTC

tptacek wrote: post #3

shandor wrote: post #2

I'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 capabilities do solve real application security problems, and this capability system is proven correct. You can get the same thing on Linux [1], but there is no guarantee that it can't be circumvented or broken.

[1]: http://www.cl.cam.ac.uk/research/security/capsicum/

Re: L4 microkernels: The lessons from 20 years of research and deployment

#26

Post by XparXnoiAx » Tue, Sep 20, 2016, 3:59 PM UTC

shandor wrote: post #2

I'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…

At DefCon, someone did a talk investigating the wireless security of some drones. Some of them had a TELNET port open for anyone to log in. The problem here isn't a lack of formal verification, it's a lack of people caring.

There is only one thing that will fix the problem, and that is when corporations get hit in the wallet for having security flaws, see for example: https://medium.com/@xParXnoiAx/irresponsible-disclosure-52d0...

Re: L4 microkernels: The lessons from 20 years of research and deployment

#27

Post by pjmlp » Tue, Sep 20, 2016, 4:07 PM UTC

tptacek wrote: post #18

shandor wrote: post #8

Earlier quoted context omitted.

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?

If written in languages like C and C++, you just get the own the complete device when exploiting application errors.

It can also happen when using unsafe code with the Ada, Java, Pascal and Basic variants available for such devices, but the probability is lower.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#28

Post by pjmlp » Tue, Sep 20, 2016, 4:09 PM UTC

jkot wrote: post #14

TheMagicHorsey wrote: post #10

If 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

Not really, to verify C code you need to set the compiler and its corresponding version in stone for the verification process, as UB can change even between versions of the same compiler.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#29

Post by cmrx64 » Tue, Sep 20, 2016, 4:10 PM UTC

DashRattlesnake wrote: post #21

mafribe wrote: post #9

Earlier 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…

> The full verification of seL4 came a lot earlier (by about a decade) than I thought possible. Is it a full verification yet? I am by no means an expert, but IIRC, they were still using a simplified model MMU in their proofs.

It's a simplified model, but it's well validated. Without connecting the proofs to a formally verified chip, it's about the best you can do.

Re: L4 microkernels: The lessons from 20 years of research and deployment

#30

Post by cmrx64 » Tue, Sep 20, 2016, 4:10 PM UTC

eternalban wrote: post #12

Eridrus wrote: post #6

Earlier quoted context omitted.

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?

Yes. See the manual or the tutorials.