A model-based approach to integrating security policies for embedded devices

ABSTRACT

Embedded devices like smartcards can now run multiple interacting applications. A particular challenge in this domain is to dynamically integrate diverse security policies. In this paper we show how a framework based on a concise formal model lets us securely customize a payment card equipped with a programmable chip. We present policy automata, a formal model of computations that grant or deny access to a resource. This model combines defeasible logic with state machines, representing complex policies as combinations of simpler modular policies. We use the model in a framework for specifying, merging and analyzing modular policies. This framework is implemented as Polaris, a tool which analyzes policy automata to reveal potential conflicts or redundancies, and compiles automata into Java Card applets.

REFERENCES

• 1: Rajeev Alur , Michael McDougall , Zijiang Yang, Exploiting Behavioral Hierarchy for Efficient Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.338-342, July 27-31, 2002
• 2: G. Antoniou , D. Billington , M. J. Maher, On the Analysis of Regulations using Defeasible Rules, Proceedings of the Thirty-second Annual Hawaii International Conference on System Sciences-Volume 6, p.6033, January 05-08, 1999
• 3: Grady Booch , James Rumbaugh , Ivar Jacobson, The Unified Modeling Language user guide, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1999
• 4: C.-B. Breunesse, N. Cataño, M. Huisman, and B. Jacobs. Formal methods for smart cards: an experience report. Technical Report NIII-R0316, University of Nijmegen, Department of Computer Science, Sept 2003.
• 5: G. Brewka, J. Dix, and K. Konolige. Nonmonotonic Reasoning: An Overview. CSLI Lecture Notes 73. CSLI Publications, Stanford, CA, 1997.
• 6: Marsha Chechik , Steve Easterbrook , Victor Petrovykh, Model-Checking over Multi-valued Logics, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.72-98, March 12-16, 2001
• 7: Edmund M. Clarke , Robert P. Kurshan, Computer-aided verification, IEEE Spectrum, v.33 n.6, p.61-67, June 1996 [doi>10.1109/6.499951]
• 8: Edmund M. Clarke , Jeannette M. Wing, Formal methods: state of the art and future directions, ACM Computing Surveys (CSUR), v.28 n.4, p.626-643, Dec. 1996 [doi>10.1145/242223.242257]
• 9: Nicodemos Damianou , Naranker Dulay , Emil Lupu , Morris Sloman, The Ponder Policy Specification Language, Proceedings of the International Workshop on Policies for Distributed Systems and Networks, p.18-38, January 29-31, 2001
• 10: Benjamin N. Grosof , Yannis Labrou , Hoi Y. Chan, A declarative approach to business rules in contracts: courteous logic programs in XML, Proceedings of the 1st ACM conference on Electronic commerce, p.68-77, November 03-05, 1999, Denver, Colorado, United States [doi>10.1145/336992.337010]
• 11: C. A. Gunter. Open APIs for embedded security. In L. Cardelli, editor, Proceedings of the European Conference on Object Oriented Programming, July 2003.
• 12: J. Y. Halpern and V. Weissman. Using first-order logic to reason about policies. In Proceedings of the 16th IEEE Computer Security Foundations Workshop, pages 187--201, 2003.
• 13: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 14: Allan Heydon , Mark W. Maimone , J. D. Tygar , Jeannette M. Wing , Amy Moormann Zaremski, Miro: Visual Specification of Security, IEEE Transactions on Software Engineering, v.16 n.10, p.1185-1197, October 1990 [doi>10.1109/32.60298]
• 15: J. A. Hoagland, R. Pandey, and K. Levitt. Security policy specification using a graphical approach. Technical Report CSE-98-3, University of California, Davis Department of Computer Science, 1998.
• 16: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 17: Emil C. Lupu , Morris Sloman, Conflicts in Policy-Based Distributed Systems Management, IEEE Transactions on Software Engineering, v.25 n.6, p.852-869, November 1999 [doi>10.1109/32.824414]
• 18: M. Lyubich. Die architekturen von SET mit der Java Card. In A. Bode and W. Karl, editors, ITG Fachbericht, APC 2001 Arbeitsplatzcomputer, 2001.
• 19: Michael J. Maher, Propositional defeasible logic has linear complexity, Theory and Practice of Logic Programming, v.1 n.6, p.691-711, November 2001 [doi>10.1017/S1471068401001168]
• 20: M. J. Maher, A. Rock, G. Antoniou, D. Billington, and T. Miller. Efficient defeasible reasoning systems. International Journal on Artificial Intelligence Tools, 10(4):483--501, 2001.
• 21: Mastercard and Visa. SET Secure Electronic Transaction Specification: Formal Protocol Definition, May 1997.
• 22: Donald Nute, Defeasible logic, Handbook of logic in artificial intelligence and logic programming (vol. 3): nonmonotonic reasoning and uncertain reasoning, Oxford University Press, Inc., New York, NY, 1994
• 23: 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]
• 24: Saheem Siddiqi , Joanne M. Atlee, A hybrid model for specifying features and detecting interactions, Computer Networks: The International Journal of Computer and Telecommunications Networking, v.32 n.4, p.471-485, April 2000 [doi>10.1016/S1389-1286(00)00011-6]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Smartcards

  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Languages (e.g., description, interconnection, definition); Domain-specific architectures
      D.2.4 Software/Program Verification
          Subjects: Model checking; Formal methods

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

General Terms:
Design, Theory, Verification

Keywords:
Java cards, model based design, policy integration, smartcards