Privacy-from-Birth: Protecting Sensed Data from Malicious Sensors with VERSA

TL;DR

This paper introduces VERSA, a formally verified architecture that guarantees sensed data privacy from the moment of analog-to-digital conversion, even if device software is compromised, enhancing IoT security.

Contribution

The paper formalizes the concept of Privacy-from-Birth (PfB) and presents VERSA, a hardware-assisted, formally verified system that protects sensed data from malicious software on resource-constrained IoT devices.

Findings

VERSA is formally verified for security guarantees.

PfB can be achieved affordably on IoT devices.

Experimental results confirm VERSA's effectiveness and efficiency.

Abstract

There are many well-known techniques to secure sensed data in IoT/CPS systems, e.g., by authenticating communication end-points, encrypting data before transmission, and obfuscating traffic patterns. Such techniques protect sensed data from external adversaries while assuming that the sensing device itself is secure. Meanwhile, both the scale and frequency of IoT-focused attacks are growing. This prompts a natural question: how to protect sensed data even if all software on the device is compromised? Ideally, in order to achieve this, sensed data must be protected from its genesis, i.e., from the time when a physical analog quantity is converted into its digital counterpart and becomes accessible to software. We refer to this property as PfB: Privacy-from-Birth. In this work, we formalize PfB and design Verified Remote Sensing Authorization (VERSA) -- a provably secure and formally verified architecture guaranteeing that only correct execution of expected and explicitly authorized software can access and manipulate sensing interfaces, specifically, General Purpose Input/Output (GPIO), which is the usual boundary between analog and digital worlds on IoT devices. This guarantee is obtained with minimal hardware support and holds even if all device software is compromised. VERSA ensures that malware can neither gain access to sensed data on the GPIO-mapped memory nor obtain any trace thereof. VERSA is formally verified and its open-sourced implementation targets resource-constrained IoT edge devices, commonly used for sensing. Experimental results show that PfB is both achievable and affordable for such devices.