AI helps you reading Science
AI generates interpretation videos
AI extracts and analyses the key points of the paper to generate videos automatically
AI parses the academic lineage of this thesis
AI extracts a summary of this paper
We have argued that software-based fault isolation can be a practical tool in constructing secure systems
Evaluating SFI for a CISC architecture
USENIX Security, pp.209-224, (2006)
Executing untrusted code while preserving security requires that the code be prevented from modifying memory or executing instructions except as explicitly allowed. Software-based fault isolation (SFI) or "sandboxing" enforces such a policy by rewriting the untrusted code at the instruction level. However, the original sandboxing techniqu...More
PPT (Upload PPT)
- Secure systems often need to execute a code module while constraining its actions with a security policy.
- Softwarebased fault isolation (SFI) implements such isolation via instruction rewriting, but previous research left the practicality of the technique uncertain.
- The original SFI technique works only for RISC architectures, and much followup research has neglected key security issues.
- The authors find that SFI can be implemented for the x86 with runtime overheads that are acceptable for many applications, and that the technique’s security can be demonstrated with a rigorous machine-checked proof
- Secure systems often need to execute a code module while constraining its actions with a security policy
- We find that Softwarebased fault isolation can be implemented for the x86 with runtime overheads that are acceptable for many applications, and that the technique’s security can be demonstrated with a rigorous machine-checked proof
- As far as we know, our work described in Section 9 was the first machine-checked or completely formalized soundness proof for an Softwarebased fault isolation technique or implementation
- We have argued that software-based fault isolation can be a practical tool in constructing secure systems
- Using a novel technique of artificially enforcing alignment for jump targets, we show how a simple sandboxing implementation can be constructed for an architecture with variable-length instructions like the x86
- The authors have argued that software-based fault isolation can be a practical tool in constructing secure systems.
- The authors give two new optimizations, which along with previously known ones minimize the runtime overhead of the technique, and argue for the importance of an architecture that includes separate verification.
- The authors have constructed an implementation of the technique which demonstrates separate verification and is scalable to large and complex applications.
- Though some related techniques have lower runtime overheads, and others can offer additional security guarantees, SFI’s combination of simplicity and performance is a good match for many uses
- This section compares our work with previous implementations of SFI, and with other techniques that ensure memory safety or isolation including code rewriting, dynamic translation, and low-level type systems. It also distinguishes the isolation provided by SFI from the subversion protection that some superficially similar techniques provide.
10.1 Other SFI implementations
Binary sandboxing was introduced as a technique for fault-isolation by Wahbe, Lucco, Anderson, and Graham . The basic features of their approach were described in Sections 2 and 4. Wahbe et al mention in a footnote that their technique would not be applicable to architectures like the x86 without some other technique to restrict control flow, but then drop the topic.
Subsequent researchers generally implemented a restriction on control flow for CISC architectures by collecting an explicit list of legal jump targets. The best example of such a system is Small and Seltzer’s MiSFIT , an assembly-language rewriter designed to isolate faults in C++ code for an extensible operating system. MiSFIT generates a hash table from the set of legal jump targets in a program, and redirects indirect jumps through code that checks that the target appears in the table. Function return addresses are also stored on a separate, protected stack. Because control flow is prevented from jumping into the middle of them, the instruction sequences to sandbox memory addresses don’t require a dedicated register, though MiSFIT does need to spill to the stack to obtain a scratch register in some cases. A less satisfying aspect of MiSFIT is its trust model. The rewriting engine and the code consumer must share a secret, which the rewriter uses to sign the generated code, and MiSFIT relies on the compiler to correctly manage the stack and to produce only safe references to call frames. Besides the trustworthiness problems of C compilers related to their complexity and weak specification (as exemplified by the attack against MiSFIT shown in Figure 1), this approach also requires something like a public-key certificate infrastructure for code producers, introducing problems of reputation to an otherwise objective question of code behavior.
- The first author is supported by a National Defense Science and Engineering Graduate Fellowship
- Martın Abadi, Mihai Budiu, Ulfar Erlingsson, and Jay Ligatti. Control-flow integrity: Principles, implementations, and applications. In Proceedings of the 12th ACM Conference on Computer and Communications Security, pages 340–353, Alexandria, VA, USA, November 7–11, 2005.
- Martın Abadi, Mihai Budiu, Ulfar Erlingsson, and Jay Ligatti. A theory of secure control flow. In ICFEM 2005, Proceedings of the 7th International Conference on Formal Engineering Methods, pages 111–124, Manchester, UK, November 1–4, 2005.
- Ali-Reza Adl-Tabatabai, Geoff Langdale, Steven Lucco, and Robert Wahbe. Efficient and language-independent mobile programs. In Proceedings of the SIGPLAN ’96 Conference on Programming Language Design and Implementation, pages 127–136, Philadelphia, PA, USA, May 21–24, 1996.
- Andrew W. Appel. Foundational proof-carrying code. In Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, pages 247–257, Boston, MA, USA, June 16–19, 2001.
- Jeremy Condit, Mathew Harren, Scott McPeak, George C. Necula, and Westley Weimer. CCured in the real world. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pages 232–244, San Diego, CA, USA, June 9–11, 2003.
- Crispin Cowan, Calton Pu, Dave Maier, Heather Hinton, Jonathan Walpole, Peat Bakke, Steve Beattie, Aaron Grier, Perry Wagle, and Qian Zhang. Stackguard: Automatic adaptive detection and prevention of bufferoverflow attacks. In 7th USENIX Security Symposium, pages 63–78, Austin, TX, USA, January 28–29, 1998.
- Peter Deutsch and Charles A. Grant. A flexible measurement tool for software systems. In Information Processing 71: Proceedings of IFIP Congress 71, pages 320–326, Ljubljana, Yugoslavia, August 23–28, 1971.
- Daniel C. DuVarney, Sandeep Bhatkar, and V.N. Venkatakrishnan. SELF: a transparent security extension for ELF binaries. In Proceedings of the 2003 New Security Paradigms Workshop, pages 29–38, Ascona, Switzerland, August 18–21, 2003.
- Ulfar Erlingsson. Personal communication, May 2006.
- Ulfar Erlingsson and Fred B. Schneider. SASI enforcement of security policies: A retrospective. In Proceedings of the 1999 New Security Paradigms Workshop, pages 87– 95, Caledon Hills, ON, Canada, September 22–24, 1999.
- Bryan Ford. VXA: A virtual architecture for durable compressed archives. In 4th USENIX Conference on File and Storage Technologies, pages 295–308, San Francisco, CA, USA, December 14–16, 2005.
- Andreas Gal, Christian W. Probst, and Michael Franz. A denial of service attack on the Java bytecode verifier. Technical Report 03-23, University of California, Irvine, School of Information and Computer Science, November 2003.
- Matt Kaufmann and J Strother Moore. An industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering, 23(4):203–213, April 1997.
- Douglas Kilpatrick. Privman: A library for partitioning applications. In Proceedings of the 2003 USENIX Annual Technical Conference (FREENIX Track), pages 273–284, San Antonio, TX, USA, June 12–14, 2003.
- Vladimir Kiriansky, Derek Bruening, and Saman P. Amarasinghe. Secure execution via program shepherding. In 11th USENIX Security Symposium, pages 191–206, San Francisco, CA, USA, August 7–9, 2002.
- Fei Lu. C Plus J software architecture. Undergraduate thesis, Shanghai Jiaotong University, June 2000. English summary at http://www.cs.jhu.edu/̃flu/cpj/CPJ_guide.htm.
- Stephen McCamant. A machine-checked safety proof for a CISC-compatible SFI technique. Technical Report 2006-035, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, MA, May 2006.
- Stephen McCamant and Greg Morrisett. Efficient, verifiable binary sandboxing for a CISC architecture. Technical Report 2005-030, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, MA, May 2005. (also MIT LCS TR #988).
- Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Second ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25–35, Atlanta, GA, USA, May 1, 1999.
- George C. Necula and Peter Lee. Safe kernel extensions without run-time checking. In USENIX 2nd Symposium on OS Design and Implementation, pages 229–243, Seattle, WA, USA, October 29–31, 1996.
- George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In Proceedings of the ACM SIGPLAN’98 Conference on Programming Language Design and Implementation, pages 333–344, Montreal, Canada, June 17–19 1998.
- Nicholas Nethercote and Julian Seward. Valgrind: A program supervision framework. In Proceedings of the Third Workshop on Runtime Verification, Boulder, CO, USA, July 13, 2003.
- Niels Provos, Markus Friedl, and Peter Honeyman. Preventing privilege escalation. In 12th USENIX Security Symposium, pages 231–242, Washington, DC, USA, August 6–8, 2003.
- Kevin Scott and Jack Davidson. Safe virtual execution using software dynamic translation. In Proceedings of the 2002 Annual Computer Security Applications Conference, pages 209–218, Las Vegas, NV, USA, December 9– 13, 2002.
- Christopher Small. MiSFIT: A tool for constructing safe extensible C++ systems. In Proceedings of the Third USENIX Conference on Object-Oriented Technologies, pages 174–184, Portland, OR, USA, June 16–20 1997.
- Michael M. Swift, Brian N. Bershad, and Henry M. Levy. Improving the reliability of commodity operating systems. In Proceedings of the 19th ACM Symposium on Operating Systems Principles, pages 207–222, Bolton Landing, NY, USA, October 19–22, 2003.
- Robert Wahbe, Steven Lucco, Thomas E. Anderson, and Susan L. Graham. Efficient software-based fault isolation. In Proceedings of the 14th ACM Symposium on Operating Systems Principles, pages 203–216, Asheville, NC, USA, December 5–8, 1993.
- Robert S. Wahbe and Steven E. Lucco. Methods for safe and efficient implementations of virtual machines. U.S. Patent 5,761,477, June 1998. Assigned to Microsoft Corporation.
- Simon Winwood and Manuel M. T. Chakravarty. Secure untrusted binaries - provably! In Third International Workshop on Formal Aspects in Security and Trust, pages 171–186, Newcastle upon Tyne, UK, July 18-19, 2005.