Paper Info
Title
Portable Software Fault Isolation
Abstract
We present a new technique for architecture portable software fault isolation (SFI), together with a prototype implementation in the Coq proof assistant. Unlike traditional SFI, which relies on analysis of assembly-level programs, we analyze and rewrite programs in a compiler intermediate language, the Cminor language of the Comp Cert C compiler. But like traditional SFI, the compiler remains outside of the trusted computing base. By composing our program transformer with the verified back-end of Comp Cert and leveraging Comp Cert's formally proved preservation of the behavior of safe programs, we can obtain binary modules that satisfy the SFI memory safety policy for any of Comp Cert's supported architectures (currently: Power PC, ARM, and x86-32). This allows the same SFI analysis to be used across multiple architectures, greatly simplifying the most difficult part of deploying trustworthy SFI systems.
Year
DOI
Venue
2014
10.1109/CSF.2014.10
Computer Security Foundations Symposium
Keywords
Field
DocType
program compilers,software fault tolerance,theorem proving,trusted computing,Cminor language,CompCert C compiler,Coq proof assistant,SFI memory safety policy,architecture portable software fault isolation,assembly-level program analysis,compiler intermediate language,trusted computing base,trustworthy SFI systems,Architecture Portability,Memory Safety,Software Fault Isolation,Verified Compilers
Memory safety,Programming language,Trustworthiness,Computer science,Software fault isolation,Compiler,Intermediate language,Trusted computing base,Semantics,Operating system,Distributed computing,Proof assistant
Conference
ISSN
Citations 
PageRank 
1063-6900
9
0.49
References 
Authors
27
3
Name
Order
Citations
PageRank
Joshua Kroll1143.38
Gordon Stewart2332.52
Andrew W. Appel32599292.71