The Internet of Things (IoT) is shaped by the increasing number of low-cost Internet-connected embedded devices that are becoming ubiquitous in every aspect of modern life. With their cost-sensitive design, integrating hardware-based security mechanisms is undesirable. Therefore, securing these devices is a particularly difficult challenge, especially, due to their growing popularity as attack targets, via remote malware infestations. The vast majority of such devices are bare-metal, where they execute programs in fully-accessible and unprotected memories without any operating system and even without including any form of security. This is beside the fact that IoT operating systems offer little or no protection. This paper addresses this problem through the concept of a Security MicroVisor (SμV), which provides embedded devices that lack hardware-based memory protection units with memory isolation using software virtualisation and assembly-level code verification. More specifically, our contribution is two-fold. First, we propose SμV as a software-based memory isolation technique. We then formally verify the software architecture, written in C, to prove that it is memory-safe and crash-free. Second, on top of SμV, we build-remote attestation, a security service to detect malware-infected devices. We first describe the design of both SμV and remote attestation. Then, we highlight the implementation and the formal verification procedure. We evaluate the prototype implemented using an 8-bit AVR microcontroller that is widely used in IoT devices. Evaluation results show that SμV provides strong security guarantees while maintaining extremely low overhead in terms of memory footprint, performance, and power consumption. Furthermore, results show that a limited overhead incurred by the remote attestation protocol.

SμV - The Security MicroVisor: A Formally-Verified Software-Based Security Architecture for the Internet of Things / Ammar, Mahmoud; Crispo, Bruno; Jacobs, Bart; Hughes, Danny; Daniels, Wilfried. - In: IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING. - ISSN 1545-5971. - 2019, 16:9(2019), pp. 885-901. [10.1109/TDSC.2019.2928541]

SμV - The Security MicroVisor: A Formally-Verified Software-Based Security Architecture for the Internet of Things

Crispo,Bruno;
2019-01-01

Abstract

The Internet of Things (IoT) is shaped by the increasing number of low-cost Internet-connected embedded devices that are becoming ubiquitous in every aspect of modern life. With their cost-sensitive design, integrating hardware-based security mechanisms is undesirable. Therefore, securing these devices is a particularly difficult challenge, especially, due to their growing popularity as attack targets, via remote malware infestations. The vast majority of such devices are bare-metal, where they execute programs in fully-accessible and unprotected memories without any operating system and even without including any form of security. This is beside the fact that IoT operating systems offer little or no protection. This paper addresses this problem through the concept of a Security MicroVisor (SμV), which provides embedded devices that lack hardware-based memory protection units with memory isolation using software virtualisation and assembly-level code verification. More specifically, our contribution is two-fold. First, we propose SμV as a software-based memory isolation technique. We then formally verify the software architecture, written in C, to prove that it is memory-safe and crash-free. Second, on top of SμV, we build-remote attestation, a security service to detect malware-infected devices. We first describe the design of both SμV and remote attestation. Then, we highlight the implementation and the formal verification procedure. We evaluate the prototype implemented using an 8-bit AVR microcontroller that is widely used in IoT devices. Evaluation results show that SμV provides strong security guarantees while maintaining extremely low overhead in terms of memory footprint, performance, and power consumption. Furthermore, results show that a limited overhead incurred by the remote attestation protocol.
2019
9
Ammar, Mahmoud; Crispo, Bruno; Jacobs, Bart; Hughes, Danny; Daniels, Wilfried
SμV - The Security MicroVisor: A Formally-Verified Software-Based Security Architecture for the Internet of Things / Ammar, Mahmoud; Crispo, Bruno; Jacobs, Bart; Hughes, Danny; Daniels, Wilfried. - In: IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING. - ISSN 1545-5971. - 2019, 16:9(2019), pp. 885-901. [10.1109/TDSC.2019.2928541]
File in questo prodotto:
File Dimensione Formato  
smv_formal_last.pdf

Solo gestori archivio

Descrizione: first online
Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 575.93 kB
Formato Adobe PDF
575.93 kB Adobe PDF   Visualizza/Apri
SmuVThe_Security_MicroVisor_A_Formally-Verified_Software-Based_Security_Architecture_for_the_Internet_of_Things.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 1.73 MB
Formato Adobe PDF
1.73 MB 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/288993
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 28
  • ???jsp.display-item.citation.isi??? 18
  • OpenAlex ND
social impact