Abstract

Security policies are an intuitive way to express security properties of a program. This makes them easy to use. Usually security policies are expressed as security automata and used by a monitor, which checks the compliance of the program to the security policy at run time. If the program violates the security policy, the program is halted. Because this behavior is not always desirable, Huisman and Tamalet introduced a method to check the adherence of Java programs to a security policy statically without executing the program. The method translates a security automaton into JML annotations that inline the monitor. However, this method only supports static Java classes. Concretely, this assignment extends the supported Java language to support non-static classes and methods. Furthermore, it adapts the notation of the security automaton such that an automaton transition can be associated to the execution of a method of a nonstatic classes. This enables the monitoring of non-static classes with a single monitor. The assignment also adapts the translation method of Huisman and Tamalet to inline the extended monitor in the Java code.

Additional Resources

1. The paper