7 ms·

The seL4 microkernel

194 points by gioele 12y ago

tdicola 12y ago
From the supported platforms it looks like it should work on a BeagleBone Black (arm, am335x, armv7-a, cortex-a8)--anyone been brave enough to try?
- sneak 12y ago
  AFAIK the beaglebones load their entire executable environment, including bootloader, from removable flash media - there shouldn't be any bravery required to test out experimental software (even bootloaders and firmware) because you can always just swap out the entire card. There's no bricking them.
  - yuvadam 12y ago
    Yep, they can either load from removable flash (microSD) or from onboard eMMC flash storage, selectable by switch on boot.
- hornetblack 12y ago
  Students at UNSW doing Advanced Operating systems use a SabreLite board running seL4. They're pretty similar so you should be able to get it working.
gioele 12y ago
Please note that the formally proven model has been implemented also in Haskell, not only in C. Formally-proven-correct code + Haskell + literate programming = https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Kernel/Thread.lhs https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Ke...
Intermernet 12y ago
seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement" originally developed (as far as I know) at UNSW, further developed at NICTA. The original project home page is at http://ssrg.nicta.com.au/projects/seL4/ http://ssrg.nicta.com.au/projects/seL4/ and the new page is at http://sel4.systems/ http://sel4.systems/ Downloads at http://ssrg.nicta.com.au/software/TS/seL4/ http://ssrg.nicta.com.au/software/TS/seL4/
- easytiger 12y ago
  Thanks, the given link couldn't have contained less information if it tried
  - axman6 12y ago
    The FAQ[1] has a hell of a lot of info about what seL4 does and does not do. [1] http://sel4.systems/FAQ http://sel4.systems/FAQ
    - easytiger 12y ago
      Which is not referenced from the linked article. What is the point of posting something with all but no information?
      - yen223 12y ago
        They should have submitted http://sel4.systems/ http://sel4.systems/ as the link, instead of the github link.
        daveasdf 12y ago
        I'm not sure who submitted the link (I don't think it was anyone from the seL4 team), but I inserted the http://sel4.systems/ http://sel4.systems/ link into the repo's README file, which will hopefully help a little.
      - axman6 12y ago
        Oh, I didn't realise the linked article wasn't the actual seL4 website.
- FullyFunctional 12y ago
  This is excellent. While I'm still unsure about the seL4 model being the best for a secure system (a topic for another day), it's wonderful to see this development. I hope "someone" will port this to RISC-V (32- or 64-bit). Is http://ssrg.nicta.com.au/software/TS/seL4 http://ssrg.nicta.com.au/software/TS/seL4 out of date or is the license really not open source (OPEN KERNEL LABS and National ICT Australia Limited (Licensors) NON-COMMERCIAL LICENSE AGREEMENT)?
tambourine_man 12y ago
There was a project way back when to port Darwin to L4: http://www.ertos.nicta.com/software/darbat/ http://www.ertos.nicta.com/software/darbat/ along with the accompanying rumor that Apple would be “lifting” Mach's layer in XNU to run on top of L4. That was before the iPhone, of course. I was always fascinated by the talks of L4 being specifically designed to avoid scrubbing your L1/L2 cache on operations such as IPC.
pserwylo 12y ago
It's great to see more and more stuff come out of NICTA. For those who are unaware, it is a government funded research institution in Australia. A big difference from other research institutions is that they are especially focussed on commercially viable research (rather than purely theoretical stiff - although I'm sure they do some work on that too). It is a model that has been used for quite some time on Aus, with the CSIRO doing the same thing for more general (I.e. not specifically ICT) research. The CSIRO has done some beautifull research which forms the backbones of technology such as WiFi. So, putting aside recent budgetry and financial issues, it is great to see stuff like this being released by them. Here's to many more years of fruitful research.
userbinator 12y ago
An OS that is proved to be essentially perfectly secure? For some reason this brings up thoughts of trusted computing, and not in a good way...
- pflanze 12y ago
  You seem to be misunderstanding the kind of security this is about. It's not about taking away control by the owner, just about preventing ways of control by third parties that you as owner didn't intend to give. From https://en.wikipedia.org/wiki/Trusted_computing https://en.wikipedia.org/wiki/Trusted_computing: > TC is controversial as the hardware is not only secured for its owner, but also secured against its owner. Whereas here if you're not happy with what the OS does, you can wipe it and still have full control over the hardware. And the OS is OpenSource, accessible to the hardware owner to modify if some kind of control it asserts isn't satisfying.
  - gsnedders 12y ago
    Not the parent commenter, but: A proven kernel could be seen as taking control away on devices where root access cannot be legitimately obtained. I guess some might perceive it as scary given many people in tech circles root their phones (and similar devices), when root access is normally obtained through OS-level security bugs, and it is often (though I think somewhat decreasingly?) used to install third-party OSes on such devices.
    - pflanze 12y ago
      Agreed, although the blame then still lies with the device the secure kernel is running on, or the company that produces it, or the client for choosing to buy it. I guess you can say that proven software is power, and power can be misused.
