[LINK] seL4, secure operating system kernel is being open-sourced

https://www.lesswrong.com/posts/ATg4akEqLyCirStiF/link-sel4-secure-operating-system-kernel-is-being-open

seL4 is the world’s first (and only?) operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. In 34 days it is going open source:

http://​​sel4.systems/​​

Now if only we could get a provably-correct implementation of the Amoeba operating system kernel on top of this, it’d be the perfect base for a boxed AI software stack.

Comment

https://www.lesswrong.com/posts/ATg4akEqLyCirStiF/link-sel4-secure-operating-system-kernel-is-being-open?commentId=Y226XFSdMGtqckmM4

For more on seL4, see my interview with Gerwin Klein.

Comment

  • id
    YvFDRdfvC7LKmpP4K
  • authors
    [deleted]
  • score
    4
  • omega_karma
  • votes
    2
  • date_published
    2014-06-25T08:54
https://www.lesswrong.com/posts/ATg4akEqLyCirStiF/link-sel4-secure-operating-system-kernel-is-being-open?commentId=YvFDRdfvC7LKmpP4K

When did you start talking to formal verification researchers?

Because, you know, I totally have not wanted to do a PhD under any of these guys, or anything like that...

Comment

  • id
    4ZnWxCNNvXoQATErh
  • authors
    lukeprog
  • score
    10
  • omega_karma
  • votes
    5
  • date_published
    2014-06-25T15:28

When did you start talking to formal verification researchers?

Many months ago. Subscribe to the MIRI blog! :)

  • id
    Qrit46dqoLBS2FFzw
  • authors
    Mark_Friedenbach
  • score
    0
  • omega_karma
  • votes
    0
  • date_published
    2014-06-24T23:30
https://www.lesswrong.com/posts/ATg4akEqLyCirStiF/link-sel4-secure-operating-system-kernel-is-being-open?commentId=Qrit46dqoLBS2FFzw

Awesome, thanks!

https://www.lesswrong.com/posts/ATg4akEqLyCirStiF/link-sel4-secure-operating-system-kernel-is-being-open?commentId=4QMYE4i7kG88CmCEw

Keep in mind, these things are only proven to work as specified. There is no guarantee that the specification itself is secure. Or that there is no side channel attack possible. Or other stuff.

Comment

  • id
    rRJsEyg9yCeCkcyMA
  • authors
    Mark_Friedenbach
  • score
    6
  • omega_karma
  • votes
    3
  • date_published
    2014-06-25T00:50
https://www.lesswrong.com/posts/ATg4akEqLyCirStiF/link-sel4-secure-operating-system-kernel-is-being-open?commentId=rRJsEyg9yCeCkcyMA

Correct. But what it achieves is a massive compression in the size of the attack surface. In as much as you trust the proof system, you know that the code matches the specification, so the only bugs which can exist are those in the specification itself.

https://www.lesswrong.com/posts/ATg4akEqLyCirStiF/link-sel4-secure-operating-system-kernel-is-being-open?commentId=Jzwe3Ry37jP2ug4Ji

an end-to-end proof of implementation correctness

Time to take bets on when the first security hole gets discovered.

Comment

  • id
    tgZ4ku34MffrGECeQ
  • authors
    David_Gerard
  • score
    8
  • omega_karma
  • votes
    4
  • date_published
    2014-06-25T07:22
https://www.lesswrong.com/posts/ATg4akEqLyCirStiF/link-sel4-secure-operating-system-kernel-is-being-open?commentId=tgZ4ku34MffrGECeQ

Took a few years for OpenBSD, and that relied on mere human software engineering skill.

  • id
    7pww8ua3jjp4hJ9ea
  • authors
    somervta
  • score
    6
  • omega_karma
  • votes
    3
  • date_published
    2014-06-25T05:06
https://www.lesswrong.com/posts/ATg4akEqLyCirStiF/link-sel4-secure-operating-system-kernel-is-being-open?commentId=7pww8ua3jjp4hJ9ea

You offering?