The security behaviors, provided by the contract and desired by the policy, can be represented as variant of automata (shown on Figure 2: Infinite Transitions Security Policies), where transitions corresponds to invocation of security-relevant actions. Thus, the operation of matching the midlet's claim with platform policy can be mapped into problems in automata theory.
PIM system on a phone has the ability to manage appointment books, contact directories, etc., in electronic form. A privacy conscious user may restrict network connectivity by stating a policy rule: "After PIM is opened no connections are allowed". This contract permits executing the javax.microedition.io.Connector.open() method only if the javax.microedition.pim.PIM.openPIMList() method was never called before.
The policy of an operator may only require that ``After PIM was accessed only secure connections can be opened''. This policy permits executing the javax.microedition.io.Connector.open(string url) method only if the started connection is a secure one i.e. url starts with ``https://''.
Figure 2: Infinite Transitions Security Policies
The first possible mechanism we consider to represent matching is language inclusion, such that given two automata A c and A p representing respectively the formal specification of a contract and of a policy, we have a match when the execution traces of the midlet described by A c are a subset of the acceptable traces for A p. To check this property we can complement the automaton of the policy, thus obtaining the set of traces disallowed by the policy and check its intersection with the traces of the contract. If the intersection is not empty, any behavior in it corresponds to a security violation.
The second mechanism we consider is the notion of simulation, such that we have a match when every security-relevant action invoked by A c can also be invoked by A p. In other words, every behavior of A c is also a behavior of A p. Simulation is a stronger notion than language inclusion as it requires that the policy allows the actions of the midlet's contract in a ``step-by-step'' fashion, whereas language inclusion looks at an execution trace as a whole.
While this idea of representing the security-digest as an automaton is almost a decade old, the practical realization has been hindered by a significant technical obstacle: we cannot use the naive encoding into automata for practical policies. Even the basic policies in Example 1 and Example 2 lead to automata with infinitely many transitions. For example an infinite automaton of Example 2 is shown on Figure 2.
Figure 3: AMT Examples
Figure 3 shows Example 1 and Example 2 represented in Automaton Modulo Theory (AMT).
Introduction to AMT is available on the following presentation AMT introduction.