<div dir="ltr"><br><div class="gmail_quote">---------- Forwarded message ----------<br>From: <b class="gmail_sendername">Announcements about seL4 -- low volume list</b> <span dir="ltr"><announce@sel4.systems></span><br>Date: 30 July 2018 at 11:06<br>Subject: [seL4 Announce] seL4 with proof on x64<br>To: announce@sel4.systems<br><br><br>Dear seL4 community,<br>
<br>
it’s my pleasure to announce that even more proofs have become available for seL4.<br>
<br>
In particular, the Intel x64 version of seL4 now has a functional correctness proof from abstract specification down to the C code.<br>
<br>
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.<br>
<br>
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.<br>
<br>
As usual, the proofs and code for seL4 are available on <a href="https://github.com/seL4/l4v" rel="noreferrer" target="_blank">https://github.com/seL4/l4v</a> and <a href="https://github.com/seL4/seL4" rel="noreferrer" target="_blank">https://github.com/seL4/seL4</a>.<br>
<br>
Enjoy!<br>
Gerwin for the Trustworthy Systems Team<br>
______________________________<wbr>_________________<br>
Announce mailing list<br>
Announce@sel4.systems<br>
<a href="https://sel4.systems/lists/listinfo/announce" rel="noreferrer" target="_blank">https://sel4.systems/lists/<wbr>listinfo/announce</a><br>
</div><div><br></div><div><br></div><div>This is a great step for Sel4 indeed.<br></div></div>