Formal verification of low-level execution platforms
The use of software, including life critical systems, is expanding and the volume of threats and attacks is increasing. Our long-term vision is the development of secure, formally verified and certified platforms as the core building block, or root of trust, from which to bootstrap security in future systems.
Here we focus on a separation kernel: a platform that simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. Our main goal it to demonstrate information flow security of this platform: show that information can be transferred among the partitions only using the allowed communication channel. This is done with the support of an interactive theorem prover and uses a detailed model of the instruction set architecture.
The verification is divided in three tasks (1) functional verification of the kernel design, (2) verification of confinement of the untrusted software, and (3) verification that the concrete (low-level) executable program resembles the kernel design.
We will also analyze the security effects of system traits that have not been taken into account while modeling the system (e.g. caches, TLBs). We will demonstrate that, if not properly mitigated, these hardware features can be used to build system level attacks that exploit storage side channels to invalidate the verification results.
- R. Guanciale. Formal verification of low-level execution platforms. Slides from the EWSCS 2017 course.
- Videos from the lectures (unedited, large files).
- R. Guanciale, H. Nemati, M. Dam, C. Baumann. Provably secure memory isolation for Linux in ARM. J. of Comput. Security, v. 24, n. 6, pp. 793-837, 2016. [doi link]
- T. Nipkow. Programming and Proving in Isabelle/HOL. Tutorial for Isabelle2016-1, 2016. [tutorial on Isabelle website]
March 19, 2017 0:26 Europe/Helsinki (GMT +02:00)
local organizers, ewscs17(at)cs.ioc.ee
EWSCS'17 page: //cs.ioc.ee/ewscs/2017/