The traditional realm of formal methods is the off-line verification of formal properties of hardware and software. In this technical report we describe 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. We also describe its integration with decision solver based on MathSAT and NuSMV, and the results of our experiments on matching. 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://"."

Inclusion Matching Implementation of Automata Modulo Theory (AMT) / Siahaan, Ida; Massacci, Fabio. - ELETTRONICO. - (2009), pp. 1-24.

Inclusion Matching Implementation of Automata Modulo Theory (AMT)

Siahaan, Ida;Massacci, Fabio
2009-01-01

Abstract

The traditional realm of formal methods is the off-line verification of formal properties of hardware and software. In this technical report we describe 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. We also describe its integration with decision solver based on MathSAT and NuSMV, and the results of our experiments on matching. 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://"."
2009
Trento
University of Trento - Dipartimento di Ingegneria e Scienza dell'Informazione
Inclusion Matching Implementation of Automata Modulo Theory (AMT) / Siahaan, Ida; Massacci, Fabio. - ELETTRONICO. - (2009), pp. 1-24.
Siahaan, Ida; Massacci, Fabio
File in questo prodotto:
File Dimensione Formato  
TR-16.pdf

accesso aperto

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 745.28 kB
Formato Adobe PDF
745.28 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/358205
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
  • OpenAlex ND
social impact