8 ms·

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 som

by shandor 10y ago

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

tptacek 10y ago
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.
- shandor 10y ago
  Sure, it's not a panacea. But at least it gives a much better foundation than what we usually are having now.
  - adrianN 10y ago
    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.
    - zeveb 10y ago
      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.
    - shandor 10y ago
      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.
      - tptacek 10y ago
        What does separation between kernel and application really matter for single-function devices, like most IoT things are?
        pjmlp 10y ago
        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.
        tptacek 10y ago
        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?
        wepple 10y ago
        the jeep hack (IIRC) got code exec in userland remotely, but relied upon talking to drivers to be able to flash the CAN chip. Of course, the whole thing was broken anyhow as everything was running root. But in almost everything else, I agree. I don't care if you have ring-0 on my Nest camera, because I'm more worried about network-level attacks or an attacker being able to read from the camera which (I'm guessing) is available via user space.
    - mtgx 10y ago
      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?
      - tptacek 10y ago
        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.
  - cvwright 10y ago
    Comments in this thread also illustrate why it's hard (and frustrating) to do constructive work in security. It's a big, complicated problem, and nobody's happy unless you solve it all at once. You could do the equivalent of solving world hunger and world peace, but unless you also give everyone in the world a free puppy, you're going to get bad reviews complaining about the lack of puppies. And there's always someone who wanted a kitten instead...
    - tptacek 10y ago
      I hope I'm not in this instance coming across that way! I like L4!
- Eridrus 10y ago
  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.
  - eternalban 10y ago
    Are selL4 capabilities transferable?
    - cmrx64 10y ago
      Yes. See the manual or the tutorials.
      - eternalban 10y ago
        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.)
        cmrx64 10y ago
        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.
        eternalban 10y ago
        Thanks. Skimming that, I got that (a) PHigh -> PLow via overt channels will be degraded, and that (b) seL4 reduces the attack surface to "covert channels" only which seem to be confined to H/W "platform" concerns.
- mafribe 10y ago
  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.
  - tptacek 10y ago
    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.
    - mafribe 10y ago
      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.
      - 10y ago
- oconnore 10y ago
  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/ http://www.cl.cam.ac.uk/research/security/capsicum/
- cvwright 10y ago
  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.
  - cmrx64 10y ago
    Delivery of page faults is, handling of them isn't (although the kernel does abstract the exact mechanism, into message delivery).
- skew 10y ago
  Do you mean "seL4 is great"? I agree it won't do much for application-level security without adding some formally verified code on top (perhaps as simple as setting up isolation between VMs), but it looks great if you do want to use formal methods. For the simplest thing, just starting out with a formal semantics of the OS and reason to trust that semantics would save a lot of work (of course, a lot may remain).
  - tptacek 10y ago
    Honestly, I don't much care about the formal verification of L4; it's the L4 design and implementation strategy that I find compelling.
- hughw 10y ago
  Where does one go to learn these formal methods?
  - elihu 10y ago
    I'm not very knowledgeable in this area and haven't used these tools myself, but you could start by looking into theorem-proving tools like coq and agda.
  - cmrx64 10y ago
    Depends on what level of detail you're interested in. You could check out ADA/Spark or Dafny. Or, investigate something like Isabelle/HOL or Coq - perhaps via http://concrete-semantics.org/ http://concrete-semantics.org/ or http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/.
- berkeleynerd 10y ago
  Is Mirage on L4 something that, if realized, would provide application developers with a more secure basis for building their own applications? I'm but a simple application developer but I do care about security and if there were a platform I could develop against that gave me confidence my code was far less likely to be undermined by kernel or TCP stack vulnerabilities I think I'd be encouraged to do a better job of security myself. This might not be the ideal human attitude toward secure programming but I might not be alone in feeling like my best efforts rest on shaky foundations and that's somewhat demoralizing.
- Jweb_Guru 10y ago
  For me, SeL4's verification is important because it can actually provide formal real-time guarantees. Before SeL4, if you wanted to write a hard real-time system, you pretty much had to either forego an OS, or forego formal verification (or, usually, both). Having the option to write a RTOS without also writing a bunch of boilerplate (and probably incorrect) scheduler / resource allocation code, or dedicating a core to a task because you couldn't reason about resource consumption otherwise, is pretty exciting! Sure, it may not help much with securing normal userland applications, but in many embedded systems meeting deadlines is more important than any security functionality could be; the confinement properties are in some sense just consequences of having to reliably hit deadlines and isolate resources.
XparXnoiAx 10y ago
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-52d08cddcd07 https://medium.com/@xParXnoiAx/irresponsible-disclosure-52d0...
- nickpsecurity 10y ago
  Yeah, the feeds are sent unencrypted, command centers keep getting infected due to running Windows instead of least-privilege architecture, probably written in unsafe languages, not using parser/protocol toolkits that reduce 0-days there, and I'm sure more I'll find out soon. Yeah, the companies' financial incentive is to ignore the stuff since they'll get the contracts anyway. They're just paying for capabilities rather than capabilities with expected quality level. I'd understand if the autopilot's AI or whatever wasn't perfect due to the complexity of the job or the graphics stack occasionally had artifacts in it. The systems not having basic security measure that budget startups pull off indicates it's not that such a baseline was too difficult: they just don't give a shit.
  - XparXnoiAx 10y ago
    To the point that sometimes, it seems they go out of their way to make things insecure...........
  - angry_octet 10y ago
    If you read about the OPM hack you get an idea of the absolute ineptness and decision paralysis at work in these large organisations, and you begin to understand why you can connect to the drone with telnet and why the command centre relies on 13 year old Share Point and Active X. OPM https://news.ycombinator.com/item?id=12457786 https://news.ycombinator.com/item?id=12457786