bjourne 12y ago
I don't suppose anyone has, or know where to find, a generated pdf of the extensive Latex documentation? My own pdflatex skills are failing me. :/
- vlad003 12y ago
  Conveniently enough, I just generated myself a pdf of it: http://avacariu.me/files/seL4-manual.pdf http://avacariu.me/files/seL4-manual.pdf
  - bjourne 12y ago
    Thanks
DCKing 12y ago
Is there any recent benchmark of an L4 implementation with servers compared to a modern monolithic Linux or *BSD kernel? I'm still thinking there's huge untapped potential in microkernels and I wonder how the "state of the art" stacks up against modern monolithic kernels on processors with a lot of cache.
haberman 12y ago
This link to the GitHub repository doesn't give a lot of the context about why this is exciting. As others have mentioned, seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement." But for many years it was proprietary, and only available under commercial terms. The paper was published in 2009, so it's been five years that it was proprietary. As of today at noon, the kernel was released under GPLv2 and userland under two-clause BSD. That is exciting.
- phkahler 12y ago
  "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement." And as soon as one person makes a commit, that proof is invalid right?
  - klibertp 12y ago
    Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong? Anyway, I'm going to read more about what and how they did, it's fascinating to see a non-trivial software system proven correct.
    - sanxiyn 12y ago
      Yes, that's how they did it. Quoting from the paper: "Note that we have integrated all proofs into an automated proof checking suite, similar to an automated regression-test suite, but using machine-checked formal proofs instead of executable tests. This provides an automatic check, after each commit into the version control system, of the state of all the existing formal proofs, and identifies which specific portions of the proof must be re-established."
    - daveasdf 12y ago
      > Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong? Yes, that's the plan. Internally this is how we have been operating since 2009, when the proof was first completed: You don't push a change to the verified kernel branch unless you are willing (or are able to convince someone else) to do the proof updates. We don't yet have a regression website publicly available, but it's on the short-term roadmap.
awhitty 12y ago
Can someone explain to me what it means for a kernel to have an end-to-end proof of implementation? Does it just mean that the kernel is implemented bug-free? That it will never panic?
- klibertp 12y ago
  It won't. See here: http://sel4.systems/FAQ/#verif http://sel4.systems/FAQ/#verif It's actually a very impressive piece of work, I can't wait to read about the details of how it was done.
  - sanxiyn 12y ago
    Then go read http://www.nicta.com.au/pub?id=7371 http://www.nicta.com.au/pub?id=7371 :)

194 points by gioele 12y ago

From the supported platforms it looks like it should work on a BeagleBone Black (arm, am335x, armv7-a, cortex-a8)--anyone been brave enough to try?

sneak 12y ago
AFAIK the beaglebones load their entire executable environment, including bootloader, from removable flash media - there shouldn't be any bravery required to test out experimental software (even bootloaders and firmware) because you can always just swap out the entire card. There's no bricking them.
- yuvadam 12y ago
  Yep, they can either load from removable flash (microSD) or from onboard eMMC flash storage, selectable by switch on boot.
hornetblack 12y ago
Students at UNSW doing Advanced Operating systems use a SabreLite board running seL4. They're pretty similar so you should be able to get it working.

gioele 12y ago

Please note that the formally proven model has been implemented also in Haskell, not only in C. Formally-proven-correct code + Haskell + literate programming = https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Kernel/Thread.lhs https://github.com/seL4/seL4/blob/master/haskell/src/SEL4/Ke...

Intermernet 12y ago

seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement" originally developed (as far as I know) at UNSW, further developed at NICTA. The original project home page is at http://ssrg.nicta.com.au/projects/seL4/ http://ssrg.nicta.com.au/projects/seL4/ and the new page is at http://sel4.systems/ http://sel4.systems/ Downloads at http://ssrg.nicta.com.au/software/TS/seL4/ http://ssrg.nicta.com.au/software/TS/seL4/

easytiger 12y ago
Thanks, the given link couldn't have contained less information if it tried
- axman6 12y ago
  The FAQ[1] has a hell of a lot of info about what seL4 does and does not do. [1] http://sel4.systems/FAQ http://sel4.systems/FAQ
  - easytiger 12y ago
    Which is not referenced from the linked article. What is the point of posting something with all but no information?
    - yen223 12y ago
      They should have submitted http://sel4.systems/ http://sel4.systems/ as the link, instead of the github link.
      - daveasdf 12y ago
        I'm not sure who submitted the link (I don't think it was anyone from the seL4 team), but I inserted the http://sel4.systems/ http://sel4.systems/ link into the repo's README file, which will hopefully help a little.
    - axman6 12y ago
      Oh, I didn't realise the linked article wasn't the actual seL4 website.
