Hi seL4 friends,

Any thoughts and/or feelings about the Hyperkernel paper from SOSP'17?

This paper describes an approach to designing, implementing, and formally verifying the functional correctness of an OS kernel, named Hyperkernel, with a high degree of proof automation and low proof burden.

https://homes.cs.washington.edu/~helgi/papers/hyperkernel.pdf

Indeed (you’ll find yours truly credited as the shepherd of the paper, which implies I reviewed it ;-)

The high-level summary: It’s an impressive achievement to do this verification in a fully automated way (“only” 8 years after we did it manually in seL4 ;-)

Unlike seL4, which was designed for real-world use from Day 1, hyperkernel is a toy system, and the approach doesn’t scale to non-toys. This is a consequence of their “finiteness” requirement. The same approach won’t work for seL4 (despite seL4’s simplicity).

Gernot