On 23 Jan 2018, at 11:38, Jeff Waugh <jdub@bethesignal.orgmailto:jdub@bethesignal.org> wrote:
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