Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
Sensoria Bibliography Site Testing Decision Procedures for Security-by-Contract
Nataliia Bielova, Fabio Massacci, Ida Sri Rejeki Siahaan
abstract:
The traditional realm of formal methods is the off-line verification of formal properties of hardware and software. In this paper we report a different approach that uses formal methods (namely the integration of automata modulo theory with decision procedures) on-the-fly, at the time an application is downloaded on a mobile application such as PDA or a smart phone. The idea behind security-by-contract is that a mobile application comes equipped with a signed contract describing the security relevant behavior of the application and such contract should be matched against the mobile platform policy. Both are specified as special kinds of automata and the operation is just an on-the-fly emptiness test over two automata modulo theories where edges are not just finite states of labels but rather expressions that can capture infinite transitions such as ``connect only to urls starting with https://''. The paper describe the prototype implementation, its integration with a state of the art decision solver (based on MathSAT and NuSMV) and the preliminary experiments that we have done for contract-policy matching.
