Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

ts.data61.csiro.au

Post reply on HN
Print view View original

31–40 of 99 posts

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

#31

Post by cmrx64 »

pjmlp wrote: post #28
jkot wrote: post #14

Earlier quoted context omitted.

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.

Not really true. See https://www.nicta.com.au/publications/research-publications/... for how the compiler and its internal semantics are completely removed from the chain for l4v.

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

#32

Post by cmrx64 »

ynniv wrote: post #23
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

The "real" specification (if it can be said to exist) is the abstract spec, in Isabelle/HOL.

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

#33

Post by eternalban »

cmrx64 wrote: post #30
eternalban wrote: post #12

Earlier quoted context omitted.

Are selL4 capabilities transferable?

Yes. See the manual or the tutorials.

Plese correct any/my minunderstanding here: doesn't that imply that flaws in the capability holder can obviate the "isolation boundary" guarantees? (For example, if app x has capability to address a certain memory block and then hands that off to another application.)

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

#34

Post by tptacek »

mtgx wrote: post #22
adrianN wrote: post #5

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

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?

This is almost tautological. Application vulnerabilities will always be the low-hanging fruit, because that's where the attack surface is. 20 years ago, an OS had juicy attack surface, because the bugs hadn't been shaken out of TCP/IP stacks and OS's shipped with stupid services enabled that nobody used. But it hasn't been 1998 for quite some time now.

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

#35

Post by tptacek »

nanolith wrote: post #24
tptacek wrote: post #15

Earlier quoted context omitted.

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…

Can you describe this with an example of a realistic use of L4-enabled sandboxing for a single-function IoT device?

(I've done some L4 work so you don't need to spend a lot of time explaining.)

General purpose OSs like iOS? No question: L4 is a major win. But that's not what the discussion here is really about.

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

#36

Post by tptacek »

pjmlp wrote: post #27
tptacek wrote: post #18

Earlier quoted context omitted.

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.

Right, but if the device exists more or less to run a single program or small set of programs, what do I care if I own the box once I've taken control of that program?

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

#37

Post by nickpsecurity »

A number of comments here cover how one would use something like this to benefit security of real-world systems. After all, it's a building block you have to combine with other things. This was demonstrated by team behind Nizza in the paper below with examples including digital signatures, VPN's, and so on.

https://os.inf.tu-dresden.de/papers_ps/nizza.pdf

The first to get certified to high assurance under recent models and delivered in products was INTEGRITY-178B. Like Nizza, they implemented desktops that virtualized the machine with Windows/Linux partitions side-by-side with native apps directly on separation kernel. Runtimes for Ada and Java subsets let you write critical components without common errors from C. Special middleware applies security policies to interactions between components.

http://www.ghs.com/products/safety_critical/integrity-do-178...

A recent product that's more accessible is the GenodeOS architecture that builds hierarchical, desktop system on top of components like seL4, NOVA, and Nitpicker GUI. They're dual-licensed with open-source available. Work in progress.

https://genode.org/

It should be noted that seL4 itself is aiming for embedded. Many of the top teams are also focusing on language and spec-level models for verification of holistic properties. The isolation approach isn't enough for the level of correctness they're aiming for. Anyone interested in such work should check out Galois's project or CertiKOS.

http://smaccmpilot.org/

http://flint.cs.yale.edu/certikos/mcertikos.html

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

#38

Post by nickpsecurity »

mafribe wrote: post #19
tptacek wrote: post #15

Earlier quoted context omitted.

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.

See my comment. It has top approaches to that which already delivered implementations.

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

#39

Post by cvwright »

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.

This is more true than many here may realize. If you're not familiar with how microkernels work, remember that everything is moved from kernel to user space if it's at all feasible to do so. In L4 and related systems, that usually means that the kernel doesn't even include the memory manager (the "pager"). So even page faults are handled by application code, which IIRC is not part of the current verification.

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

#40

Post by cmrx64 »

eternalban wrote: post #33
cmrx64 wrote: post #30

Earlier quoted context omitted.

Yes. See the manual or the tutorials.

Plese correct any/my minunderstanding here: doesn't that imply that flaws in the capability holder can obviate the "isolation boundary" guarantees? (For example, if app x has capability to address a certain memory block and then hands that off to another application.)

That's not what isolation is meant here: if there is a connection between applications that allows cap transfer, they aren't isolated at the cap level. See www.nicta.com.au/pub?doc=7371 for more details, page 35 ("Authority Confinement and Integrity"). If there is any shared memory or potential for shared memory via the vspace caps, there can still be info flows (see page 38, "Confidentiality: Information-flow security").

The theorems are somewhat technical, but your intuition is correct.

Post reply on HN