AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
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)

Cited by: 236|Views157
EI
Full Text
Bibtex
Weibo

Abstract

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

Code:

Data:

Introduction
  • 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
Highlights
  • 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
Conclusion
  • 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
Related work
  • 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 [27]. 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 [25], 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.
Funding
  • The first author is supported by a National Defense Science and Engineering Graduate Fellowship
Reference
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Ulfar Erlingsson. Personal communication, May 2006.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Findings
  • 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.
    Google ScholarFindings
  • 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).
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科