[seL4 Announce] seL4 with proof on x64

Announcements about seL4 -- low volume list announce at sel4.systems
Mon Jul 30 17:06:27 AEST 2018


Dear seL4 community,

it’s my pleasure to announce that even more proofs have become available for seL4.

In particular, the Intel x64 version of seL4 now has a functional correctness proof from abstract specification down to the C code.

This brings the number of architecture configurations seL4 is verified for up to three (ARMv7, ARMv7 with hypervisor extensions, Intel x64) with a fourth one (RISC-V) in progress.

The x64 functional correctness proof does not yet include the fast path, VT-x, or VT-d extensions, nor binary verification or the security proofs we have for ARM, but functional correctness is the core part for all of these other properties and is in itself a big step forward for reliability of the x64 code base.

As usual, the proofs and code for seL4 are available on https://github.com/seL4/l4v and https://github.com/seL4/seL4.

Enjoy!
Gerwin for the Trustworthy Systems Team


More information about the Announce mailing list