1199

LESSWRONG
LW

1198
Personal Blog

6

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

by [anonymous]
24th Jun 2014
1 min read
9

6

Personal Blog

6

[LINK] seL4, secure operating system kernel is being open-sourced
16lukeprog
4[anonymous]
10lukeprog
0[anonymous]
12Metus
6[anonymous]
9Shmi
8David_Gerard
6somervta
New Comment
9 comments, sorted by
top scoring
Click to highlight new comments since: Today at 2:48 AM
[-]lukeprog11y160

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

Reply
[-][anonymous]11y40

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

Reply
[-]lukeprog11y100

When did you start talking to formal verification researchers?

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

Reply
[-][anonymous]11y00

Awesome, thanks!

Reply
[-]Metus11y120

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.

Reply
[-][anonymous]11y60

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.

Reply
[-]Shmi11y90

an end-to-end proof of implementation correctness

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

Reply
[-]David_Gerard11y80

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

Reply
[-]somervta11y60

You offering?

Reply
Moderation Log
Curated and popular this week
9Comments

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.