13 ms·

Note that the SEL4 kernel is only a small portion of this project. They've secured the entire stack, top to bottom. HACMS leverages a number of other projects

by achille 11y ago

Note that the SEL4 kernel is only a small portion of this project. They've secured the entire stack, top to bottom. HACMS leverages a number of other projects including the CompCert verifying C compiler, Verve OS Theorem prover, model checkers. You also need need proofs for the communication protocol, the IP stack, secured device drivers, memory protection units, control systems that can detect attacks, etc. Just a proven kernel won't keep the helicopter flying, you've got to secure everything. Additionally you need to reason about execution time and memory constraints. Slides: http://www.cyber.umd.edu/sites/default/files/documents/symposium/fisher-HACMS-MD.pdf http://www.cyber.umd.edu/sites/default/files/documents/sympo... Presentation from Kathleen Fisher, the researcher who's won the DARPA grant for the program: * https://www.youtube.com/watch?v=YqRdbgRPYw8 https://www.youtube.com/watch?v=YqRdbgRPYw8

petra 11y ago
Interesting lecture by DARPA. It also refers to their secure UAV project, which is as anexample to embedded system: http://ssrg.nicta.com.au/projects/TS/SMACCM/ http://ssrg.nicta.com.au/projects/TS/SMACCM/ They also released a formally proven real-time OS.
mtgx 11y ago
So can you create a general purpose OS with something like this, or is it only useful for embedded stuff, like say voting machines?
- tptacek 11y ago
  It is unlikely that anyone is going to create a general-purpose operating system based directly on an L4 kernel. L4 is incredibly simple. The more reasonable thing to do with L4 is to run another OS on top of it.
  - hga 11y ago
    I know of this effort: http://genode.org/ http://genode.org/ More specifically, I'd wonder about efforts to create not (necessarily) POSIX based stuff on top of seL4 etc.
    - pakled_engineer 11y ago
      The documentation for genode OS framework is a full free book (creative commons) http://genode.org/documentation/release-notes/15.05#Comprehensive_architectural_documentation http://genode.org/documentation/release-notes/15.05#Comprehe...
    - csirac2 11y ago
      NICTA/UNSW have apparently started working on a QubesOS port https://my.cse.unsw.edu.au/thesis/thesis_topic_details.php?ID=3289 https://my.cse.unsw.edu.au/thesis/thesis_topic_details.php?I... http://sel4.systems/pipermail/devel/2015-March/000312.html http://sel4.systems/pipermail/devel/2015-March/000312.html
      - throwaway7767 11y ago
        Huh, I'm surprised I'm seeing this first in a HN comment. I read qubes-devel with interest and have not noticed anything from these guys, but it sounds like a great project. I really hope it's something that turns into an actual maintained project instead of dying after the paper is out like so many security-focused research projects, but the lack of communication doesn't give me great hope.
        nickpsecurity 11y ago
        That's because Joanna is against it and will aggressively defend their platform choice. After our argument online [1], she posted this essay [2] comparing QubesOS to other things. She censored my piece-by-piece counter, too, lol. She did eventually do something with trusted path and mentioned QubesOS could be ported to different platforms. So, there's some progress... Honestly, it wasn't clear whether she really understood INFOSEC (esp TCB concept) based on her replies so I avoid QubesOS. [1] http://pastebin.com/5fnh8g2S http://pastebin.com/5fnh8g2S [2] http://theinvisiblethings.blogspot.com/2012/09/how-is-qubes-os-different-from.html http://theinvisiblethings.blogspot.com/2012/09/how-is-qubes-...
        hga 11y ago
monochromatic 11y ago
> Just a proven kernel won't keep the helicopter flying, you've got to secure everything. Including making sure that some moron doesn't keep his password on a post-it note on his monitor.

by achille 11y ago

petra 11y ago

Interesting lecture by DARPA. It also refers to their secure UAV project, which is as anexample to embedded system: http://ssrg.nicta.com.au/projects/TS/SMACCM/ http://ssrg.nicta.com.au/projects/TS/SMACCM/ They also released a formally proven real-time OS.

mtgx 11y ago

So can you create a general purpose OS with something like this, or is it only useful for embedded stuff, like say voting machines?

tptacek 11y ago
It is unlikely that anyone is going to create a general-purpose operating system based directly on an L4 kernel. L4 is incredibly simple. The more reasonable thing to do with L4 is to run another OS on top of it.
- hga 11y ago
  I know of this effort: http://genode.org/ http://genode.org/ More specifically, I'd wonder about efforts to create not (necessarily) POSIX based stuff on top of seL4 etc.
  - pakled_engineer 11y ago
    The documentation for genode OS framework is a full free book (creative commons) http://genode.org/documentation/release-notes/15.05#Comprehensive_architectural_documentation http://genode.org/documentation/release-notes/15.05#Comprehe...
  - csirac2 11y ago
    NICTA/UNSW have apparently started working on a QubesOS port https://my.cse.unsw.edu.au/thesis/thesis_topic_details.php?ID=3289 https://my.cse.unsw.edu.au/thesis/thesis_topic_details.php?I... http://sel4.systems/pipermail/devel/2015-March/000312.html http://sel4.systems/pipermail/devel/2015-March/000312.html
    - throwaway7767 11y ago
      Huh, I'm surprised I'm seeing this first in a HN comment. I read qubes-devel with interest and have not noticed anything from these guys, but it sounds like a great project. I really hope it's something that turns into an actual maintained project instead of dying after the paper is out like so many security-focused research projects, but the lack of communication doesn't give me great hope.
      - nickpsecurity 11y ago
        That's because Joanna is against it and will aggressively defend their platform choice. After our argument online [1], she posted this essay [2] comparing QubesOS to other things. She censored my piece-by-piece counter, too, lol. She did eventually do something with trusted path and mentioned QubesOS could be ported to different platforms. So, there's some progress... Honestly, it wasn't clear whether she really understood INFOSEC (esp TCB concept) based on her replies so I avoid QubesOS. [1] http://pastebin.com/5fnh8g2S http://pastebin.com/5fnh8g2S [2] http://theinvisiblethings.blogspot.com/2012/09/how-is-qubes-os-different-from.html http://theinvisiblethings.blogspot.com/2012/09/how-is-qubes-...
        hga 11y ago

monochromatic 11y ago

> Just a proven kernel won't keep the helicopter flying, you've got to secure everything. Including making sure that some moron doesn't keep his password on a post-it note on his monitor.