Polaris is a model-based design framework for creating flexible and modular access policies appropriate for embedded devices.
Policies in polaris are described as policy automata, a formal model of stateful access-control policies. Polaris checks these policies, looking for problems like conflicts and redundancies. Polaris also compiles the automata into Java Card applets suitable for a programmable credit card. This work is part of the OpEm project. The Daily Pennsylvian, a local student paper, interviewed some of the researchers about this work.
Michael McDougall, Rajeev Alur and Carl A. Gunter. "A Model-Based Approach to Integrating Security Policies for Embedded Devices". To appear at ACM EMSOFT, Italy, September 2004. Full paper - PS PDF
The Java files corressponding to the policy automata in the paper can be seen here: