The notion of Security-by-Contract (SxC) was proposed in [DMNS07, BDM+09]. In SxC framework, a mobile code is augmented with a claim on its security behavior (an application's contract) that could be matched against a mobile platform's policy before downloading the code. Thus, a digital signature does not just certify the origin of the code but also bind together the code with a contract with the main goal to provide a semantics for digital signatures on mobile code. This framework is a step in the transition from trusted code to trustworthy code.

At development time the mobile code developers are responsible for providing a description of the security behavior that their code finally provides. Such a code may undergo a formal certification process by the developer’s own company, the smart card provider, a mobile phone operator, or any other third party for which the application has been developed. By using suitable techniques such as static analysis, monitor in-lining, or general theorem proving, the code is certified to comply with the developer’s contract. Technically, the contract can just be the package manifest of an application. Next, the code and the security claims are sealed together with the evidence for compliance (either a digital signature or a proof) and shipped as shown on Figure 1.

At deployment time, the target platform follows the workflow depicted in Figure 1. First, the correctness of the evidence of a code is checked. Such evidence can be a trusted signature or a proof that the code satisfies the contract (one can use Proof-Carrying-Code techniques to check it). When there is evidence that a contract is trustworthy, a platform checks that the claimed contract is compliant with the policy desired. If it is, then the application can be run without further ado. If it fails to comply, we may decide to still run the application, then we add a number of checks into the application so that any undesired behavior can be immediately stopped or corrected (in-line monitor).

Figure 1: Workflow and Mobile Code Components in Security-by-Contract

A contract is a formal specification of the behavior of an application for relevant security actions for example Virtual Machine API Calls or Web Messages. By signing the code the developer certifies that the code complies with the stated claims on its security-relevant behavior. We use the term policy to denote specification of the acceptable behavior of applications to be executed on a platform for what concerns relevant security actions. In this scenario compliant check can be reduced to checking whether the contract matches the policy.

Automata Modulo Theory (AMT) provides a formal model and algorithms for matching contract with policy for realistic security scenarios in SxC framework. AMT extends Buchi Automata with satisfiability-modulo-theory. AMT is suitable for formalizing systems with finitely many states but infinitely many transitions. AMT enables us to define expressive and customizable policies as a model for security-by-contract, by capturing the infinite transition into finite transitions labeled as expressions in suitable theories.

In this site we provide publications related to AMT and prototype implementations of matching using language inclusion and simulation.

This work has been partly supported by the following Projects: