Distributed Dynamic Enforcement with Service Automata
Dynamic enforcement is a popular technique for ensuring the compliance of a given program with given security requirements. A dynamic enforcement mechanism monitors the execution of the program and applies countermeasures - such as terminating the program - whenever the program is about to violate the security requirements. For soundly enforcing security requirements on distributed programs, an enforcement mechanism may require information that is distributed as well and, hence, not available for the enforcement mechanism at one location.
In this talk, we present Service Automata, a dynamic enforcement mechanism for distributed programs. Service Automata have a modular architecture that supports decentralized but coordinated enforcement. We formalized Service Automata in the process algebra CSP. This formal model is parametric in a security policy and a distributed program. It supports stepwise instantiation of the parameters and enables formal soundness proofs. We implemented Service Automata for Java programs, with which we demonstrate the practical feasibility of Service Automata for concrete programs. We give an overview over the formal model and the implementation, focusing on the stepwise instantiation of Service Automata as well as on how Service Automata and target programs are composed.
The talk presents joint work with Jinwei Hu, Heiko Mantel, and Barbara Sprick.