Presented by

  • Gernot Heiser

    Gernot Heiser
    @GernotHeiser
    http://gernot-heiser.org/

    Gernot is the microkernel dude, having for 25 years led the development of various L4 microkernels. With is group he has produced the L4 kernels that have shipped on billions of Qualcomm mobile modem chips, and are shipping on the secure enclave of all iOS devices. His team has developed the seL4 microkernel, the world's first OS kernel that is mathematically proved free of implementation bugs, and that was open-sourced in July'14. Gernot is a Scientia Professor and John Lions Chair at UNSW and founder and former leader of the Trustworthy Systems group at Data61. He is a Fellow of the ACM, the IEEE and the Australian Academy of Technology and Engineering (ATSE). He has won multiple awards, including ICT Researcher of the year 2016 of the South-East Asian Regional Computing Confederation (SEARCH) and 2015 of the Australian Computer Society (ACS), Entrepreneur of the Year 2014 by Engineers Australia, and New South Wales Scientist of the Year 2009 (Category Engineering, Mathematics and Computer Science). He serves as Chief Scientist (Software) of HENSOLDT Cyber GmbH and was the co-founder and CTO of Open Kernel Labs which was acquired by General Dynamics in 2012.

Abstract

RISC-V has many attractions, ranging from the openness of the architecture, its clean-slate design based on simplicity and scalability, as well as the RISC-V Foundation's strong commitment to security from the ground up. As such, RISC-V is an extremely attractive platform for the open-source seL4 microkernel with its unrivalled verification and security story. This has led industry players, especially Germany-based HENSOLDT Cyber, making a major bet on the combination of RISC-V and seL4, resulting in them funding the formal verification (implementation correctness proof) of seL4 on RISC-V. I will discuss our experience with implementing and verifying seL4 on the RISC-V architecture, and related open-source technologies we are employing to allow us to build secure systems. This includes the CAmkES component framework that supports a security-by-architecture approach, and the Cogent systems language that is designed to reduce the cost of verified system components such as file systems and device drivers. One interesting aspect are timing channels. We have been working for a number of years on *time protection*, the temporal equivalent of memory protection, as a systematic timing-channel prevention. Our experience on x86 and ARM processors is that they lack the mechanisms to do this completely. RISC-V presents an opportunity to get this right, and I will report on my experience working with the RISC-V Foundation's Security Standing Committee to get the required mechanisms into the processor specification.