Document Type
Report
Date
8-2018
Keywords
formal verification, boot loading, trusted computing, refinement, TPM chip
Language
English
Disciplines
Computer Sciences | Information Security | Software Engineering
Description/Abstract
We introduce the Syracuse Assured Boot Loader Executive (SABLE), a trustworthy secure loader. A trusted boot loader performs a cryptographic measurement (hash) of program code and executes it unconditionally, allowing later-stage software to verify the integrity of the system through local or remote attestation. A secure loader differs from a trusted loader in that it executes subsequent code only if measurements of that code match known-good values. We have applied a rigorous formal verification technique recently demonstrated in practice by NICTA in their verification of the seL4 microkernel. We summarize our design philosophy from a high level and present our formal verification strategy.
Recommended Citation
Constable, Scott D.; Sutton, Rob; Sahebolamri, Arash; and Chapin, Steve, "Formal Verification of a Modern Boot Loader" (2018). Electrical Engineering and Computer Science - Technical Reports. 183.
https://surface.syr.edu/eecs_techreports/183
Source
Local input
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
