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.

Source

Local input

Creative Commons License

Creative Commons Attribution-Noncommercial-No Derivative Works 4.0 License
This work is licensed under a Creative Commons Attribution-Noncommercial-No Derivative Works 4.0 License.

Share

COinS
 
 

To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.