The SeL4 Foundation: What and Why

https://microkerneldude.wordpress.com/2020/04/07/the-sel4-foundation-what-and-why/

by ingve • 6 years ago

104 64 6 years ago

microkerneldude.wordpress.com

I'd be really happy to see seL4 thrive and I like that this blog-post shows that the people behind it understand what could potential hold it back - the infrastructure around it. It needs what GNU and systemd are for Linux. And it needs an Arduino/Raspberry Pi - a halo platform that I can buy and play around with.

What I wonder is how this formal verification works. seL4 is written in C and apparently the formal verification is done in a different language. Is it possible to have a programming language where the compiler does the formal verification?

saithound4• 6 years ago

Is it possible to have a programming language where the compiler does the formal verification?

It is possible, but using separate languages (as seL4 does) has certain benefits. For example:

- Kernel developers tend to have C experience. If the OS is writen in C, they have a much larger pool to hire from.

- Any such language would have to be acceptable both for the people who develop the OS and for the people who do the verification: I suspect it's not easy to find something that pleases both crowds.

- C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler.

MaxBarraclough4• 6 years ago

Formal methods aren't just an academic curiosity, they have been used for real-world OS work. https://en.wikipedia.org/wiki/SLAM_project

Less mainstream programming languages get better only if you have an expensive in-house team working on the compiler.

Not if you defer optimisation to an external (and actively maintained) backend like LLVM. Rust and Zig do this.

cwzwarich2• 6 years ago

C compilers get better all the time. Every time someone improves the gcc code generator, seL4 automatically gets a bit faster. Less mainstream programming languages get better only if you maintain an expensive in-house team working on the compiler.

Doesn't SeL4 need -O1 codegen to make their extraction from the generated code (and the thus the rest of the formal proof) work out?

vbezhenar• 6 years ago

How will it prove that this new optimization does not introduce bugs? It's not like GCC is verified compiler.

hinkley• 6 years ago

Probably an Unsolved Problem in computer programming:

If you are trying to solve an old problem a new way, is it necessarily true that having a large pool of applicants is an advantage? It could be a liability.

On the one hand, there could be more variance in a large pool, so you might find a lot of unconventional thinkers who think like you. On the other hand, large groups have social mores, and so the dogma might be difficult to overcome, like the old "people can write fortran in any language" problem.

lawfulcactus• 6 years ago

So, I think what you're missing here is that the 'verification' is a formal specification about the behavior of the kernel, along with a set of proofs about that specification. This is vastly simplified (there are multiple levels of specification, last I checked), but that's the general idea. It's possible to have your compiler automatically derive the specification from your code (and, indeed, the seL4 people have written a Rust-like language called Cogent that does this), but formal verification inherently involves an understanding of what your code is /intended/ to do, and proving that it /does/. The compiler only has information about what it /does/, so it can only generate a specification that describes this. Information about your high-level intentions for the code has to be concretized somewhere, while ensuring that the spec conforms to it-- that's the job of the proof engineers.

turbinerneiter2• 6 years ago

How does this formal specification look like?

From my naive standpoint: input, output, side-effect, time

  [no_sideffect, 1ms]
  fn increment(int i) -> int:
      return i + 1

What this is missing is a formal statement that says "increases the value of the input by one" -> except you accept the function body as formal statement.

Thanks for all the answers here, I guess I'm going to look for some more reading material.

MaxBarraclough4• 6 years ago

What I wonder is how this formal verification works

Curiously it involves Haskell for its specification. [0]

They've also done some very impressive work verifying that the ARM machine code corresponds to the verified C code. They did this not by using a formally verified compiler, but by using GCC and then verifying the correspondence afterwards.

Is it possible to have a programming language where the compiler does the formal verification?

Yes, but these languages are not all that approachable.

There's SPARK, which is Ada-based and has seen real-world use in various life-or-death applications like military aviation.

There's also ZZ, which is in early days, and which aims to be closer to C. [2] [3]

There's also Perfect Developer, a proprietary payware product, which does impressive things adding formal verification machinery to C and C++. [4]

[0] https://en.wikipedia.org/wiki/L4_microkernel_family#High_ass...

[1] https://en.wikipedia.org/wiki/SPARK_(programming_language)

[2] https://github.com/aep/zz

[3] https://news.ycombinator.com/item?id=22245409

[4] https://www.eschertech.com/articles/index.php

wahern3• 6 years ago

How does Perfect Developer compare to Frama-C? Is it more capable or maybe simply more convenient for MISRA verification?

