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

Roberto Guanciale

School of Computer Science and Communication
KTH Royal Institute of Technology
Sweden

Formal verification of low-level execution platforms

Abstract

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

• R. Guanciale. Formal verification of low-level execution platforms. Slides from the EWSCS 2017 course.
• Lecture 1 [pdf]
• Lecture 2 [pdf]
• Lecture 3 [pdf]
• Lecture 4 [pdf]
• Videos from the lectures (unedited, large files).
• Lecture 1 [mts]
• Lecture 2 [mts]
• Lecture 3 [mts]
• Lecture 4 [mts]


• 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]

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