In the past, formal verification of security properties of distributed applications has been mostly targeted to security protocols and generic security properties, like confidentiality and authenticity. At ESSOS 2010, Moebius et. al. presented an approach for developing Java applications with formally verified application-specific security properties. That method, however, is based on an interactive theorem prover, which is not automatic and requires considerable expertise. This paper shows that a similar result can be achieved in a fully automated way, using a different model-driven approach and state-of-the-art automated verification tools. The proposed method splits the verification problem into two independent sub-problems using compositional verification techniques and exploits one tool for analyzing the security protocol under active attackers and another tool for verifying the application logic. The same case study that was verified in the previous work is used here in order to show how the new approach works.

Automated Formal Verification of Application-specific Security Properties / BETTASSA COPET, Piergiuseppe; Sisto, Riccardo. - STAMPA. - 8364:(2014), pp. 45-59. (Intervento presentato al convegno Engineering Secure Software and Systems (ESSOS) tenutosi a Munich, Germany nel 26-28/2/2014) [10.1007/978-3-319-04897-0_4].

Automated Formal Verification of Application-specific Security Properties

BETTASSA COPET, PIERGIUSEPPE;SISTO, Riccardo
2014

Abstract

In the past, formal verification of security properties of distributed applications has been mostly targeted to security protocols and generic security properties, like confidentiality and authenticity. At ESSOS 2010, Moebius et. al. presented an approach for developing Java applications with formally verified application-specific security properties. That method, however, is based on an interactive theorem prover, which is not automatic and requires considerable expertise. This paper shows that a similar result can be achieved in a fully automated way, using a different model-driven approach and state-of-the-art automated verification tools. The proposed method splits the verification problem into two independent sub-problems using compositional verification techniques and exploits one tool for analyzing the security protocol under active attackers and another tool for verifying the application logic. The same case study that was verified in the previous work is used here in order to show how the new approach works.
2014
9783319048963
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/11583/2521101
 Attenzione

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