|
|
Abstract:
A traditional way to ensure security of an application is to monitor its execution with a security automaton. In this talk, we show how this monitoring behaviour can be captured by appropriate JML annotations. We prove that the translation is correct, i.e., if and only if a monitored program can reach a ``halted'' states, the generated annotations will be violated. The core of the proof consists in showing that there exists a bisimulation between the states of the monitored program and the annotated program. The translation and correctness statement are formalised with the PVS theorem prover. We will also highlights certain parts of the specification, that allowed to modularise the proofs. This is work in progress, done in collaboration with Alejandro Tamalet from the Radboud University, Nijmegen, Netherlands. |