Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

SeL4 Whitepaper [pdf]

sel4.systems

Post reply on HN
Print view View original

21–30 of 31 posts

Re: SeL4 Whitepaper [pdf]

#21

Post by person_of_color »

762236 wrote: post #17
vander_elst wrote: post #6

Does anyone have more information about where sel4 is used in production?

Self driving cars via driveghost.com: "Ghost has assembled a team of leading experts in formal methods, an approach to software development that makes it possible to build complex software systems that can be proven to run without bugs or errors. Unlike existing systems built on error-prone platforms, Ghost will be the first to bring formal methods to the roadways with the world's only formally verified runtime built…

Seems like a dumb approach that only marketing would come up with.

The challenge is SDC is AI, not correctness of the kernel that the AI stack runs on. Is an SDC based on a formally verified OS but using logistic regression safe?

Re: SeL4 Whitepaper [pdf]

#22

Post by technion »

simcop2387 wrote: post #14
5d749d7da7d5 wrote: post #11

What will it take for there to be a sel4 router/firewall I can build/buy? Anything directly connected to the internet needs these kind of security guarantees.

The two big things are a network stack that can act as a router (SeL4 has no network stack at all) and drivers. I;d imagine that a decent portion could be ripped from another open source operating system and run in userspace in SeL4 and get some benefits, but I'm not aware of any real effort to do that. Otherwise the usual way to use SeL4 as a hypervisor and just run linux under itm which gets you some benefits but p…

Would a good first target here be SDN switches? In general, their own networking is mostly for remote access.

Re: SeL4 Whitepaper [pdf]

#23

Post by microkerneldude »

Thanks for featuring my white paper. Some responses to some of the comments.

"Opinionated": guilty as charged. However, I claim that the opinions are well-grounded in fact.

Deployments: There are seL4-based devices in regular use in several defence forces. And it's being built in to various products, including civilian, eg critical infrastructure protection. And much we only hear anecdotally – that's open source...

Re: SeL4 Whitepaper [pdf]

#24

Post by microkerneldude »

Re scalability of verification: you don't have to verify everything to get a massive security/safety boost. A well-structured system has a small trusted computing base (TCB), and if you get that right, your system can be pretty secure even if parts of the TCB remain unverified. Eg drivers and network stacks are outside the TCB if you encrypt all data, they can only threaten availability. This was just demonstrated pretty well with AMNESIA:33: for an seL4-based OS, it's just a minor issue, not a critical vulnerability: https://hensoldt-cyber.com/2020/12/08/how-amnesia33-does-aff.... This confirms my analysis from a few years ago, looking at critical exploits in Linux and how seriously they'd be in an seL4-based OS (hint: mostly not at all): https://ts.data61.csiro.au/publications/csiro_full_text//Big...

Re: SeL4 Whitepaper [pdf]

#25

Post by aidenn0 »

5d749d7da7d5 wrote: post #11

What will it take for there to be a sel4 router/firewall I can build/buy? Anything directly connected to the internet needs these kind of security guarantees.

Is there a use case for a microkernel firewall? If you compromise just the tcp/ip stack, you can send and receive arbitrary packets, which is exactly what you would use a root exploit on a monolithic kernel to do.

Re: SeL4 Whitepaper [pdf]

#26

Post by aidenn0 »

person_of_color wrote: post #21
762236 wrote: post #17

Earlier quoted context omitted.

Self driving cars via driveghost.com: "Ghost has assembled a team of leading experts in formal methods, an approach to software development that makes it possible to build complex software systems that can be proven to run without bugs or errors. Unlike existing systems built on error-prone platforms, Ghost will be the first to bring formal methods to the roadways with the world's only formally verified runtime built…

Seems like a dumb approach that only marketing would come up with. The challenge is SDC is AI, not correctness of the kernel that the AI stack runs on. Is an SDC based on a formally verified OS but using logistic regression safe?

It's at least safe from someone hacking into it and intentionally (or accidentally) causing harm.

Re: SeL4 Whitepaper [pdf]

#27

Post by moonchild »

person_of_color wrote: post #21
762236 wrote: post #17

Earlier quoted context omitted.

Self driving cars via driveghost.com: "Ghost has assembled a team of leading experts in formal methods, an approach to software development that makes it possible to build complex software systems that can be proven to run without bugs or errors. Unlike existing systems built on error-prone platforms, Ghost will be the first to bring formal methods to the roadways with the world's only formally verified runtime built…

Seems like a dumb approach that only marketing would come up with. The challenge is SDC is AI, not correctness of the kernel that the AI stack runs on. Is an SDC based on a formally verified OS but using logistic regression safe?

A verifiably correct kernel is a necessary, but not sufficient condition for a self-driving vehicle to be trustworthy.

Re: SeL4 Whitepaper [pdf]

#28

Post by cmrx64 »

kaba0 wrote: post #13
cmrx64 wrote: post #8

i've been working on and off (mostly off) on https://robigalia.org/ for five years now, and interned with the sel4 verification team. feel free to swing by freenode#robigalia if you you want to chat sel4 or trustworthy software, there's a small group collected over the years that would love to answer your questions :)

What’s your opinion on the scalability of formal methods? Isn’t it still the case that basically formal verification is impossible to do for larger code bases (like at least 10-100x that of sel4 in lines of code) and even sel4 took many many years and experts?

current tools, verifying C code like seL4? never going to happen. but i'm hopeful about new techniques, things like the work Amal Ahmed http://www.ccs.neu.edu/home/amal/ is doing. you don't need to formally verify the entire codebase for basic properties like "can compose with the sel4 proofs" if your runtime/compiler/language/OS is all participating. right now you have to fight against the fact that none of the software of interest is well-understood mechanically by other software.

Re: SeL4 Whitepaper [pdf]

#29

Post by microkerneldude »

ncmncm wrote: post #20

I wonder if seL4 would make a better basis for Qubes than the Xen it is on now. In particular, does Xen provide anything seL4 doesn't?

In terms of security, the answer is a clear yes. Xen is kernel of 100+kSLOC of unverified code, while seL4 is verified. On top of that, Xen has Dom0 and thus a complete Linux system in its TCB. What Xen has over seL4 is the management/admin framework. But there is a project to port Qubes to seL4, waiting for the funding to be cleared.

Re: SeL4 Whitepaper [pdf]

#30

Post by microkerneldude »

5d749d7da7d5 wrote: post #11

What will it take for there to be a sel4 router/firewall I can build/buy? Anything directly connected to the internet needs these kind of security guarantees.

Simpler versions of such devices exist, eg HENSOLDT Cyber markets a secure VPN gateway that is built on seL4. Over the years we've been in on-and-off discussions with vendors of networking equipment, it's always a battle between those in the company who take security seriously and those resisting any rocking of the boat. Having said that, we're presently in such a discussion again and it's looking promising so far. However, it's entirely possible that someone has already done it and is not talking about it...
Post reply on HN