Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

5-2014

Abstract

An increasing number of ”smart” embedded devices are employed in our living environment nowadays. Unlike traditional computer systems, these devices are often physically accessible to the attackers. It is therefore almost impossible to guarantee that they are un-compromised, i.e., that indeed the devices are executing the intended software. In such a context, software-based attestation is deemed as a promising solution to validate their software integrity. It guarantees that the software running on the embedded devices are un-compromised without any hardware support. However, designing software-based attestation protocols are shown to be error-prone. In this work, we develop a framework for design and analysis of software-based attestation protocols. We first propose a generic attestation scheme that captures most existing software-based attestation protocols. After formalizing the security criteria for the generic scheme, we apply our analysis framework to several well-known software-based attestation protocols and report various potential vulnerabilities. To the best of our knowledge, this is the first practical analysis framework for software-based attestation protocols.

Keywords

Memory State, Data Memory, Memory Address, Malicious Code, Embed Device

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 16th International Conference on Formal Engineering Methods, ICFEM 2014, Luxembourg, November 3–5

First Page

284

Last Page

299

ISBN

9783319117362

Identifier

10.1007/978-3-319-11737-9_19

Publisher

IEEE

City or Country

Luxembourg

Additional URL

https://doi.org/10.1007/978-3-319-11737-9_19

Download

Share

COinS