Portable software fault isolation

Joshua A. Kroll, Gordon Stewart, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationProceedings - 2014 IEEE 27th Computer Security Foundations Symposium, CSF 2014
PublisherIEEE Computer Society
Pages18-32
Number of pages15
ISBN (Electronic)9781479942909
DOIs
StatePublished - Nov 13 2014
Event27th IEEE Computer Security Foundations Symposium, CSF 2014 - Vienna, Austria
Duration: Jul 19 2014Jul 22 2014

Publication series

NameProceedings of the Computer Security Foundations Workshop
Volume2014-January
ISSN (Print)1063-6900

Other

Other27th IEEE Computer Security Foundations Symposium, CSF 2014
CountryAustria
CityVienna
Period7/19/147/22/14

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Architecture Portability
  • Memory Safety
  • Software Fault Isolation
  • Verified Compilers

Fingerprint Dive into the research topics of 'Portable software fault isolation'. Together they form a unique fingerprint.

  • Cite this

    Kroll, J. A., Stewart, G., & Appel, A. W. (2014). Portable software fault isolation. In Proceedings - 2014 IEEE 27th Computer Security Foundations Symposium, CSF 2014 (pp. 18-32). [6957100] (Proceedings of the Computer Security Foundations Workshop; Vol. 2014-January). IEEE Computer Society. https://doi.org/10.1109/CSF.2014.10