Hacker News Reader

SEL4 is proven correct. Formally verified. No security holes in the default install, of any sort, ever. I mean, it doesn't do anything. But it has no security holes, with almost mathematical certainty.

View on HN

As a huge believer in formal methods, this statement should _also_ be tempered somewhat. Formal proof is a great technique, but it's incredibly dependent on getting your specs right, which is very hard to do.

As an example, CompCERT is a formally verified C compiler, and it's had a couple bugs as a result of their specification of the underlying hardware being wrong.

I know, I know, I'm mostly being silly about SEL4. Also, obviously, OpenBSD does a lot more than SEL4. :)

Yeah, I get it, and obviously the question is where people want a balance. OpenBSD does more than nothing, less than SELinux-secured Linux, which does less than some other things.

Also, doesn't SEL4 have widespread, practical application? IIRC as the microkernal (maybe under Minix?) on the baseband hardware on cell phones? Maybe I'm confusing it with something else.

Reply on news.ycombinator.com