13–15 Sept 2021
LPC Virtual
US/Mountain timezone

Invited talk: How can we formally verify Rust for Linux?

13 Sept 2021, 11:45
30m
Refereed Track/Virtual-Room (LPC Virtual)

Refereed Track/Virtual-Room

LPC Virtual

150

Speaker

Alastair Reid

Description

Using Rust in Linux aims to create more solid, secure code: avoiding memory safety issues and concurrency issues by taking advantage of Rust's language features and by designing a safe API for drivers to use. This talk examines how / whether we can go further using automatic formal verification tools.

Can we go beyond the checks that Rust provides?
What additional checks would we want to perform?
What can be done using the tools that exist today?
What needs to be done to make this useful to developers? (Spoiler: we are not there yet)

Presentation materials

There are no materials yet.