Automated Formal Verification of a Software Fault Isolation System

TL;DR

This paper presents an automated formal verification of a Software Fault Isolation system, ensuring that the verifier correctly enforces sandbox boundaries to prevent memory safety violations.

Contribution

It introduces a formal verification approach for the LFI SFI system, addressing potential verifier bugs and enhancing security guarantees.

Findings

Verified that LFI verifier enforces sandbox memory boundaries

Identified potential verifier bugs that could compromise security

Demonstrated the effectiveness of formal methods in SFI verification

Abstract

Software fault isolation (SFI) is a popular way to sandbox untrusted software. A key component of SFI is the verifier that checks the untrusted code is written in a subset of the machine language that guarantees it never reads or writes outside of a region of memory dedicated to the sandbox. Soundness bugs in the SFI verifier would break the SFI security model and allow the supposedly sandboxed code to read protected memory. In this paper, we address the concern of SFI verifier bugs by performing an automated formal verification of a recent SFI system called Lightweight Fault Isolation (LFI). In particular, we formally verify that programs accepted by the LFI verifier never read or write to memory outside of a designated sandbox region.