Security-by-Contract using Automata Modulo Theory

Trust without control is a precarious solution to human nature. This belief has lead to many ways for guaranteeing secure software such as statically analyzing programs to check that they comply to the intended specifications which results in software certification. One problem with this approach is that the current systems can only accept all or nothing without knowing what the software is doing. Another way to complement is by run-time monitoring such that programs are checked during execution that they comply to security policy defined by the systems. The problem with this approach is the significant overhead which may not be desirable for some applications. This thesis describes a formalism, called Automata Modulo Theory, that allows us to have model of what programs do in more precise details thus giving semantics to certification. Automata Modulo Theory allows us to define very expressive policies with infinite cases while keeping the task of matching computationally tractable. This representation is suitable for formalizing systems with finitely many states but infinitely many transitions. Automata Modulo Theory consists of a formal model, two algorithms for matching the claims on the security behavior of a midlet (for short contract) with the desired security behavior of a platform (for short policy), and an algorithm for optimizing policy. The prototype implementations of Automata Modulo Theory matching using language inclusion and simulation have been built, and the results from our experience with the prototype implementations are also evaluated in this thesis.