SpecificationGenerationExplanation

An alternative way to alleviate the burden of annotating code is to provide some higher-level specification formalism, which makes developing specifications less work. These high-level specifications are then automatically translated into to more basic program annotations.

The earlier work on security requirements reported in Deliverable 1.2 (MobiusConsortium06A) suggested that so-called midlet navigation graphs (Cre06) could be such a higher-level specification formalism. Such graphs are essentially a form of security automata, and the existing industry standard for testing MIDP applications (PR08) already prescribes the use of a similar, albeit completely informal, notion of "flow diagram".

Security automata are a convenient way to describe security policies. Traditionally they are used to monitor an application at runtime, and to interrupt it as soon as it violates the security policy. However, in our setting of PCC, we would like to use security automata as JML specifications, and verify adherence to them statically. The JML annotations effectively inline the monitor in the application.

The translation of security automata into program annotations is not trivial, and there is the danger that the semantics of the annotations is not equivalent to the effect of runtime monitoring.

The translation from security automata to program annotations is defined in several steps:

• complete the security automata, adding a special trap state that should not be reached (whereas partial automata, describing only the allowed transitions are sufficient for monitoring);
• generate special set-annotations at the level of method specifications, capturing the behavior of the security automata, together with an invariant stating that the error state should not be reached; and
• inline the annotations into the method body.

We have developed a generic program semantics that is instantiated for monitoring and run-time annotation checking. We prove that every translation step preserves the program behavior. In particular this means that monitoring will not find a security violation iff run-time annotation checking will not find any annotation violation (provided that earlier existing annotations are not violated either).

A full description of the translation, its formalisation and the correctness proof are available in (HT08). The correctness proofs revealed several subtleties that have to be considered in the algorithm, and necessary assumptions about program behavior.

Using an annotation propagation algorithm (as in (PBB+04)) the generated annotations give rise to pre- and postcondition annotations in the whole application, that can be verified statically.

In the simplest form of security automata, each edge corresponds to some unique event, typically some method call, but for convenient specifications one can allow richer languages for decorating edges. In (PR08) we define suitable notions of refinement for MIDP navigation graphs, and propose a translation of these to JML annotations.

We have also adapted AutoJML, a tool we developed earlier in Nijmegen (HO03) to generate JML annotations from automata-like specifications, to cope with richer forms of automata. In (PS07) this has been used to generate JML annotations to verify that the MIDP-SSH implementation is correct with respect to a formal specification of the SSH protocol. Here our formal specification probably goes into much more detail than one would typically give in a security automaton.

Version: 2 Time: Fri Mar 28 13:53:03 2008 Author: dcochran (dcochran) IP: 193.1.132.32