BSc Presentation: Verifying Security Policies by using JML annotations

When: Aug. 5, 2011, 13:45-14:45

Where: Zi 5126

Who: Nils Klatter

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.

	Home > News and Events > Events
<< EEMCS (EWI) Home News and Events » Group Colloquium » Events » In the Media People Research Education Vacancies Intranet Contact	BSc Presentation: Verifying Security Policies by using JML annotations When: Aug. 5, 2011, 13:45-14:45 Where: Zi 5126 Who: Nils Klatter 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.