Skip to main content

Portable software fault isolation

Author(s): Kroll, JA; Stewart, G; Appel, Andrew W.

To refer to this page use:
Full metadata record
DC FieldValueLanguage
dc.contributor.authorKroll, JA-
dc.contributor.authorStewart, G-
dc.contributor.authorAppel, Andrew W.-
dc.identifier.citationKroll, JA, Stewart, G, Appel, AW. "Portable software fault isolation" Proceedings of the Computer Security Foundations Workshop, 2014-January, 18 - 32, doi:10.1109/CSF.2014.10en_US
dc.description.abstract© 2014 IEEE.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.en_US
dc.format.extent18 - 32en_US
dc.relation.ispartof27th Computer Security Foundations Symposiumen_US
dc.rightsThis is the author’s final manuscript. All rights reserved to author(s).en_US
dc.titlePortable software fault isolationen_US
dc.typeConference Articleen_US

Files in This Item:
File Description SizeFormat 
AppelCSF2014.pdf369.04 kBAdobe PDFView/Download

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.