Security-by-Contract using Automata Modulo Theory

Siahaan, Ida Sri Rejeki (2010) Security-by-Contract using Automata Modulo Theory. PhD thesis, University of Trento.

PDF - Doctoral Thesis


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.

Item Type:Doctoral Thesis (PhD)
Doctoral School:Information and Communication Technology
PhD Cycle:XXII
Subjects:Area 01 - Scienze matematiche e informatiche > INF/01 INFORMATICA
Uncontrolled Keywords:language-based security, malicious code, security and privacy policies
Repository Staff approval on:03 May 2010 10:38

Repository Staff Only: item control page