No Crash, No Exploit: Automated Verification of Embedded Kernels

TL;DR

This paper presents an automated, efficient method for verifying embedded kernels against crashes and exploits directly from binary code, requiring minimal annotations and applicable to real-world kernels.

Contribution

It introduces a novel verification approach that works on binary executables, enabling fast and simple security and safety checks for embedded kernels without extensive manual effort.

Findings

Successfully verified a new embedded real-time kernel.

Verified an industrial real-time kernel with no modifications.

Method is fast, easy to use, and prevents errors and vulnerabilities.

Abstract

The kernel is the most safety- and security-critical component of many computer systems, as the most severe bugs lead to complete system crash or exploit. It is thus desirable to guarantee that a kernel is free from these bugs using formal methods, but the high cost and expertise required to do so are deterrent to wide applicability. We propose a method that can verify both absence of runtime errors (i.e. crashes) and absence of privilege escalation (i.e. exploits) in embedded kernels from their binary executables. The method can verify the kernel runtime independently from the application, at the expense of only a few lines of simple annotations. When given a specific application, the method can verify simple kernels without any human intervention. We demonstrate our method on two different use cases: we use our tool to help the development of a new embedded real-time kernel, and we verify an existing industrial real-time kernel executable with no modification. Results show that the method is fast, simple to use, and can prevent real errors and security vulnerabilities.