Model-Carrying Code (MCC): a new paradigm for mobile-code security

ABSTRACT

A new approach for ensuring the security of mobile code is proposed. Our approach enables a mobile-code consumer to understand and formally reason about what a piece of mobile code can do; check if the actions of the code are compatible with his/her security policies; and, if so, execute the code. The compatibility-checking process is automated, but if there are conflicts, consumers have the opportunity to refine their policies, taking into account the functionality provided by the mobile code. Finally, when the code is executed, our framework uses runtime-monitoring techniques to ensure that the code does not violate the consumer's (refined) policies.At the heart of our method, which we call model-carrying code (MCC), is the idea that a piece of mobile code comes equipped with an expressive yet concise model of the code's (security-relevant) behavior. The generation of such models can be automated. MCC enjoys several advantages over current approaches to mobile-code security. It protects consumers of mobile code from malicious or faulty code without unduly restricting the code's functionality. Also, it is applicable to the vast majority of code that exists today, which is written in C or C++. This contrasts with previous approaches such as Java 2 security and proof-carrying code, which are either language-specific or are limited to type-safe languages. Finally, MCC can be combined with existing techniques such as cryptographic signing and proof-carrying code to yield additional benefits.

REFERENCES

• 1: R Bowen, D Chee, M Segal, R Sekar, P Uppuluri, and T Shanbag. Building survivable systems: An integrated approach based on intrusion detection and confinement. In DARPA Information Security Symposium, 2000.
• 2: 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]
• 3: B. Cui, Y. Dong, X. Du, K. Narayan Kumar, C. R. Ramakrishnan, I. V. Ramakrishnan, A. Roychoudhury, S. A. Smolka, and D. S. Warren. Logic programming and model checking. In Static Analysis Symposium. Springer Verlag, 1998.
• 4: S Forrest, S Hofmeyr, and A Somayaji. Intrusion detection using sequences of system calls. Journal of Computer Security, 1998.
• 5: Li Gong, Inside Java 2 platform security architecture, API design, and implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 6: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 7: K Jain and R Sekar. User-level infrastructure for system call interposition: A platform for intrusion detection and confinement. In ISOC Network and Distributed System Security, 2000.
• 8: C Ko, G Fink, and K Levitt. Automated detection of vulnerabilities in privileged programs by execution monitoring. In Computer Security Application Conference, 1994.
• 9: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 10: Charlie Lai , Li Gong , Larry Koved , Anthony Nadalin , Roland Schemers, User Authentication and Authorization in the Java(tm) Platform, Proceedings of the 15th Annual Computer Security Applications Conference, p.285, December 06-10, 1999
• 11: R. Milner, Communication and Concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
• 12: 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]
• 13: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 14: Y. S. Ramakrishna , C. R. Ramakrishnan , I. V. Ramakrishnan , Scott A. Smolka , Terrance Swift , David Scott Warren, Efficient Model Checking Using Tabled Resolution, Proceedings of the 9th International Conference on Computer Aided Verification, p.143-154, June 22-25, 1997
• 15: 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]
• 16: C. R. Ramakrishnan , I. V. Ramakrishnan , Scott A. Smolka , Yifei Dong , Xiaoqun Du , Abhik Roychoudhury , V. N. Venkatakrishnan, XMC: A Logic-Programming-Based Verification Toolset, Proceedings of the 12th International Conference on Computer Aided Verification, p.576-580, July 15-19, 2000
• 17: Abhik Roychoudhury , C. R. Ramakrishnan , I. V. Ramakrishnan, Justifying proofs using memo tables, Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.178-189, September 20-23, 2000, Montreal, Quebec, Canada [doi>10.1145/351268.351290]
• 18: 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
• 19: R. Sekar and P. Uppuluri. Synthesizing fast intrusion prevention/detection systems from high-level specifications. In USENIX Security Symposium, 1999.
• 20: 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
• 21: XSB. The XSB tabled logic programming system. Available from http://xsb.sourceforge.net.

INDEX TERMS

General Terms:
Security

Keywords:
information assurance, mobile code security