FullyFunctional 12y ago
This is excellent. While I'm still unsure about the seL4 model being the best for a secure system (a topic for another day), it's wonderful to see this development. I hope "someone" will port this to RISC-V (32- or 64-bit). Is http://ssrg.nicta.com.au/software/TS/seL4 http://ssrg.nicta.com.au/software/TS/seL4 out of date or is the license really not open source (OPEN KERNEL LABS and National ICT Australia Limited (Licensors) NON-COMMERCIAL LICENSE AGREEMENT)?

tambourine_man 12y ago

There was a project way back when to port Darwin to L4: http://www.ertos.nicta.com/software/darbat/ http://www.ertos.nicta.com/software/darbat/ along with the accompanying rumor that Apple would be “lifting” Mach's layer in XNU to run on top of L4. That was before the iPhone, of course. I was always fascinated by the talks of L4 being specifically designed to avoid scrubbing your L1/L2 cache on operations such as IPC.

pserwylo 12y ago

It's great to see more and more stuff come out of NICTA. For those who are unaware, it is a government funded research institution in Australia. A big difference from other research institutions is that they are especially focussed on commercially viable research (rather than purely theoretical stiff - although I'm sure they do some work on that too). It is a model that has been used for quite some time on Aus, with the CSIRO doing the same thing for more general (I.e. not specifically ICT) research. The CSIRO has done some beautifull research which forms the backbones of technology such as WiFi. So, putting aside recent budgetry and financial issues, it is great to see stuff like this being released by them. Here's to many more years of fruitful research.

userbinator 12y ago

An OS that is proved to be essentially perfectly secure? For some reason this brings up thoughts of trusted computing, and not in a good way...

pflanze 12y ago
You seem to be misunderstanding the kind of security this is about. It's not about taking away control by the owner, just about preventing ways of control by third parties that you as owner didn't intend to give. From https://en.wikipedia.org/wiki/Trusted_computing https://en.wikipedia.org/wiki/Trusted_computing: > TC is controversial as the hardware is not only secured for its owner, but also secured against its owner. Whereas here if you're not happy with what the OS does, you can wipe it and still have full control over the hardware. And the OS is OpenSource, accessible to the hardware owner to modify if some kind of control it asserts isn't satisfying.
- gsnedders 12y ago
  Not the parent commenter, but: A proven kernel could be seen as taking control away on devices where root access cannot be legitimately obtained. I guess some might perceive it as scary given many people in tech circles root their phones (and similar devices), when root access is normally obtained through OS-level security bugs, and it is often (though I think somewhat decreasingly?) used to install third-party OSes on such devices.
  - pflanze 12y ago
    Agreed, although the blame then still lies with the device the secure kernel is running on, or the company that produces it, or the client for choosing to buy it. I guess you can say that proven software is power, and power can be misused.

bjourne 12y ago

I don't suppose anyone has, or know where to find, a generated pdf of the extensive Latex documentation? My own pdflatex skills are failing me. :/

vlad003 12y ago
Conveniently enough, I just generated myself a pdf of it: http://avacariu.me/files/seL4-manual.pdf http://avacariu.me/files/seL4-manual.pdf
- bjourne 12y ago
  Thanks

DCKing 12y ago

Is there any recent benchmark of an L4 implementation with servers compared to a modern monolithic Linux or *BSD kernel? I'm still thinking there's huge untapped potential in microkernels and I wonder how the "state of the art" stacks up against modern monolithic kernels on processors with a lot of cache.

haberman 12y ago

This link to the GitHub repository doesn't give a lot of the context about why this is exciting. As others have mentioned, seL4 is "The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement." But for many years it was proprietary, and only available under commercial terms. The paper was published in 2009, so it's been five years that it was proprietary. As of today at noon, the kernel was released under GPLv2 and userland under two-clause BSD. That is exciting.

phkahler 12y ago
"The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement." And as soon as one person makes a commit, that proof is invalid right?
- klibertp 12y ago
  Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong? Anyway, I'm going to read more about what and how they did, it's fascinating to see a non-trivial software system proven correct.
  - sanxiyn 12y ago
    Yes, that's how they did it. Quoting from the paper: "Note that we have integrated all proofs into an automated proof checking suite, similar to an automated regression-test suite, but using machine-checked formal proofs instead of executable tests. This provides an automatic check, after each commit into the version control system, of the state of all the existing formal proofs, and identifies which specific portions of the proof must be re-established."
  - daveasdf 12y ago
    > Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong? Yes, that's the plan. Internally this is how we have been operating since 2009, when the proof was first completed: You don't push a change to the verified kernel branch unless you are willing (or are able to convince someone else) to do the proof updates. We don't yet have a regression website publicly available, but it's on the short-term roadmap.

awhitty 12y ago

Can someone explain to me what it means for a kernel to have an end-to-end proof of implementation? Does it just mean that the kernel is implemented bug-free? That it will never panic?

klibertp 12y ago
It won't. See here: http://sel4.systems/FAQ/#verif http://sel4.systems/FAQ/#verif It's actually a very impressive piece of work, I can't wait to read about the details of how it was done.
- sanxiyn 12y ago
  Then go read http://www.nicta.com.au/pub?id=7371 http://www.nicta.com.au/pub?id=7371 :)