research-article

RockSalt: better, faster, stronger SFI for the x86

Authors:

Greg Morrisett,

Joseph Tassarotti,

Jean-Baptiste Tristan, and

Edward GanAuthors Info & Claims

PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2012

Pages 395 - 404

https://doi.org/10.1145/2254064.2254111

Published: 11 June 2012 Publication History

Abstract

Software-based fault isolation (SFI), as used in Google's Native Client (NaCl), relies upon a conceptually simple machine-code analysis to enforce a security policy. But for complicated architectures such as the x86, it is all too easy to get the details of the analysis wrong. We have built a new checker that is smaller, faster, and has a much reduced trusted computing base when compared to Google's original analysis. The key to our approach is automatically generating the bulk of the analysis from a declarative description which we relate to a formal model of a subset of the x86 instruction set architecture. The x86 model, developed in Coq, is of independent interest and should be usable for a wide range of machine-level verification tasks.

References

[1]

J. Alglave, A. C. J. Fox, S. Ishtiaq, M. O. Myreen, S. Sarkar, P. Sewell, and F. Z. Nardelli. The semantics of Power and ARM multiprocessor machine code. In Proc. of the Workshop on Declarative Aspects of Multicore Programming, pages 13--24. ACM, 2009.

Digital Library

[2]

J. B. Almeida, N. Moreira, D. Pereira, and S. M. de Sousa. Partial derivative automata formalized in Coq. In Proc. of the 15th Intl. Conf. on Implementation and Application of Automata, number 6482 in CIAA '10, pages 59--68. Springer-Verlag, Aug. 2010.

Digital Library

[3]

A. Barthwal and M. Norrish. Verified, executable parsing. In European Symp. on Programming, ESOP '09, pages 160--174. LNCS, 2009.

Digital Library

[4]

J. A. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11: 481--494, 1964.

Digital Library

[5]

A. Chlipala. A verified compiler for an impure functional language. In Proc. of the 37th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 93--106. ACM, 2010.

Digital Library

[6]

D. Cock. Lyrebird: assigning meanings to machines. In Proc. of the 5th Intl. Conf. on Systems Software Verification, SSV'10, pages 6--15. USENIX Association, 2010.

Digital Library

[7]

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In Proc. of the 22nd Intl. Conf. on Theorem Proving in Higher Order Logics, TPHOLs '09, pages 23--42. Springer-Verlag, 2009.

Digital Library

[8]

CoqCoq development team. The Coq proof assistant. http://coq.inria.fr/, 1989--2012.

[9]

L. Correnson, Z. Dargaye, and A. Pacalet. WP plug-in manual. CEA LIST.

[10]

J. Dias and N. Ramsey. Automatically generating instruction selectors using declarative machine descriptions. In Proc. of the 37th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL '10, pages 403--416. ACM, 2010.

Digital Library

[11]

A. C. J. Fox and M. O. Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Interactive Theorem Proving, volume 6172 of LNCS, pages 243--258. Springer, 2010.

Digital Library

[12]

IntelIntel Corporation. Pentium® Processor Family Developer's Manual, volume 3. Intel Corporation, 1996.

[13]

J.-H. Jourdan, F. Pottier, and X. Leroy. Validating LR(1) parsers. In European Symp. on Programming, ESOP '12. Springer, 2012. To appear.

Digital Library

[14]

W. A. H. Jr. and S. Swords. Centaur technology media unit verification. In Computer Aided Verification, 21st Intl. Conf., volume 5643 of LNCS, pages 353--367. Springer, 2009.

Digital Library

[15]

J. Kroll and D. Dean. BakerSFIeld: Bringing software fault isolation to x64. http://www.cs.princeton.edu/~kroll/papers/bakersfield-sfi.pdf.

[16]

X. Leroy. Formal verification of a realistic compiler. Commun. of the ACM, 52 (7): 107--115, 2009.

Digital Library

[17]

J. Lim. Transformer Specification Language: A System for Generating Analyzers and its Applications. PhD thesis, University of Wisconsin-Madison, May 2011.

Digital Library

[18]

C.-K. Luk, R. Cohn, R. Muth, H. Patil, A. Klauser, G. Lowney, S. Wallace, V. J. Reddi, and K. Hazelwood. Pin: building customized program analysis tools with dynamic instrumentation. In Proc. of the ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI '05, pages 190--200. ACM, 2005.

Digital Library

[19]

