veyepar: Verified seL4 on secure RISC-V processors

Author(s):	Gernot Heiser
Location	Room 6
Date	jan Wed 15	Days Raw Files
Start	11:40	First Raw Start	error-in-template
Duration	0:45:0	Offset	None
End	12:25	Last Raw End
Chapters
Total cuts_time	None min.

https://lca2020.linux.org.au/schedule/presentation/40/
raw-playlist raw-mp4-playlist encoded-files-playlist mp4 svg png

assets release.pdf Verified_seL4_on_secure_RISCV_processors.json
logs
Admin: episode episode list cut list raw files day marks day marks day image_files

State:

Locked:

clear this to unlock

Locked by:

user/process that locked.

Start:

initially scheduled time from master, adjusted to match reality

Duration:

length in hh:mm:ss

Name:

Video Title (shows in video search results)

Emails:

email(s) of the presenter(s)

Released:

has someone authorised pubication

Normalise:

Channelcopy:

m=mono, 01=copy left to right, 10=right to left, 00=ignore.

Thumbnail:

filename.png

Description:

markdown

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.

Comment:

production notes