Model-carrying code: a practical approach for safe execution of untrusted applications

ABSTRACT

This paper presents a new approach called model-carrying code (MCC) for safe execution of untrusted code. At the heart of MCC is the idea that untrusted code comes equipped with a concise high-level model of its security-relevant behavior. This model helps bridge the gap between high-level security policies and low-level binary code, thereby enabling analyses which would otherwise be impractical. For instance, users can use a fully automated verification procedure to determine if the code satisfies their security policies. Alternatively, an automated procedure can sift through a catalog of acceptable policies to identify one that is compatible with the model. Once a suitable policy is selected, MCC guarantees that the policy will not be violated by the code. Unlike previous approaches, the MCC framework enables code producers and consumers to collaborate in order to achieve safety. Moreover, it provides support for policy selection as well as enforcement. Finally, MCC makes no assumptions regarding the inherent risks associated with untrusted code. It simply provides the tools that enable a consumer to make informed decisions about the risk that he/she is willing to tolerate so as to benefit from the functionality offered by an untrusted application.

REFERENCES

• 1: Anurag Acharya and Mandar Raje. Mapbox: Using parameterized behavior classes to confine applications. In USENIX Security Symposium, 2000.
• 2: Glenn Ammons , Rastislav Bodík , James R. Larus, Mining specifications, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.4-16, January 16-18, 2002, Portland, Oregon
• 3: Thomas Ball , Sriram K. Rajamani, The SLAM Toolkit, Proceedings of the 13th International Conference on Computer Aided Verification, p.260-264, July 18-22, 2001
• 4: T. Bowen, D. Chee, M. Segal, R. Sekar, T. Shanbhag, and P. Uppuluri. Building survivable systems: An integrated approach based on intrusion detection and damage containment. In DARPA Information Survivability Conference (DISCEX), 2000.
• 5: Guillaume Brat, Klaus Havelund, SeungJoon Park, and William Visser. Java pathfinder: Second generation of a Java model checker. Post-CAV 2000 Workshop on Advances in Verification, 2000.
• 6: C. C. Michael , Anup Ghosh, Simple, state-based approaches to program-based anomaly detection, ACM Transactions on Information and System Security (TISSEC), v.5 n.3, p.203-237, August 2002 [doi>10.1145/545186.545187]
• 7: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 8: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 9: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 10: Daniel C. DuVarney , S. Purushothaman Iyer, C Wolf - A Toolset for Extracting Models from C Programs, Proceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems, p.260-275, November 11-14, 2002
• 11: Dawson Engler, Benjamin Chelf, Andy Chou, and Seth Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2000.
• 12: Úlfar Erlingsson , Fred B. Schneider, SASI enforcement of security policies: a retrospective, Proceedings of the 1999 workshop on New security paradigms, p.87-95, September 22-24, 1999, Caledon Hills, Ontario, Canada [doi>10.1145/335169.335201]
• 13: Ulfar Erlingsson , Fred B. Schneider, IRM Enforcement of Java Stack Inspection, Proceedings of the 2000 IEEE Symposium on Security and Privacy, p.246, May 14-17, 2000
• 14: David Evans and Andrew Tywman. Flexible policy directed code safety. In IEEE Symposium on Security and Privacy, 1999.
• 15: Henry Hanping Feng , Oleg M. Kolesnikov , Prahlad Fogla , Wenke Lee , Weibo Gong, Anomaly Detection Using Call Stack Information, Proceedings of the 2003 IEEE Symposium on Security and Privacy, p.62, May 11-14, 2003
• 16: Stephanie Forrest , Steven A. Hofmeyr , Anil Somayaji , Thomas A. Longstaff, A Sense of Self for Unix Processes, Proceedings of the 1996 IEEE Symposium on Security and Privacy, p.120, May 06-08, 1996
• 17: Timothy Fraser, Lee Badger, and Mark Feldman. Hardening COTS software with generic software wrappers. In IEEE Symposium on Security and Privacy, 1999.
• 18: Ian Goldberg, David Wagner, Randi Thomas, and Eric A. Brewer. A secure environment for untrusted helper applications: confining the wily hacker. In USENIX Security Symposium, 1996.
• 19: L Gong, M Mueller, H Prafullchandra, and R Schemers. Going beyond the sandbox: An overview of the new security architecture in the Java development kit 1.2. In USENIX Symposium on Internet Technologies and Systems, 1997.
• 20: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Grégoire Sutre , Westley Weimer, Temporal-Safety Proofs for Systems Code, Proceedings of the 14th International Conference on Computer Aided Verification, p.526-538, July 27-31, 2002
• 21: Gerard J. Holzmann , Margaret H. Smith, Software Model Checking, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.481-497, October 05-08, 1999
• 22: Http-analyze application. Available from http://www.http-analyze.org/.
• 23: Butler W. Lampson, A note on the confinement problem, Communications of the ACM, v.16 n.10, p.613-615, Oct. 1973 [doi>10.1145/362375.362389]
• 24: David Larochelle and David Evans. Statically detecting likely buffer overflow vulnerabilities. In USENIX Security Symposium, 2001.
• 25: Wenke Lee and Sal Stolfo. Data mining approaches for intrusion detection. In USENIX Security Symposium, 1997.
• 26: David Lie , Andy Chou , Dawson Engler , David L. Dill, A simple method for extracting models for protocol code, Proceedings of the 28th annual international symposium on Computer architecture, p.192-203, June 30-July 04, 2001, Göteborg, Sweden
• 27: Christoph Michael , Anup K. Ghosh, Using Finite Automata to Mine Execution Data for Intrusion Detection: A Preliminary Report, Proceedings of the Third International Workshop on Recent Advances in Intrusion Detection, p.66-79, October 02-04, 2000
• 28: Andrew C. Myers , Barbara Liskov, Protecting privacy using the decentralized label model, ACM Transactions on Software Engineering and Methodology (TOSEM), v.9 n.4, p.410-442, Oct. 2000 [doi>10.1145/363516.363526]
• 29: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 30: L. Pitt , M. K. Warmuth, The minimum consistent DFA problem cannot be approximated within and polynomial, Proceedings of the twenty-first annual ACM symposium on Theory of computing, p.421-432, May 14-17, 1989, Seattle, Washington, United States [doi>10.1145/73007.73048]
• 31: Fred B. Schneider, Enforceable security policies, ACM Transactions on Information and System Security (TISSEC), v.3 n.1, p.30-50, Feb. 2000 [doi>10.1145/353323.353382]
• 32: R. Sekar , M. Bendre , D. Dhurjati , P. Bollineni, A Fast Automaton-Based Method for Detecting Anomalous Program Behaviors, Proceedings of the 2001 IEEE Symposium on Security and Privacy, p.144, May 14-16, 2001
• 33: R Sekar and Prem Uppuluri. Synthesizing fast intrusion prevention/detection systems from high-level specifications. In USENIX Security Symposium, 1999.
• 34: Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. Detecting format-string vulnerabilities with type qualifiers. In USENIX Security Symposium, 2001.
• 35: Premchand Uppuluri , R. Sekar, Intrusion detection/prevention using behavior specifications, 2003
• 36: V. N. Venkatakrishnan , Ram Peri , R. Sekar, Empowering mobile code using expressive security policies, Proceedings of the 2002 workshop on New security paradigms, September 23-26, 2002, Virginia Beach, Virginia [doi>10.1145/844102.844113]
• 37: An Approach for Secure Software Installation, Proceedings of the 16th USENIX conference on System administration, November 03-08, 2002, Philadelphia, PA
• 38: David Wagner , Drew Dean, Intrusion Detection via Static Analysis, Proceedings of the 2001 IEEE Symposium on Security and Privacy, p.156, May 14-16, 2001
• 39: David Wagner , Paolo Soto, Mimicry attacks on host-based intrusion detection systems, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586145]
• 40: Andreas Wespi, Hervé Debar, Marc Dacier, and Mehdi Nassehi. Fixed- vs. variable-length patterns for detecting suspicious process behavior. Journal of Computer Security (JCS), 8(2/3), 2000.
• 41: XSB. The XSB logic programming system v2.3, 2001. Available from http://www.cs.sunysb.edu/~sbprolog.
• 42: Steve Zdancewic , Lantian Zheng , Nathaniel Nystrom , Andrew C. Myers, Untrusted hosts and confidentiality: secure program partitioning, Proceedings of the eighteenth ACM symposium on Operating systems principles, October 21-24, 2001, Banff, Alberta, Canada

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Invasive software (e.g., viruses, worms, Trojan horses)

Additional Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Unauthorized access (e.g., hacking, phreaking)

General Terms:
Security, Verification

Keywords:
mobile code security, policy enforcement, sand-boxing, security policies