{"id":{"repo_id":"trento","oai_identifier":"oai:iris.unitn.it:11572/368352"},"canonical_url":"https://search.dev.ndltd.org/etd/trento/oai:iris.unitn.it:11572/368352","repository":{"repo_id":"trento","name":"Università degli Studi di Trento","base_url":"https://iris.unitn.it/oai/request"},"display":{"title":"Security-by-Contract using Automata Modulo Theory","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Siahaan, Ida Sri Rejeki"],"institution":"Università degli studi di Trento","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Massacci, Fabio"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2010,"date_issued":"2010","date_published":"2010","updated_at":"2026-07-24T05:04:24Z","subjects":["Settore INF/01 - Informatica"],"languages":["eng"],"rights":["info:eu-repo/semantics/openAccess","license:Tutti i diritti riservati (All rights reserved)"],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["10.15168/11572_368352"],"render_values":[{"text":"10.15168/11572_368352","href":"https://doi.org/10.15168/11572_368352","code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/11572/368352","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Siahaan, Ida Sri Rejeki","Massacci, Fabio"]},{"key":"dc:creator","label":"Author","values":["Siahaan, Ida Sri Rejeki"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2010"]},{"key":"dc:publisher","label":"Institution","values":["Università degli studi di Trento","place:TRENTO"]},{"key":"dc:relation","label":"Dc Relation","values":["firstpage:1","lastpage:112","numberofpages:112"]},{"key":"dc:type","label":"Dc Type","values":["info:eu-repo/semantics/doctoralThesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Settore INF/01 - Informatica"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["info:eu-repo/semantics/openAccess","license:Tutti i diritti riservati (All rights reserved)"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["https://hdl.handle.net/11572/368352","10.15168/11572_368352"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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."]},{"key":"dc:title","label":"Title","values":["Security-by-Contract using Automata Modulo Theory"]}]}],"canonical_facts":{"dc:contributor":["Siahaan, Ida Sri Rejeki","Massacci, Fabio"],"dc:creator":["Siahaan, Ida Sri Rejeki"],"dc:date":["2010"],"dc:description":["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."],"dc:identifier":["https://hdl.handle.net/11572/368352","10.15168/11572_368352"],"dc:language":["eng"],"dc:publisher":["Università degli studi di Trento","place:TRENTO"],"dc:relation":["firstpage:1","lastpage:112","numberofpages:112"],"dc:rights":["info:eu-repo/semantics/openAccess","license:Tutti i diritti riservati (All rights reserved)"],"dc:subject":["Settore INF/01 - Informatica"],"dc:title":["Security-by-Contract using Automata Modulo Theory"],"dc:type":["info:eu-repo/semantics/doctoralThesis"]},"updated_at":"2026-07-24T05:04:24Z"}