22nd Estonian Winter School in Computer Science (EWSCS)
XXII Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 5 - 10, 2017

Roberto Guanciale

School of Computer Science and Communication
KTH Royal Institute of Technology

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.

Course materials

Valid CSS! Valid XHTML 1.0 Strict Last changed March 19, 2017 0:26 Europe/Helsinki (GMT +02:00) by local organizers, ewscs17(at)cs.ioc.ee
EWSCS'17 page: http://cs.ioc.ee/ewscs/2017/