Automated Formal Verification of a Software Fault Isolation System
By: Matthew Sotoudeh, Zachary Yedidia
Potential Business Impact:
Protects computers from bad code trying to escape.
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.
Similar Papers
Empirical Security Analysis of Software-based Fault Isolation through Controlled Fault Injection
Cryptography and Security
Finds bugs that let hackers break into browsers.
Empirical Security Analysis of Software-based Fault Isolation through Controlled Fault Injection
Cryptography and Security
Finds bugs to stop hackers from stealing your data.
Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
Software Engineering
Checks computer programs for safety errors.