A Formal Connection Between Security Automata and JML Annotations
Source: University of Twente
Security automata are a convenient way to describe security policies. Their typical use is to monitor the execution of an application, and to interrupt it as soon as the security policy is violated. However, run-time adherence checking is not always convenient. Instead, the authors aim at developing a technique to verify adherence to a security policy statically. To do this, they consider a security automaton as specification, and they generate JML annotations that inline the monitor - as a specification - into the application. They describe this translation and prove preservation of program behaviour, i.e., if monitoring does not reveal a security violation, the generated annotations are respected by the program.