https://microkerneldude.wordpress.com/2021/05/05/sel4-on-risc-v-verified-to-binary-code/ Skip to content Follow: RSS Twitter microkerneldude Random rants and pontifications by Gernot Heiser * Home * About * academia * embedded systems * Open Kernel Labs * operating systems and virtualization * politics and society * safety and security * seL4 * Uncategorized seL4 on RISC-V Verified to Binary Code 2021/05/05 [tall_2] ... and seL4 and RISC-V Foundations form an alliance In June 2020 we announced that the seL4 microkernel, the world's first operating system (OS) kernel with a machine-checked proof of implementation correctness, has now also been verified for the RV64 architecture, making it the first formally verified OS for RISC-V. We are pleased to announce that this verification has now been extended to the executable binary, meaning that the machine code running on the processor is proved to be correct against the kernel's specification. RISC-V is the first 64-bit architecture for which this has been achieved. What does this mean? The previously announced proof means that, according to the semantics of the C language in which seL4 is implemented, the kernel will always behave as specified. Among others this means that seL4 cannot be attacked with stack overflows, malformed inputs or other forms of code injection or control-flow hijacking - it is provably secure in a very strong sense. However, there is still the risk of security holes resulting from a buggy (or compromised) C compiler, or from the compiler and kernel developers interpreting the C semantics differently. The newly completed binary verification completely removes these risks - it guarantees that properties we prove about the C code hold for the executable code, and thus that the executable kernel binary behaves as required by the kernel's formal specification. More than porting to a different ISA [binary]The binary verification toolchain. Dark blue arrows are proved. While seL4's implementation correctness proofs use interactive theorem proving, with hundreds of thousands of (mostly hand-written but machine-checked) lines of proof, the binary verification uses an automated tool chain (see the seL4 White Paper for details). The tool chain converts both the C code as well as the binary into an intermediate language that represents the control flow of the program. It then uses SMT solvers to prove equivalence of the two programs, one short code sequence at a time. SMT solvers prove properties by a very efficient exploration of the state space, using state compression techniques to make the problem tractable. We had previously built the binary-verification toolchain for the 32-bit Armv7 architecture. As the state space grows exponentially with the word size, taking the step to a 64-bit architecture requires overcoming significant scalability challenges - which the ingenuity of our team around Matt Brecknell and Zoltan Kocsis could overcome in the end. Further implications This work represents a significant step for both the RISC-V and seL4 ecosystems. No 64-bit architecture other than RISC-V presently has an OS with such a comprehensive verification and security story. And seL4 has with RISC-V the ideal base for driving further innovation in computer system security, especially for our work on the systematic prevention of information leakage through timing channels, based on the approach we call time protection. Stay tuned for more exciting results to come! [sel4_found] We are now formalising the link between the two ecosystems by announcing that RISC-V International and the seL4 Foundation are joining each other as Associate Members. Share this: * Twitter * Facebook * Like this: Like Loading... From - Uncategorized Leave a Comment Leave a Reply Cancel reply Enter your comment here... [ ] Fill in your details below or click an icon to log in: * * * * * Gravatar Email (required) (Address never made public) [ ] Name (required) [ ] Website [ ] WordPress.com Logo You are commenting using your WordPress.com account. ( Log Out / Change ) Google photo You are commenting using your Google account. ( Log Out / Change ) Twitter picture You are commenting using your Twitter account. ( Log Out / Change ) Facebook photo You are commenting using your Facebook account. ( Log Out / Change ) Cancel Connecting to %s [ ] Notify me of new comments via email. [ ] Notify me of new posts via email. [Post Comment] [ ] [ ] [ ] [ ] [ ] [ ] [ ] [ ] No Safety without (Cyber-)Security! >> * Recent Posts + seL4 on RISC-V Verified to Binary Code + No Safety without (Cyber-)Security! + seL4 is verified on RISC-V! + The seL4 Foundation - What and Why + seL4 Design Principles + What does seL4's license imply? + Can seL4 reduce the cost of satellites? + 10 Years seL4: Still the Best, Still Getting Better + How to (and how not to) use seL4 IPC + Microkernels Really Do Improve Security * Categories + academia + embedded systems + Open Kernel Labs + operating systems and virtualization + politics and society + safety and security + seL4 + Uncategorized * Archives + May 2021 + November 2020 + June 2020 + April 2020 + March 2020 + December 2019 + November 2019 + August 2019 + March 2019 + August 2018 + February 2018 + June 2016 + April 2016 + April 2015 + February 2015 + December 2014 + November 2014 + October 2014 + September 2014 + August 2014 + July 2014 + May 2013 + April 2013 + March 2013 + October 2012 + September 2012 + June 2012 + February 2012 + January 2012 + September 2011 + November 2010 + October 2010 + August 2009 + July 2009 + April 2009 + March 2009 + February 2009 + July 2008 + April 2008 + March 2008 + February 2008 + January 2008 Blog at WordPress.com. [ ] Email (Required) [ ] Name (Required) [ ] Website [ ] [Post Comment] Loading Comments... Comment x [Close and accept] Privacy & Cookies: This site uses cookies. By continuing to use this website, you agree to their use. To find out more, including how to control cookies, see here: Cookie Policy %d bloggers like this: [b]