L. Martignoni, R. Paleari, G. F. Roglia, and D. Bruschi. Testing CPU emulators. In Proc. of the 18th Intl. Symp. on Software Testing and Analysis, pages 261--272. ACM, 2009.

Digital Library

[20]

S. McCamant and G. Morrisett. Evaluating SFI for a CISC architecture. In Proc. of the 15th Conf. on USENIX Security Symp., pages 209--224. USENIX Association, 2006.

Digital Library

[21]

N. G. Michael and A. W. Appel. Machine instruction syntax and semantics in higher order logic. In Automated Deduction - CADE-17, 17th Intl. Conf. on Automated Deduction, volume 1831 of LNCS, pages 7--24. Springer, 2000.

Digital Library

[22]

M. Might, D. Darais, and D. Spiewak. Parsing with derivatives: a functional pearl. In Proc. of the 16th ACM SIGPLAN Intl. Conf. on Functional Programming, ICFP '11, pages 189--195. ACM, 2011.

Digital Library

[23]

ContestNative Client team. Native client security contest. http://code.google.com/contests/nativeclient-security/index.html, 2009.

[24]

S. Owens, J. Reppy, and A. Turon. Regular-expression derivatives re-examined. J. Funct. Program., 19: 173--190, March 2009.

Digital Library

[25]

S. Owens, P. Böhm, F. Z. Nardelli, and P. Sewell. Lem: A lightweight tool for heavyweight semantics. In Interactive Theorem Proving, volume 6898 of LNCS, pages 363--369. Springer, 2011.

Digital Library

[26]

A. Pilkiewicz. A proved version of the inner sandbox. In native-client-discuss mailing list, April 2011.

[27]

N. Ramsey and J. W. Davidson. Machine descriptions to build tools for embedded systems. In Languages, Compilers, and Tools for Embedded Systems, volume 1474 of LNCS, pages 176--192. Springer, 1998.

Digital Library

[28]

N. Ramsey and M. F. Fernandez. Specifying representations of machine instructions. ACM Trans. Program. Lang. Syst., 19 (3): 492--524, 1997.

Digital Library

[29]

S. Ray. Towards a formalization of the X86 instruction set architecture. Technical Report TR-08-15, Department of Computer Science, University of Texas at Austin, March 2008.

[30]

S. Sarkar, P. Sewell, F. Z. Nardelli, S. Owens, T. Ridge, T. Braibant, M. O. Myreen, and J. Alglave. The semantics of x86-CC multiprocessor machine code. In Proc. of the 36th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 379--391. ACM, 2009.

Digital Library

[31]

M. Seaborn. A DFA-based x86-32 validator for Native Client. In native-client-discuss mailing list, June 2011.

[32]

P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen. x86-TSO: a rigorous and usable programmer's model for x86 multiprocessors. Commun. ACM, 53 (7): 89--97, 2010.

Digital Library

[33]

R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficient software-based fault isolation. In Proc. of the 14th ACM Symp. on Operating Systems Principles, SOSP '93, pages 203--216. ACM, 1993.

Digital Library

[34]

X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In Proc. of the 32nd ACM SIGPLAN Conf. on Programming Language Design and Implementation, PLDI '11, pages 283--294. ACM, 2011.

Digital Library

[35]

B. Yee, D. Sehr, G. Dardyk, J. B. Chen, R. Muth, T. Ormandy, S. Okasaka, N. Narula, and N. Fullagar. Native Client: a sandbox for portable, untrusted x86 native code. Commun. of the ACM, 53 (1): 91--99, 2010.

Digital Library

[36]

L. Zhao, G. Li, B. D. Sutter, and J. Regehr. Armor: Fully verified software fault isolation. In 11th Intl. Conf. on Embedded Software. ACM, 2011.

Digital Library

Cited By

Yedidia ZTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Lightweight Fault Isolation: Practical, Efficient, and Secure Software SandboxingProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640408(649-665)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620665.3640408
Bai MPan RParmer G(2024)OmniWasm: Efficient, Granular Fault Isolation and Control-Flow Integrity for Arm Microcontrollers2024 IEEE 30th Real-Time and Embedded Technology and Applications Symposium (RTAS)10.1109/RTAS61025.2024.00027(239-251)Online publication date: 13-May-2024
https://doi.org/10.1109/RTAS61025.2024.00027
Jia XKumar ATan G(2023)A Derivative-based Parser Generator for Visibly Pushdown GrammarsACM Transactions on Programming Languages and Systems10.1145/359147245:2(1-68)Online publication date: 15-May-2023
https://dl.acm.org/doi/10.1145/3591472
Show More Cited By