For the unfamiliar, see http://frama-c.com/ and https://en.wikipedia.org/wiki/Frama-C

h91wka6• 6 years ago

Is it possible to have a programming language where the compiler does the formal verification?

Such compiler would require solving halting problem. Most problems related to search of formal proofs are undecidable.

MaxBarraclough4• 6 years ago

This is true, but SPARK and ZZ do it anyway. Automatic deductive program-verification can work, but the halting problem means there will always be truths than cannot be automatically proved. This can still be good enough to get the job done.

In the case of SPARK, it's necessary to use timeouts on the prover. Ugly, sure enough, but real work can still be done with it.

https://docs.adacore.com/spark2014-docs/html/ug/en/tutorial....

wolfgke4• 6 years ago

Such compiler would require solving halting problem.

Wrong: Because of the finite memory instead of an unbounded tape (among other reasons), computers are strictly less expressive than Turing machines.

_0w8t• 6 years ago

Strictly speaking real computers are finite state machines and are trivially decidable from the halting problem point of view. The problem is that it just takes long long time.

seb314• 6 years ago

Such compiler would require solving halting problem.

I don't think so. As long as false-negative results are acceptable. (i.e. it is ok if for some programs no proof if found even though they fulfill the specification)

Occasional false-negatives seem perfectly fine for real-world use.

curryhoward2• 6 years ago

Not if the human provides the proofs and the compiler merely checks them (like in Coq, for example).

qznc• 6 years ago

Practically every compiler does formal verification. The type checking of C for example. The question is what properties you want to verify. It isn't a binary question but rather a continuum from C up to Isabelle/Coq.

cwzwarich2• 6 years ago

Is it really formal verification if the type system is unsound? Due to undefined behavior, a "proven pointer-to-int" may not end up being a valid pointer-to-int at runtime. Even in Haskell, the type system is actually logically inconsistent (see http://okmij.org/ftp/Haskell/impredicativity-bites.html).

skyde• 6 years ago

spark version of Ada is such a language but it use design by contract assertion only.

jiveturkey2• 6 years ago

systemd

nobody needs systemd. nobody but RedHat. it is a step backwards, net net.

mycall• 6 years ago

I see Genode Operating System Framework as the infrastructure it needs.

akavel2• 6 years ago

Hm, as to userland, I wonder why they don't seem to mention GenodeOS in any way?

dathinab• 6 years ago

It's not directly related to them. It's just one of many projects using the kennel.

Also this is not a official post but a semi official one by one of it's members on his personal blog!

snvzz2• 6 years ago

Genode is Affero GPL licensed. Very troublesome.

That's probably why.

akavel2• 6 years ago

Ohhh, now that is something I totally missed, thanks!

microcolonel2• 6 years ago

That "Verification of the multicore kernel" thing seems like it could use some bold, underline, and italics. I doubt it is as simple as adding an AArch64 model.

snvzz2• 6 years ago

Definitely not simple, but simpler than you might imagine.

Specifically, I'm referring to the fact that the microkernel can't be run from more than one CPU at once and can't be preempted, which is an important design decision.

Its execution time is, however, constrained into the WCET, complete with proof. And that is a very small amount of time, allowing for hard real-time applications to be built on top of seL4.

microcolonel2• 6 years ago

Every time I learn more about seL4, I fall a bit more in love with it. Can't wait to see what people do in terms of integration over time.

I think it would be super cool to see L4Linux updated again, and on seL4 this time; maybe start shifting device drivers into tasks behind a low-overhead abstraction. We're going to have Linux and POSIX applications for a loooong time, but maybe we can make incremental progress toward something a bit less braindead.

segfaultbuserr2• 6 years ago

Simple question: What are some seL4 "distros" one can install today? Which types of hardware is supported? And how usable the userland is?

closeneough• 6 years ago

https://genode.org/

tptacek2• 6 years ago

If you're looking for a desktop/end-user operating system (even for a server of some sort), you're not really looking for L4. You might as well just use Qubes; the security model will be similar (in that you'll be "using" hosted Linux, not the underlying OS directly).

L4 gets interesting if you're building another platform.

segfaultbuserr2• 6 years ago

Well, I think it's an interesting idea in itself to build a full operating system based on a secure kernel, even if it's server/CLI only, runs in a virtual machine as a prototype (think GNU Hurd). Isn't it?

exikyut• 6 years ago

Looking at all the comments here, one question seems missing yet relevant: why is CompCert not used?

jiveturkey2• 6 years ago

seL4 is a game-changer

probably overstating the case.

The SeL4 Foundation: What and Why

Related Stories