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

Embedded devices like smart cards 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. Categories and Subject Descriptors: C.3 [Computer Systems Organization]: Special-Purpose and Application-Based Systems realtime and embedded systems, smartcards; D.2.4 [Software Engin...

• Type: Conference
• Year: 2004
• Where: EMSOFT
• Authors: Michael McDougall, Rajeev Alur, Carl A. Gunter
• Keywords: Concise Formal Model, EMSOFT 2004, Formal Model, Policy Automata