Provable Time Protection for Eliminating Timing Channels
Abstract
This project aims to develop techniques that allow formally proving the absence of timing channels in an operating system, and apply them to the formally verified seL4 microkernel. It combines systems design, formal hardware models, information flow reasoning and theorem proving to achieve a goal that is widely considered infeasible. Successful completion will result in a system that provably prevents (accidental or intentional) leakage of critical information, such as encryption keys, through timing channels. This would prevent sophisticated attacks, such as the recent Spectre attack, on public clouds, mobile devices and military grade cross domain devices.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jan 14, 2022
- Source ID
- FA23861914021
Entities
People
- Gernot Heiser
Organizations
- Air Force Office of Scientific Research
- Commonwealth Scientific and Industrial Research Organisation
- United States Air Force