4 ms·

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

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)?
- reirob 12y ago
  Just found a great summary about what is proved to be secure and what is assumed: https://news.ycombinator.com/item?id=8100033 https://news.ycombinator.com/item?id=8100033
- read 12y ago
  Can you explain why you are unsure the seL4 model is the best for a secure system?
  - FullyFunctional 12y ago
    I guess today _is_ another day. The fundamental issue is that, IMhO, security classification needs to be attached to the data at the lowest level -- OS level is simply to coarse. Take for example an encrypted channel. At the OS level the channel is treated opaquely whereas at the programming language level, after decryption the authenticated data can be assigned both a different level of secrecy and trust, and it can be data dependent. Strong type systems can ensure that secret data is never accidentally leaked, nor untrusted data used in a trusted context. (For a real-life simple subset of this, see tperl). It may be possible to build such a system on top of seL4, but seL4 isn't sufficient. I do intend on working on this eventually. Incidentally, D. J. Bernstein recently shared a similar complaint about the state of security - the models we use have practically not advanced since the 1950es.
    - fanf2 12y ago
      You should have a look at the literature on capability security, especially http://www.erights.org/elib/capability/duals/myths.html http://www.erights.org/elib/capability/duals/myths.html There was hardly any computer security in the 1950s: it was before time sharing and networking. Your cynicism is over-done.
damian2000 12y ago
Something about L4 here: http://en.wikipedia.org/wiki/L4_microkernel_family http://en.wikipedia.org/wiki/L4_microkernel_family I hadn't heard about it before
- adamnemecek 12y ago
  The paper they published based on their findings, "Improving IPC by kernel design"[0], is pretty #cool and worth reading. [0] http://www.scs.stanford.edu/nyu/04fa/sched/readings/l3.pdf http://www.scs.stanford.edu/nyu/04fa/sched/readings/l3.pdf
FullyFunctional 12y ago
Maybe this is a bad place to ask, but why the virtualization requirement for running Linux on top? Is there for security reasons? There are (have been?) other L4/Linux projects and they didn't require this.

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

reirob 12y ago
Just found a great summary about what is proved to be secure and what is assumed: https://news.ycombinator.com/item?id=8100033 https://news.ycombinator.com/item?id=8100033
read 12y ago
Can you explain why you are unsure the seL4 model is the best for a secure system?
- FullyFunctional 12y ago
  I guess today _is_ another day. The fundamental issue is that, IMhO, security classification needs to be attached to the data at the lowest level -- OS level is simply to coarse. Take for example an encrypted channel. At the OS level the channel is treated opaquely whereas at the programming language level, after decryption the authenticated data can be assigned both a different level of secrecy and trust, and it can be data dependent. Strong type systems can ensure that secret data is never accidentally leaked, nor untrusted data used in a trusted context. (For a real-life simple subset of this, see tperl). It may be possible to build such a system on top of seL4, but seL4 isn't sufficient. I do intend on working on this eventually. Incidentally, D. J. Bernstein recently shared a similar complaint about the state of security - the models we use have practically not advanced since the 1950es.
  - fanf2 12y ago
    You should have a look at the literature on capability security, especially http://www.erights.org/elib/capability/duals/myths.html http://www.erights.org/elib/capability/duals/myths.html There was hardly any computer security in the 1950s: it was before time sharing and networking. Your cynicism is over-done.

damian2000 12y ago

Something about L4 here: http://en.wikipedia.org/wiki/L4_microkernel_family http://en.wikipedia.org/wiki/L4_microkernel_family I hadn't heard about it before

adamnemecek 12y ago
The paper they published based on their findings, "Improving IPC by kernel design"[0], is pretty #cool and worth reading. [0] http://www.scs.stanford.edu/nyu/04fa/sched/readings/l3.pdf http://www.scs.stanford.edu/nyu/04fa/sched/readings/l3.pdf

FullyFunctional 12y ago

Maybe this is a bad place to ask, but why the virtualization requirement for running Linux on top? Is there for security reasons? There are (have been?) other L4/Linux projects and they didn't require this.