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

ACM Software System Award Given to seL4 Microkernel

awards.acm.org

Post reply on HN
Print view View original

61–66 of 66 posts

Re: ACM Software System Award Given to seL4 Microkernel

#61

Post by senko »

langfan wrote: post #57
senko wrote: post #39

Earlier quoted context omitted.

SeL4 is a very interesting kernel even without taking the proof into account (eg in platforms/builds that the proof doesn't cover). I wish someone would build a beyond-posix desktop OS on top of it...

Why is it interesting?

It's at the same time pure microkernel and performant and usable in real world (not just a research project).

The memory management, scheduling and IPC are implemented in an interesting and novel way (compared to your typical mainstream OS) and allow for quite different OS design.

In particular, capability-based IPC and memory management could provide a robust base for a secure OS from the ground up, instead playing whackamole in an aging POSIXish design.

Sadly (tho I understand the rationale), most approaches to building a full OS on top of (L4 in general) are "run userspace Linux in an isolated container", which kind of ignores all the power underneath.

Re: ACM Software System Award Given to seL4 Microkernel

#62

Post by langfan »

langfan wrote: post #57
senko wrote: post #39

Earlier quoted context omitted.

SeL4 is a very interesting kernel even without taking the proof into account (eg in platforms/builds that the proof doesn't cover). I wish someone would build a beyond-posix desktop OS on top of it...

Why is it interesting?

Thanks to all who replied.

Re: ACM Software System Award Given to seL4 Microkernel

#63

Post by bjoli »

hedora wrote: post #52
bjoli wrote: post #32

Earlier quoted context omitted.

Maybe an ARM desktop once multi core is implemented and verified. Verifying the whole thing for x86 seems scary. It is a kind of undertaking that gives normal people a glimpse of how ADHD is. It is a huge task and I would not know how to structure it, where to start and how to predict and plan all the intermediate steps.

The only thing that works is modularity. Write down all the modules, then write down their dependencies on each other. Make sure the dependency graph is as close to a line as possible. This is called “layering” in software engineering. Now, figure out how to prove each layer correct.

Of course. But that approach was complex enough for risc-v with is a much much simpler architecture

Re: ACM Software System Award Given to seL4 Microkernel

#65

Post by kjs3 »

hedora wrote: post #51
kjs3 wrote: post #42

Earlier quoted context omitted.

It's proven correct against specification. That's not the same thing as 'secure' (although it helps).

The specification includes the semantics of the hardware it runs on, and shows security properties. Having said that, it is surprisingly easy to get hardware to violate its specifications.

Which...is not the same thing as 'secure' (although it helps).

Re: ACM Software System Award Given to seL4 Microkernel

#66

Post by suavesito »

tptacek wrote: post #21
suavesito wrote: post #19

Earlier quoted context omitted.

Except that making changes can actually invalidate the proof that were made. At least it matters in the sense that Apple should have made an arrangement so the things added didn't invalidate the correctness.

That's not really how any of this works. The formally verified kernel of the operating system gives you some assurance that your primitives are reliable (unlike on, say, Linux, where you're always a kernel reference tracking bug away from an LPE). But the "application" code you build on top of L4 doesn't "inherit" that formal verification; it's just code, with code bugs. If you formally verify your own code, it's ver…

Absolutely, the problem I'm referring to is if Apple changed the kernel and not only built an application on top of it. I don't know, but maybe Apple just built an application on top, which seems sensible.
Post reply on HN