Simulating midlet's security claims with automata modulo theory

ABSTRACT

Model-carrying code and security-by-contract have proposed to augment mobile code with a claim on its security behavior that could be matched against a mobile platform policy before downloading the code. In order to capture realistic scenarios with potentially infinite transitions (e.g. "only connections to urls starting with https") we have proposed to represent those policies with the notion of Automata Modulo Theory (AMT), an extension of Buchi Automata (BA), with edges labeled by expressions in a decidable theory.

Our objective is the run-time matching of the mobile's platform policy against the midlet's security claims expressed as AMT. To this extent the use of on-the-fly product and emptiness test from automata theory may not be effective. In this paper we present an algorithm extending fair simulation between Büchi automata that can be more efficiently implemented.

REFERENCES

• 1: Jean Bacon, Toward Pervasive Computing, IEEE Pervasive Computing, v.1 n.2, p.84, April 2002 [doi>10.1109/MPRV.2002.1012341]
• 2: L. Bauer, J. Ligatti, and D. Walker. More enforceable security policies. In Found. of Comp. Security, 2002.
• 3: Lujo Bauer , Jay Ligatti , David Walker, Composing security policies with polymer, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 4: Nataliia Bielova , Marco Dalla Torre , Nicola Dragoni , Ida Siahaan, Matching Policies with Security Claims of Mobile Applications, Proceedings of the 2008 Third International Conference on Availability, Reliability and Security, p.128-135, March 04-07, 2008 [doi>10.1109/ARES.2008.96]
• 5: M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, S. Ranise, P.v. Rossum, and R. Sebastiani. Efficient satisfiability modulo theories via delayed theory combination. In K. Etessami and S.K. Rajamani, editors, Proc. of CAV?05, volume 3576 of LNCS, pages 335--349. Springer-Verlag, 2005.
• 6: J. R. Büchi. On a decision method in restricted second-order arithmetic. In E. Nagel et al., editor, Int. Cong. on Logic, Methodology and Philosophy of Science, pages 1--11. Stanford University Press, 1962.
• 7: N. Dragoni, F. Massacci, K. Naliuka, and I. Siahaan. Security-by-Contract: Toward a Semantics for Digital Signatures on Mobile Code. In Proc. of EuroPKI?07. Springer-Verlag, 2007a.
• 8: N. Dragoni, F. Massacci, C. Schaefer, T. Walter, and E. Vetillard. A security-by-contracts architecture for pervasive services. In Proc. of the 3rd Int. Workshop on Security, Privacy and Trust in Pervasive and Ubiquitous Computing. IEEE Press, 2007b.
• 9: U. Erlingsson. The Inlined Reference Monitor Approach to Security Policy Enforcement. Technical report 2003--1916, Department of Computer Science, Cornell University, 2003.
• 10: 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
• 11: Kousha Etessami , Thomas Wilke , Rebecca A. Schuller, Fair Simulation Relations, Parity Games, and State Space Reduction for Büchi Automata, SIAM Journal on Computing, v.34 n.5, p.1159-1175, 2005 [doi>10.1137/S0097539703420675]
• 12: Sankar Gurumurthy , Roderick Bloem , Fabio Somenzi, Fair Simulation Minimization, Proceedings of the 14th International Conference on Computer Aided Verification, p.610-624, July 27-31, 2002
• 13: Kevin W. Hamlen , Greg Morrisett , Fred B. Schneider, Certified In-lined Reference Monitoring on .NET, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada [doi>10.1145/1134744.1134748]
• 14: M. Hennessy , H. Lin, Symbolic bisimulations, Selected papers of the meeting on Mathematical foundations of programming semantics, p.353-389, February 1995, Univ. of Oxford, Oxford, United Kingdom
• 15: Thomas A. Henzinger , Orna Kupferman , Sriram K. Rajamani, Fair Simulation, Proceedings of the 8th International Conference on Concurrency Theory, p.273-287, July 01-04, 1997
• 16: Thomas A. Henzinger , Rupak Majumdar , Jean-François Raskin, A classification of symbolic transition systems, ACM Transactions on Computational Logic (TOCL), v.6 n.1, p.1-32, January 2005 [doi>10.1145/1042038.1042039]
• 17: G. J. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2004.
• 18: Marcin Jurdzinski, Small Progress Measures for Solving Parity Games, Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, p.290-301, February 01, 2000
• 19: F. Massacci and I. Siahaan. Matching midlet?s security claims with a platform security policy using automata modulo theory. In Proc. of The 12th Nordic Workshop on Secure IT Systems (NordSec?07), 2007.
• 20: 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]
• 21: George C. Necula , Peter Lee, Safe kernel extensions without run-time checking, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.229-243, October 29-November 01, 1996, Seattle, Washington, United States
• 22: Robert Nieuwenhuis , Albert Oliveras , Cesare Tinelli, Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T), Journal of the ACM (JACM), v.53 n.6, p.937-977, November 2006 [doi>10.1145/1217856.1217859]
• 23: S. Safra, On the complexity of omega -automata, Proceedings of the [Proceedings 1988] 29th Annual Symposium on Foundations of Computer Science, p.319-327, October 24-26, 1988 [doi>10.1109/SFCS.1988.21948]
• 24: 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]
• 25: Fred B. Schneider , J. Gregory Morrisett , Robert Harper, A Language-Based Approach to Security, Informatics - 10 Years Back. 10 Years Ahead., p.86-101, January 2001
• 26: R. Sekar , V.N. Venkatakrishnan , Samik Basu , Sandeep Bhatkar , Daniel C. DuVarney, Model-carrying code: a practical approach for safe execution of untrusted applications, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 27: Lieven Desmet , Wouter Joosen , Fabio Massacci , Katsiaryna Naliuka , Pieter Philippaerts , Frank Piessens , Dries Vanoverberghe, A flexible security architecture to support third-party applications on mobile devices, Proceedings of the 2007 ACM workshop on Computer security architecture, November 02-02, 2007, Fairfax, Virginia, USA [doi>10.1145/1314466.1314470]
• 28: M.Y. Vardi. Büchi complementation a 40-year saga. March 2006.
• 29: 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]
• 30: Bennet S. Yee, A sanctuary for mobile agents, Secure Internet programming: security issues for mobile and distributed objects, Springer-Verlag, London, 2001

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Additional Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms

General Terms:
Security, Theory, Verification

Keywords:
automata, mobile code, security policy