Embedded systems are increasingly pervasive, interdependent and in many cases critical to our every day life and safety. As such devices are more and more subject to attacks, new protection mechanisms are needed to provide the required resilience and dependency at low cost. Remote attestation (RA) is a software-hardware mechanism that securely checks the internal state of remote embedded devices. This protocol is executed by: (1) a prover that, given a secret key and its actual state, generates a result through an attestation algorithm; (2) a verifier that, given the key, the expected prover actual state, accepts or rejects the result through a verification algorithm. As the security of a protocol is only as good as its weakest link, a comprehensive validation of its security requirements is paramount. In this paper, we present a methodology for formal verification of hardware security requirements of RA architectures. First we perform an analysis and a comparison of three selected RA architectures, then we define security properties for RA systems and we verify them using a complete framework for formal verification.

Formal Verification of Embedded Systems for Remote Attestation / Cabodi, Gianpiero; Camurati, Paolo Enrico; Loiacono, Carmelo; Pipitone, Giovanni; Savarese, Francesco; Vendraminetto, Danilo. - In: WSEAS TRANSACTIONS ON COMPUTERS. - ISSN 1109-2750. - ELETTRONICO. - 14:(2015), pp. 760-769.

Formal Verification of Embedded Systems for Remote Attestation

CABODI, Gianpiero;CAMURATI, Paolo Enrico;LOIACONO, CARMELO;PIPITONE, GIOVANNI;SAVARESE, FRANCESCO;VENDRAMINETTO, DANILO
2015

Abstract

Embedded systems are increasingly pervasive, interdependent and in many cases critical to our every day life and safety. As such devices are more and more subject to attacks, new protection mechanisms are needed to provide the required resilience and dependency at low cost. Remote attestation (RA) is a software-hardware mechanism that securely checks the internal state of remote embedded devices. This protocol is executed by: (1) a prover that, given a secret key and its actual state, generates a result through an attestation algorithm; (2) a verifier that, given the key, the expected prover actual state, accepts or rejects the result through a verification algorithm. As the security of a protocol is only as good as its weakest link, a comprehensive validation of its security requirements is paramount. In this paper, we present a methodology for formal verification of hardware security requirements of RA architectures. First we perform an analysis and a comparison of three selected RA architectures, then we define security properties for RA systems and we verify them using a complete framework for formal verification.
2015
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/2614525
 Attenzione

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