Index Terms

RockSalt: better, faster, stronger SFI for the x86

Recommendations

RockSalt: better, faster, stronger SFI for the x86
PLDI '12

Software-based fault isolation (SFI), as used in Google's Native Client (NaCl), relies upon a conceptually simple machine-code analysis to enforce a security policy. But for complicated architectures such as the x86, it is all too easy to get the ...
Read More
Portable Software Fault Isolation
CSF '14: Proceedings of the 2014 IEEE 27th Computer Security Foundations Symposium

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 ...
Read More
Language-independent sandboxing of just-in-time compilation and self-modifying code
PLDI '11

When dealing with dynamic, untrusted content, such as on the Web, software behavior must be sandboxed, typically through use of a language like JavaScript. However, even for such specially-designed languages, it is difficult to ensure the safety of ...
Read More

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2012

572 pages

ISBN:9781450312059

DOI:10.1145/2254064

General Chairs:
Jan Vitek
Purdue University
,
Haibo Lin
Microsoft China
,
Program Chair:
Frank Tip
IBM T.J. Watson Research Center

ACM SIGPLAN Notices Volume 47, Issue 6
PLDI '12
June 2012
534 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2345156
Issue’s Table of Contents

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 June 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '12

Sponsor:

SIGPLAN

PLDI '12: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 11 - 16, 2012

Beijing, China

Acceptance Rates

PLDI '12 Paper Acceptance Rate 48 of 255 submissions, 19%;

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

120
Total Citations
View Citations
1,164
Total Downloads

Downloads (Last 12 months)49
Downloads (Last 6 weeks)12

Other Metrics

View Author Metrics

Citations

Cited By

Yedidia ZTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Lightweight Fault Isolation: Practical, Efficient, and Secure Software SandboxingProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640408(649-665)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620665.3640408
Bai MPan RParmer G(2024)OmniWasm: Efficient, Granular Fault Isolation and Control-Flow Integrity for Arm Microcontrollers2024 IEEE 30th Real-Time and Embedded Technology and Applications Symposium (RTAS)10.1109/RTAS61025.2024.00027(239-251)Online publication date: 13-May-2024
https://doi.org/10.1109/RTAS61025.2024.00027
Jia XKumar ATan G(2023)A Derivative-based Parser Generator for Visibly Pushdown GrammarsACM Transactions on Programming Languages and Systems10.1145/359147245:2(1-68)Online publication date: 15-May-2023
https://dl.acm.org/doi/10.1145/3591472
Rao XGeorges ALegoupil MWatt CPichon-Pharabod JGardner PBirkedal L(2023)Iris-Wasm: Robust and Modular Verification of WebAssembly ProgramsProceedings of the ACM on Programming Languages10.1145/35912657:PLDI(1096-1120)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591265
Narayan SGarfinkel TTaram MRudek JMoghimi DJohnson EFallin CVahldiek-Oberwagner ALeMay MSahita RTullsen DStefan DAamodt TJerger NSwift M(2023)Going beyond the Limits of SFI: Flexible and Secure Hardware-Assisted In-Process Isolation with HFIProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 310.1145/3582016.3582023(266-281)Online publication date: 25-Mar-2023
https://dl.acm.org/doi/10.1145/3582016.3582023
Lee HSong CKang B(2023)Harnessing the x86 Intermediate Rings for Intra-Process IsolationIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2022.319252420:4(3251-3268)Online publication date: 1-Jul-2023
https://doi.org/10.1109/TDSC.2022.3192524
Yavarzadeh HTaram MNarayan SStefan DTullsen D(2023)Half&Half: Demystifying Intel’s Directional Branch Predictors for Fast, Secure Partitioned Execution2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179415(1220-1237)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179415
Johnson ELaufer EZhao ZGohman DNarayan SSavage SStefan DBrown F(2023)WaVe: a verifiably secure WebAssembly sandboxing runtime2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179357(2940-2955)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179357
Yavarzadeh HTaram MNarayan SStefan DTullsen D(2023)Half&Half: Demystifying Intel’s Directional Branch Predictors for Fast, Secure Partitioned Execution2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179309(1220-1237)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179309
Kulik TDongol BLarsen PMacedo HSchneider STran-Jørgensen PWoodcock J(2022)A Survey of Practical Formal Methods for SecurityFormal Aspects of Computing10.1145/352258234:1(1-39)Online publication date: 5-Jul-2022
https://dl.acm.org/doi/10.1145/3522582
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents