Abstract

As security is an important concern in many areas, often security policies are defined that applications in these areas should obey. These policies can be conveniently formalized as security automata, which can be used to moni- tor applications at run time. However, this kind of validation is not always feasible or desirable, as it only reveals violations when they are already about to occur. Static verification is a way to check adherence at compile time. This requires Hoare logic style annotations to be provided, which is error-prone and time-consuming. Earlier work [6] provides a method that assists in this by translating security automata into JML annotations. However, this method only produces annotations for the methods included in the automaton, so-called core annotations. To be able to verify the correctness of the application’s usage patterns of the core methods, the security policy should be woven throughout the application: previous work [9] presents a method that propagates the core annotations to the methods (indirectly) invoking the core- annotated ones. This method, however, has severe limitations. We have developed a very precise algorithm that overcomes the most important limitations: Where the old algorithm cannot propagate the kind of annotations the translation produces, ours can, even when they are getting complex. Our algorithm supports all types of variables and considers branching, as opposed to the old one, which can only propagate static specification-only variables. We have applied our method to complex examples; where the old algorithm produced annotated Java code the static checker could not prove to be correct, our algorithm produced code the static checker could prove to be correct.

Additional Resources

1. The paper