by shandor 10y ago

tptacek 10y ago

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.

shandor 10y ago
Sure, it's not a panacea. But at least it gives a much better foundation than what we usually are having now.
- adrianN 10y ago
  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.
  - zeveb 10y ago
    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.
  - shandor 10y ago
    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.
    - tptacek 10y ago
      What does separation between kernel and application really matter for single-function devices, like most IoT things are?
      - pjmlp 10y ago
        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.
        tptacek 10y ago
        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?
        wepple 10y ago
        the jeep hack (IIRC) got code exec in userland remotely, but relied upon talking to drivers to be able to flash the CAN chip. Of course, the whole thing was broken anyhow as everything was running root. But in almost everything else, I agree. I don't care if you have ring-0 on my Nest camera, because I'm more worried about network-level attacks or an attacker being able to read from the camera which (I'm guessing) is available via user space.
  - mtgx 10y ago
    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?
    - tptacek 10y ago
      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.
- cvwright 10y ago
  Comments in this thread also illustrate why it's hard (and frustrating) to do constructive work in security. It's a big, complicated problem, and nobody's happy unless you solve it all at once. You could do the equivalent of solving world hunger and world peace, but unless you also give everyone in the world a free puppy, you're going to get bad reviews complaining about the lack of puppies. And there's always someone who wanted a kitten instead...
  - tptacek 10y ago
    I hope I'm not in this instance coming across that way! I like L4!
Eridrus 10y ago
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.
- eternalban 10y ago
  Are selL4 capabilities transferable?
  - cmrx64 10y ago
    Yes. See the manual or the tutorials.
    - eternalban 10y ago
      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.)
      - cmrx64 10y ago
        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.
        eternalban 10y ago
        Thanks. Skimming that, I got that (a) PHigh -> PLow via overt channels will be degraded, and that (b) seL4 reduces the attack surface to "covert channels" only which seem to be confined to H/W "platform" concerns.
mafribe 10y ago
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.
- tptacek 10y ago
  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.
  - mafribe 10y ago
    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.
    - 10y ago
oconnore 10y ago
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/ http://www.cl.cam.ac.uk/research/security/capsicum/
cvwright 10y ago
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.
- cmrx64 10y ago
  Delivery of page faults is, handling of them isn't (although the kernel does abstract the exact mechanism, into message delivery).
skew 10y ago
Do you mean "seL4 is great"? I agree it won't do much for application-level security without adding some formally verified code on top (perhaps as simple as setting up isolation between VMs), but it looks great if you do want to use formal methods. For the simplest thing, just starting out with a formal semantics of the OS and reason to trust that semantics would save a lot of work (of course, a lot may remain).
- tptacek 10y ago
  Honestly, I don't much care about the formal verification of L4; it's the L4 design and implementation strategy that I find compelling.
hughw 10y ago
Where does one go to learn these formal methods?
- elihu 10y ago
  I'm not very knowledgeable in this area and haven't used these tools myself, but you could start by looking into theorem-proving tools like coq and agda.
- cmrx64 10y ago
  Depends on what level of detail you're interested in. You could check out ADA/Spark or Dafny. Or, investigate something like Isabelle/HOL or Coq - perhaps via http://concrete-semantics.org/ http://concrete-semantics.org/ or http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/.
berkeleynerd 10y ago
Is Mirage on L4 something that, if realized, would provide application developers with a more secure basis for building their own applications? I'm but a simple application developer but I do care about security and if there were a platform I could develop against that gave me confidence my code was far less likely to be undermined by kernel or TCP stack vulnerabilities I think I'd be encouraged to do a better job of security myself. This might not be the ideal human attitude toward secure programming but I might not be alone in feeling like my best efforts rest on shaky foundations and that's somewhat demoralizing.
Jweb_Guru 10y ago
For me, SeL4's verification is important because it can actually provide formal real-time guarantees. Before SeL4, if you wanted to write a hard real-time system, you pretty much had to either forego an OS, or forego formal verification (or, usually, both). Having the option to write a RTOS without also writing a bunch of boilerplate (and probably incorrect) scheduler / resource allocation code, or dedicating a core to a task because you couldn't reason about resource consumption otherwise, is pretty exciting! Sure, it may not help much with securing normal userland applications, but in many embedded systems meeting deadlines is more important than any security functionality could be; the confinement properties are in some sense just consequences of having to reliably hit deadlines and isolate resources.

XparXnoiAx 10y ago

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-52d08cddcd07 https://medium.com/@xParXnoiAx/irresponsible-disclosure-52d0...

nickpsecurity 10y ago
Yeah, the feeds are sent unencrypted, command centers keep getting infected due to running Windows instead of least-privilege architecture, probably written in unsafe languages, not using parser/protocol toolkits that reduce 0-days there, and I'm sure more I'll find out soon. Yeah, the companies' financial incentive is to ignore the stuff since they'll get the contracts anyway. They're just paying for capabilities rather than capabilities with expected quality level. I'd understand if the autopilot's AI or whatever wasn't perfect due to the complexity of the job or the graphics stack occasionally had artifacts in it. The systems not having basic security measure that budget startups pull off indicates it's not that such a baseline was too difficult: they just don't give a shit.
- XparXnoiAx 10y ago
  To the point that sometimes, it seems they go out of their way to make things insecure...........
- angry_octet 10y ago
  If you read about the OPM hack you get an idea of the absolute ineptness and decision paralysis at work in these large organisations, and you begin to understand why you can connect to the drone with telnet and why the command centre relies on 13 year old Share Point and Active X. OPM https://news.ycombinator.com/item?id=12457786 https://news.ycombinator.com/item?id=12457786