Explore the implementation and verification of seL4 microkernel on RISC-V architecture in this 45-minute conference talk from linux.conf.au 2020. Delve into the attractions of RISC-V, including its open architecture and commitment to security. Learn about industry investments in combining RISC-V and seL4, focusing on formal verification and implementation correctness proof. Discover related open-source technologies like the CAmkES component framework and Cogent systems language. Examine the challenges of timing channels and the development of time protection mechanisms. Gain insights into collaborations with the RISC-V Foundation's Security Standing Committee to enhance processor specifications for improved security.
Overview
Syllabus
Intro
seL4: The Dream Come True!
A Microkernel is not an OS
Core Mechanism: Object Capability
Microkernel: seL4 vs Linux Licensing
Military-Strength Security
World's Most Secure OS: Arm v7
Background: HENSOLD Cyber
Performance on RV64 Message-passing round-trip latency in cycles
Verification: RISC-V Status
Sharing: Stateful Hardware Low
Time Protection: Partition Hardware
Spatially Partition: Cache Colouring
Foundation Structure
Community Engagement
Taught by
linux.conf.au
