BootSafe—Malicious Boot Firmware Detection

ATC-NY developed BootSafe for detecting malicious boot firmware, and for limiting the possible damage that such code can cause. BootSafe implements a static check, based on Efficient Code Certification (ECC) as modules of firmware are loaded, and before they are executed.

At the heart of the ECC technique is a certifying compiler that produces both a very well structured executable, and a certificate. The certificate is a detailed description of the expression types and other security-relevant aspects of the original program, with pointers to the corresponding blocks of compiled code. The static check compares the executable to the assertions in the certificate.

We applied the Efficient Code Certification (ECC) technique to boot software (particularly, boot-time device drivers) for the Open Firmware platform. We built a prototype certifying compiler for the Java language with a back-end that generates Forth FCode, as required for Open Firmware drivers. The BootSafe verifier can then independently check that this Forth FCode satisfies type safety and other conditions appropriate to Java.