Methods for the Design, Analysis, and Certification of Secure Boot Processes

Methods for the Design, Analysis, and Certification of Secure Boot Processes

Status

This project started in December 2008 and finished in September 2012.

Researchers

Prof. Dr. David Basin, Information Security Group, ETH
Ognjen Maric, Information Security Group, ETH
Chan Ngo, Information Security Group, ETH
Dr. Christoph Sprenger, Information Security Group, ETH
Dr. Tamas Visegrady, IBM Research Rüschlikon

Description

In computer systems with layered architectures, the integrity of higher layers depends on the integrity of the lower layers and this chain begins with the boot process. The secure operation of the lowest-layer boot process is therefore an essential foundation for the integrity of the entire system. This requires the specification and verification of a security policy for the boot process.

The secure boot process problem arises in a number of different settings, for instance, in the construction and certification of cryptographic coprocessors modules at IBM Zurich Research Laboratory such as those of the 4758/4764/4765 family. These modules are programmable secure coprocessors built into a tamper-proof housing with boot software and embedded firmware that controls the security and configuration of the device.

In this project, we apply formal methods to verify the compliance of such boot processes with their intended security policy. These methods yield the high quality guarantees that are required for certification. Our goal is to develop an appropriate methodology for reducing the verification of the compliance of the system to its security policy to a model checking problem. The following issues need to be addressed to achieve this goal:
Specification of the security policy as a collection of functional and temporal properties,
Semi-automatic construction of formal models from the source code of the boot process; this includes
The definition and application of abstraction techniques such as program slicing and abstract interpretation in order to obtain models reduced state spaces that are amenable to automated formal analysis, e.g., state-of-the-art model checking techniques.