-
Towards Remotely Verifiable Software Integrity in Resource-Constrained IoT Devices
Authors:
Ivan De Oliveira Nunes,
Sashidhar Jakkamsetti,
Norrathep Rattanavipanon,
Gene Tsudik
Abstract:
Lower-end IoT devices typically have strict cost constraints that rule out usual security mechanisms available in general-purpose computers or higher-end devices. To secure low-end devices, various low-cost security architectures have been proposed for remote verification of their software state via integrity proofs. These proofs vary in terms of expressiveness, with simpler ones confirming correc…
▽ More
Lower-end IoT devices typically have strict cost constraints that rule out usual security mechanisms available in general-purpose computers or higher-end devices. To secure low-end devices, various low-cost security architectures have been proposed for remote verification of their software state via integrity proofs. These proofs vary in terms of expressiveness, with simpler ones confirming correct binary presence, while more expressive ones support verification of arbitrary code execution. This article provides a holistic and systematic treatment of this family of architectures. It also compares (qualitatively and quantitatively) the types of software integrity proofs, respective architectural support, and associated costs. Finally, we outline some research directions and emerging challenges.
△ Less
Submitted 10 January, 2024; v1 submitted 8 January, 2024;
originally announced January 2024.
-
Poster: Control-Flow Integrity in Low-end Embedded Devices
Authors:
Sashidhar Jakkamsetti,
Youngil Kim,
Andrew Searles,
Gene Tsudik
Abstract:
Embedded, smart, and IoT devices are increasingly popular in numerous everyday settings. Since lower-end devices have the most strict cost constraints, they tend to have few, if any, security features. This makes them attractive targets for exploits and malware. Prior research proposed various security architectures for enforcing security properties for resource-constrained devices, e.g., via Remo…
▽ More
Embedded, smart, and IoT devices are increasingly popular in numerous everyday settings. Since lower-end devices have the most strict cost constraints, they tend to have few, if any, security features. This makes them attractive targets for exploits and malware. Prior research proposed various security architectures for enforcing security properties for resource-constrained devices, e.g., via Remote Attestation (RA). Such techniques can (statically) verify software integrity of a remote device and detect compromise. However, run-time (dynamic) security, e.g., via Control-Flow Integrity (CFI), is hard to achieve. This work constructs an architecture that ensures integrity of software execution against run-time attacks, such as Return-Oriented Programming (ROP). It is built atop a recently proposed CASU -- a low-cost active Root-of-Trust (RoT) that guarantees software immutability. We extend CASU to support a shadow stack and a CFI monitor to mitigate run-time attacks. This gives some confidence that CFI can indeed be attained even on low-end devices, with minimal hardware overhead.
△ Less
Submitted 20 September, 2023; v1 submitted 19 September, 2023;
originally announced September 2023.
-
Caveat (IoT) Emptor: Towards Transparency of IoT Device Presence (Full Version)
Authors:
Sashidhar Jakkamsetti,
Youngil Kim,
Gene Tsudik
Abstract:
As many types of IoT devices worm their way into numerous settings and many aspects of our daily lives, awareness of their presence and functionality becomes a source of major concern. Hidden IoT devices can snoop (via sensing) on nearby unsuspecting users, and impact the environment where unaware users are present, via actuation. This prompts, respectively, privacy and security/safety issues. The…
▽ More
As many types of IoT devices worm their way into numerous settings and many aspects of our daily lives, awareness of their presence and functionality becomes a source of major concern. Hidden IoT devices can snoop (via sensing) on nearby unsuspecting users, and impact the environment where unaware users are present, via actuation. This prompts, respectively, privacy and security/safety issues. The dangers of hidden IoT devices have been recognized and prior research suggested some means of mitigation, mostly based on traffic analysis or using specialized hardware to uncover devices. While such approaches are partially effective, there is currently no comprehensive approach to IoT device transparency. Prompted in part by recent privacy regulations (GDPR and CCPA), this paper motivates and constructs a privacy-agile Root-of-Trust architecture for IoT devices, called PAISA: Privacy-Agile IoT Sensing and Actuation. It guarantees timely and secure announcements about IoT devices' presence and their capabilities. PAISA has two components: one on the IoT device that guarantees periodic announcements of its presence even if all device software is compromised, and the other that runs on the user device, which captures and processes announcements. Notably, PAISA requires no hardware modifications; it uses a popular off-the-shelf Trusted Execution Environment (TEE) -- ARM TrustZone. This work also comprises a fully functional (open-sourced) prototype implementation of PAISA, which includes: an IoT device that makes announcements via IEEE 802.11 WiFi beacons and an Android smartphone-based app that captures and processes announcements. Both security and performance of PAISA design and prototype are discussed.
△ Less
Submitted 8 September, 2023; v1 submitted 7 September, 2023;
originally announced September 2023.
-
PARseL: Towards a Verified Root-of-Trust over seL4
Authors:
Ivan De Oliveira Nunes,
Seoyeon Hwang,
Sashidhar Jakkamsetti,
Norrathep Rattanavipanon,
Gene Tsudik
Abstract:
Widespread adoption and growing popularity of embedded/IoT/CPS devices make them attractive attack targets. On low-to-mid-range devices, security features are typically few or none due to various constraints. Such devices are thus subject to malware-based compromise. One popular defensive measure is Remote Attestation (RA) which allows a trusted entity to determine the current software integrity o…
▽ More
Widespread adoption and growing popularity of embedded/IoT/CPS devices make them attractive attack targets. On low-to-mid-range devices, security features are typically few or none due to various constraints. Such devices are thus subject to malware-based compromise. One popular defensive measure is Remote Attestation (RA) which allows a trusted entity to determine the current software integrity of an untrusted remote device.
For higher-end devices, RA is achievable via secure hardware components. For low-end (bare metal) devices, minimalistic hybrid (hardware/software) RA is effective, which incurs some hardware modifications. That leaves certain mid-range devices (e.g., ARM Cortex-A family) equipped with standard hardware components, e.g., a memory management unit (MMU) and perhaps a secure boot facility. In this space, seL4 (a verified microkernel with guaranteed process isolation) is a promising platform for attaining RA. HYDRA made a first step towards this, albeit without achieving any verifiability or provable guarantees.
This paper picks up where HYDRA left off by constructing a PARseL architecture, that separates all user-dependent components from the TCB. This leads to much stronger isolation guarantees, based on seL4 alone, and facilitates formal verification. In PARseL, We use formal verification to obtain several security properties for the isolated RA TCB, including: memory safety, functional correctness, and secret independence. We implement PARseL in F* and specify/prove expected properties using Hoare logic. Next, we automatically translate the F* implementation to C using KaRaMeL, which preserves verified properties of PARseL C implementation (atop seL4). Finally, we instantiate and evaluate PARseL on a commodity platform -- a SabreLite embedded device.
△ Less
Submitted 23 August, 2023;
originally announced August 2023.
-
CASU: Compromise Avoidance via Secure Update for Low-end Embedded Systems
Authors:
Ivan De Oliveira Nunes,
Sashidhar Jakkamsetti,
Youngil Kim,
Gene Tsudik
Abstract:
Guaranteeing runtime integrity of embedded system software is an open problem. Trade-offs between security and other priorities (e.g., cost or performance) are inherent, and resolving them is both challenging and important. The proliferation of runtime attacks that introduce malicious code (e.g., by injection) into embedded devices has prompted a range of mitigation techniques. One popular approac…
▽ More
Guaranteeing runtime integrity of embedded system software is an open problem. Trade-offs between security and other priorities (e.g., cost or performance) are inherent, and resolving them is both challenging and important. The proliferation of runtime attacks that introduce malicious code (e.g., by injection) into embedded devices has prompted a range of mitigation techniques. One popular approach is Remote Attestation (RA), whereby a trusted entity (verifier) checks the current software state of an untrusted remote device (prover). RA yields a timely authenticated snapshot of prover state that verifier uses to decide whether an attack occurred.
Current RA schemes require verifier to explicitly initiate RA, based on some unclear criteria. Thus, in case of prover's compromise, verifier only learns about it late, upon the next RA instance. While sufficient for compromise detection, some applications would benefit from a more proactive, prevention-based approach. To this end, we construct CASU: Compromise Avoidance via Secure Updates. CASU is an inexpensive hardware/software co-design enforcing: (i) runtime software immutability, thus precluding any illegal software modification, and (ii) authenticated updates as the sole means of modifying software. In CASU, a successful RA instance serves as a proof of successful update, and continuous subsequent software integrity is implicit, due to the runtime immutability guarantee. This obviates the need for RA in between software updates and leads to unobtrusive integrity assurance with guarantees akin to those of prior RA techniques, with better overall performance.
△ Less
Submitted 2 September, 2022;
originally announced September 2022.
-
Privacy-from-Birth: Protecting Sensed Data from Malicious Sensors with VERSA
Authors:
Ivan De Oliveira Nunes,
Seoyeon Hwang,
Sashidhar Jakkamsetti,
Gene Tsudik
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…
▽ More
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.
△ Less
Submitted 5 May, 2022;
originally announced May 2022.
-
DIALED: Data Integrity Attestation for Low-end Embedded Devices
Authors:
Ivan De Oliveira Nunes,
Sashidhar Jakkamsetti,
Gene Tsudik
Abstract:
Verifying integrity of software execution in low-end micro-controller units (MCUs) is a well-known open problem. The central challenge is how to securely detect software exploits with minimal overhead, since these MCUs are designed for low cost, low energy and small size. Some recent work yielded inexpensive hardware/software co-designs for remotely verifying code and execution integrity. In parti…
▽ More
Verifying integrity of software execution in low-end micro-controller units (MCUs) is a well-known open problem. The central challenge is how to securely detect software exploits with minimal overhead, since these MCUs are designed for low cost, low energy and small size. Some recent work yielded inexpensive hardware/software co-designs for remotely verifying code and execution integrity. In particular, a means of detecting unauthorized code modifications and control-flow attacks were proposed, referred to as Remote Attestation (RA) and Control-Flow Attestation (CFA), respectively. Despite this progress, detection of data-only attacks remains elusive. Such attacks exploit software vulnerabilities to corrupt intermediate computation results stored in data memory, changing neither the program code nor its control flow. Motivated by lack of any current techniques (for low-end MCUs) that detect these attacks, in this paper we propose, implement and evaluate DIALED, the first Data-Flow Attestation (DFA) technique applicable to the most resource-constrained embedded devices (e.g., TI MSP430). DIALED works in tandem with a companion CFA scheme to detect all (currently known) types of runtime software exploits at fairly low cost.
△ Less
Submitted 23 March, 2021;
originally announced March 2021.
-
Tiny-CFA: A Minimalistic Approach for Control-Flow Attestation Using Verified Proofs of Execution
Authors:
Ivan De Oliveira Nunes,
Sashidhar Jakkamsetti,
Gene Tsudik
Abstract:
The design of tiny trust anchors has received significant attention over the past decade, to secure low-end MCU-s that cannot afford expensive security mechanisms. In particular, hardware/software (hybrid) co-designs offer low hardware cost, while retaining similar security guarantees as (more expensive) hardware-based techniques. Hybrid trust anchors support security services, such as remote atte…
▽ More
The design of tiny trust anchors has received significant attention over the past decade, to secure low-end MCU-s that cannot afford expensive security mechanisms. In particular, hardware/software (hybrid) co-designs offer low hardware cost, while retaining similar security guarantees as (more expensive) hardware-based techniques. Hybrid trust anchors support security services, such as remote attestation, proofs of software update/erasure/reset, proofs of remote software execution, in resource-constrained MCU-s, e.g., MSP430 and AVR AtMega32. Despite these advances, detection of control-flow attacks in low-end MCU-s remains a challenge, since hardware requirements of the cheapest related architectures are often more expensive than the MCU-s themselves. In this work, we tackle this challenge by designing Tiny-CFA - a control-flow attestation (CFA) technique with a single hardware requirement - the ability to generate proofs of remote software execution (PoX). In turn, PoX can be implemented very efficiently and securely in low-end MCU-s. Consequently, our design achieves the lowest hardware overhead of any CFA architecture (i.e., two orders of magnitude cheaper), while relying on a formally verified PoX architecture as its sole hardware requirement. With respect to runtime overhead, Tiny-CFA also achieves better performance than prior CFA techniques based on code instrumentation. We implement and evaluate Tiny-CFA, analyze its security, and demonstrate its practicality using real-world publicly available applications.
△ Less
Submitted 14 December, 2020; v1 submitted 14 November, 2020;
originally announced November 2020.
-
On the TOCTOU Problem in Remote Attestation
Authors:
Ivan De Oliveira Nunes,
Sashidhar Jakkamsetti,
Norrathep Rattanavipanon,
Gene Tsudik
Abstract:
We propose Remote Attestation with TOCTOU Avoidance (RATA): a provably secure approach to address the RA TOCTOU problem. With RATA, even malware that erases itself before execution of the next RA, can not hide its ephemeral presence. RATA targets hybrid RA architectures (implemented as Hardware/Software co-designs), which are aimed at low-end embedded devices. We present two alternative techniques…
▽ More
We propose Remote Attestation with TOCTOU Avoidance (RATA): a provably secure approach to address the RA TOCTOU problem. With RATA, even malware that erases itself before execution of the next RA, can not hide its ephemeral presence. RATA targets hybrid RA architectures (implemented as Hardware/Software co-designs), which are aimed at low-end embedded devices. We present two alternative techniques - RATAa and RATAb - suitable for devices with and without real-time clocks, respectively. Each is shown to be secure and accompanied by a publicly available and formally verified implementation. Our evaluation demonstrates low hardware overhead of both techniques. Compared with current RA architectures - that offer no TOCTOU protection - RATA incurs no extra runtime overhead. In fact, RATA substantially reduces computational costs of RA execution.
△ Less
Submitted 15 April, 2021; v1 submitted 8 May, 2020;
originally announced May 2020.