Mads Dam gave a PhD course on provable security for low level execution platforms at the Bertinoro International Spring School 2018 (in March 2018).

Abstract: Much attention has been paid in the recent years to the problem of verification for various types of low level execution platforms such as OS kernels, device drivers, hypervisors, and cryptographic software. In the course we cover a range of topics related to this problem: Formulating correct and relevant verification goals, formally modelling the hardware platforms and security requirements, and formally verifying that the requirements are met. We start in a rather idealised setting suitable for very simple hardware platforms such as those found in legacy embedded control systems, and gradually add system features such as virtual memory, devices and IO, and caches, and examine how the formalisations and verification approaches are adapted. The course presupposes familiarity with first order logic, the use of first order logic for modelling of computer systems, transition system semantics, and, preferably also some basic familiarity with processor architecture. At the end of the course the student should be able to independently model a piece of simple sequential system software and verify it at the level of transition system semantics against a high level behavioural specification.

Slides: Link

More info: