[lugm.org] Fwd: [seL4 Announce] seL4 with proof on x64

[Jheengut Pritvi]

---------- Forwarded message ----------
From: Announcements about seL4 -- low volume list <announce at sel4.systems>
Date: 30 July 2018 at 11:06
Subject: [seL4 Announce] seL4 with proof on x64
To: announce at sel4.systems


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
_______________________________________________
Announce mailing list
Announce at sel4.systems
https://sel4.systems/lists/listinfo/announce


This is a great step for Sel4 indeed.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://discuss.lugm.org/pipermail/discuss_discuss.lugm.org/attachments/20180730/2ac75805/attachment.html>