Ivan Oliveira Nunes

dblp:173/5375 · also Ivan De Oliveira Nunes · DBLP profile ↗
← Back
35ranked-venue papers
18as first author
23since 2021 · last 2026
0000-0003-3486-6550ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Security and privacy · 16 · 6 first-author · 13 since 2021Systems, architecture and hardware · 12 · 7 first-author · 9 since 2021Computer networks · 7 · 5 first-author · 1 since 2021Software engineering, systems software and programming languages · 1 · 1 first-author · 1 since 2021
YearPublicationVenuePosition
2026 RESPEC-CFA: Representation-Aware Speculative Control Flow Attestation
Liam Tyler, Adam Caulfield, Ivan Oliveira Nunes
ACNS (3)3
2025 RAP-Track: Efficient Control Flow Attestation via Parallel Tracking in Commodity MCUs
abstract
Control Flow Attestation (CFA) has emerged as an important security service to enable remote verification of control flow paths in safety-critical embedded systems. However, current CFA for commodity devices suffers performance penalties due to code instrumentation and frequent context switches required to securely log control flow paths at runtime. Our work introduces RAP-Track, a technique leveraging commodity hardware extensions, namely Micro Trace Buffer and Data Watchpoint and Trace Unit, to track control flow paths in parallel with the execution of the attested program, thus avoiding aforementioned overheads present in state-of-the-art CFA. Our evaluation (based on an open-source prototype of RAP-Track) demonstrates substantial performance gains, enhancing practicality and security of CFA.
Antonio Joia, Adam Caulfield, Ivan Oliveira Nunes
DAC3
2025 SoK: Integrity, Attestation, and Auditing of Program Execution
abstract
This paper provides a systematic exploration of Control Flow Integrity (CFI) and Control Flow Attestation (CFA) mechanisms, examining their differences and relationships. It addresses crucial questions about the goals, assumptions, features, and design spaces of CFI and CFA, including their potential coexistence on the same platform. Through a comprehensive review of existing defenses, this paper positions CFI and CFA within the broader landscape of runtime defenses, critically evaluating their strengths, limitations, and trade-offs. The findings emphasize the importance of further research to bridge the gaps in CFI and CFA and thus advance the field of runtime defenses.
Mahmoud Ammar, Adam Caulfield, Ivan Oliveira Nunes
SP3
2025 PEARTS: Provable Execution in Real-Time Embedded Systems
abstract
Embedded devices are increasingly ubiquitous and vital, often supporting safety-critical functions. However, due to strict cost and energy constraints, they are typically implemented with Micro-Controller Units (MCUs) that lack advanced architectural security features. Within this space, recent efforts have created low-cost architectures capable of generating Proofs of Execution (PoX) of software on potentially compromised MCUs. This capability can ensure the integrity of sensor data from the outset, by binding sensed results to an unforgeable cryptographic proof of execution on edge sensor MCUs. However, the security of existing PoX requires the proven execution to occur atomically (i.e., uninterrupted). This requirement precludes the application of PoX to (1) time-shared systems, and (2) applications with real-time constraints, creating a direct conflict between execution integrity and the real-time availability needs of several embedded system uses. In this paper, we formulate a new security goal called Real-Time Proof of Execution (RT-PoX) that retains the integrity guarantees of classic PoX while enabling its application to existing real-time systems. This is achieved by relaxing the atomicity requirement of PoX while dispatching interference attempts from other potentially malicious tasks (or compromised operating systems) executing on the same device. To realize the RT-PoX goal, we develop Provable Execution Architecture for Real-Time Systems (PEARTS). To the best of our knowledge, PEARTS is the first PoX system that can be directly deployed alongside a commodity embedded real-time operating system (FreeRTOS). This enables both real-time scheduling and execution integrity guarantees on commodity MCUs. To showcase this capability, we develop a PEARTS open-source prototype atop FreeRTOS on a single-core ARM Cortex- M33processor. Based on this prototype, we evaluate and report on PEARTS security and (modest) overheads.
Antonio Joia, Norrathep Rattanavipanon, Ivan Oliveira Nunes
SP3
2025 Run-time Attestation and Auditing: The Verifier's Perspective
abstract
In run-time attestation schemes, including Control Flow Attestation (CFA) and Data Flow Attestation (DFA), a remote Verifier (Vrf) requests a potentially compromised Prover device (Prv) to generate evidence of its execution control flow path (in CFA) and optionally execution data inputs (in DFA). Recent advances in this space also guarantee that Vrf eventually receives run-time evidence from Prv, even when Prv is fully compromised. Reliable delivery, in theory, enables run-time auditing in addition to attestation, allowing Vrf to examine run-time compromise traces to pinpoint/remediate attack root causes. However, Vrf's perspective in this security service remains unexplored, with most prior work focusing on the secure generation of authentic run-time evidence on Prv.
Adam Caulfield, Norrathep Rattanavipanon, Ivan Oliveira Nunes
WISEC3
2025 SLAPP: Poisoning Prevention in Federated Learning and Differential Privacy via Stateful Proofs of Execution
abstract
The rise of IoT-driven distributed data analytics, coupled with increasing privacy concerns, has led to a demand for effective privacy-preserving and federated data collection/model training mechanisms. In response, approaches such as Federated Learning (FL) and Local Differential Privacy (LDP) have been proposed and attracted much attention over the past few years. However, they still share the common limitation of being vulnerable to poisoning attacks wherein adversaries compromising edge devices feed forged (a.k.a. “poisoned”) data to aggregation back-ends, undermining the integrity of FL/LDP results. In this work, we propose a system-level approach to remedy this issue based on a novel security notion of Proofs of Stateful Execution ($\mathsf {PoSX}$) for IoT/embedded devices’ software. To realize the$\mathsf {PoSX}$concept, we design$\mathsf {SLAPP}$: a System-Level Approach for Poisoning Prevention.$\mathsf {SLAPP}$leverages commodity security features of embedded devices – in particular ARM TrustZone-M security extensions – to verifiably bind raw sensed data to their correct usage as part of FL/LDP edge device routines. As a consequence, it offers robust security guarantees against poisoning. Our evaluation, based on real-world prototypes featuring multiple cryptographic primitives and data collection schemes, showcases$\mathsf {SLAPP}$’s security and low overhead.
Norrathep Rattanavipanon, Ivan Oliveira Nunes
IEEE Trans. Inf. Forensics Secur.2
2024 TRACES: TEE-based Runtime Auditing for Commodity Embedded Systems
abstract
Control Flow Attestation (CFA) offers a means to detect control flow hijacking attacks on remote devices, enabling verification of their runtime trustworthiness. CFA generates a trace (CFLog) containing the destination of all branching instructions executed. This allows a remote Verifier (Vrf) to inspect the execution control flow on a potentially compromised Prover (Prv) before trusting that a value/action was correctly produced/performed by Prv. However, while CFA can be used to detect runtime compromises, it cannot guarantee the eventual delivery of the execution evidence (CFLog) to Vrf. In turn, a compromised Prv may refuse to send CFLogto Vrf, preventing its analysis to determine the exploit’s root cause and appropriate remediation actions.In this work, we propose TRACES: TEE-based Runtime Auditing for Commodity Embedded Systems. TRACES guarantees reliable delivery of periodic runtime reports even when Prv is compromised. This enables secure runtime auditing in addition to best-effort delivery of evidence in CFA. TRACES also supports a guaranteed remediation phase, triggered upon compromise detection to ensure that identified runtime vulnerabilities can be reliably patched. To the best of our knowledge, TRACES is the first system to provide this functionality on commodity devices (i.e., without requiring custom hardware modifications). To that end, TRACES leverages support from the ARM TrustZone-M Trusted Execution Environment (TEE). To assess practicality, we implement and evaluate a fully functional (open-source) prototype of TRACES atop the commodity ARM Cortex-M33 micro-controller unit.
Adam Caulfield, Antonio Joia, Norrathep Rattanavipanon, Ivan Oliveira Nunes
ACSAC4
2024 SpecCFA: Enhancing Control Flow Attestation/Auditing via Application-Aware Sub-Path Speculation
abstract
At the edge of modern cyber-physical systems, Micro-Controller Units (MCUs) are responsible for safety-critical sensing/actuation. However, MCU cost constraints rule out the usual security mechanisms of general-purpose computers. Thus, various low-cost security architectures have been proposed to remotely verify MCU software integrity. Control Flow Attestation (CFA) enables a Verifier $(\mathcal{V}{\text{rf}})$ to remotely assess the run-time behavior of a prover MCU $(\mathcal{P}rv)$, generating an authenticated trace of all of $\mathcal{P}{\text{rv}}$ control flow transfers (CFLog). Further, Control Flow Auditing architectures augment CFA by guaranteeing the delivery of evidence to $\mathcal{V}{\text{rf}}$.Unfortunately, a limitation of existing CFA lies in the cost to store and transmit CFLog, as even simple MCU software may generate large traces. Given these issues, prior work has proposed static (context-insensitive) optimizations. However, they do not support configurable program-specific optimizations. In this work, we note that programs may produce unique predictable control flow sub-paths and argue that program-specific predictability can be leveraged to dynamically optimize CFA while retaining all security guarantees. Therefore, we propose SpecCFA: an approach for dynamic sub-path speculation in CFA. SpecCFA allows $\mathcal{V}{\text{rf}}$ to securely speculate on likely control flow sub-paths for each attested program. At run-time, when a sub-path in CFLogmatches a pre-defined speculation, the entire sub-path is replaced by a reserved symbol. SpecCFA can speculate on multiple variable-length control flow sub-paths simultaneously. We implement SpecCFA atop two open-source control flow auditing architectures: one based on a custom hardware design [1] and one based on a commodity Trusted Execution Environment (ARM TrustZone-M) [2]. In both cases, SpecCFA significantly lowers storage/performance costs that are critical to resource-constrained MCUs.
Adam Caulfield, Liam Tyler, Ivan Oliveira Nunes
ACSAC3
2024 Untrusted Code Compartmentalization for Bare Metal Embedded Devices
abstract
Micro-controller units (MCUs) implement the de facto interface between the physical and digital worlds. As a consequence, they appear in a variety of sensing/actuation applications from smart personal spaces to complex industrial control systems and safety-critical medical equipment. While many of these devices perform safety- and time-critical tasks, they often lack support for security features compatible with their importance to overall system functions. This lack of architectural support leaves them vulnerable to run-time attacks that can remotely alter their intended behavior, with potentially catastrophic consequences. In particular, we note that, MCU software often includes untrusted third-party libraries (some of them closed-source) that are blindly used within MCU programs, without proper isolation from the rest of the system. In turn, a single vulnerability (or intentional backdoor) in one such third-party software can often compromise the entire MCU software state. In this article, we tackle this problem by proposing, demonstrating security, and formally verifying the implementation of UCCA: anUntrustedCodeCompartmentArchitecture. UCCA provides flexible hardware-enforced isolation of untrusted code sections (e.g., third-party software modules) in resource-constrained and time-critical MCUs. To demonstrate UCCA’s practicality, we implement an open-source version of the design on a real resource-constrained MCU: the well-known TI MSP430. Our evaluation shows that UCCA incurs little overhead and is affordable even to lowest-end MCUs, requiring significantly less overhead and assumptions than the prior related work.
Liam Tyler, Ivan Oliveira Nunes
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.2
2023 Oblivious Extractors and Improved Security in Biometric-Based Authentication Systems
Ivan Oliveira Nunes, Peter Rindal, Maliheh Shirvanian
ESORICS (1)1
2023 $\mathcal{D}\mathsf{iCA}$: A Hardware-Software Co-Design for Differential Check-Pointing in Intermittently Powered Devices
abstract
Intermittently powered devices rely on opportunistic energy-harvesting to function, leading to recurrent power interruptions. Therefore, check-pointing techniques are crucial for reliable device operation. Current strategies involve storing snapshots of the device's state at specific intervals or upon events. Time-based check-pointing takes check-points at regular intervals, providing a basic level of fault tolerance. However, frequent check-point generation can lead to excessive/unnecessary energy consumption. Event-based check-pointing, on the other hand, captures the device's state only upon specific trigger events or conditions. While the latter reduces energy usage, accurately detecting trigger events and determining optimal triggers can be challenging. Finally, differential check-pointing selectively stores state changes made since the last check-point, reducing storage and energy requirements for the check-point generation. However, current differential check-pointing strategies rely on software instrumentation, introducing challenges related to the precise tracking of modifications in volatile memory as well as added energy consumption (due to instrumentation overhead). This paper introduces$\mathcal{D}\mathsf{iCA}$, a proposal for a hardware/software co-design to create differential check-points in intermittent devices.$\mathcal{D}\mathsf{iCA}$leverages an affordable hardware module that simplifies the check-pointing process, reducing the check-point generation time and energy consumption. This hardware module continuously monitors volatile memory, efficiently tracking modifications and determining optimal check-point times. To minimize energy waste, the module dynamically estimates the energy required to create and store the check-point based on tracked memory modifications, triggering the check-pointing routine optimally via a non-maskable interrupt. Experimental results show the cost-effectiveness and energy efficiency of$\mathcal{D}\mathsf{iCA}$, enabling extended application activity cycles in intermittently powered embedded devices.
Antonio Joia, Adam Caulfield, Chistabelle Alvares, Ivan Oliveira Nunes
ICCAD4
2023 $\mathcal{P}\text{ARseL}$: Towards a Verified Root-of-Trust Over seL4
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$(\mathcal{R}\mathrm{A})$which allows a trusted entity to determine the current software integrity of an untrusted remote device. For higher-end devices,$\mathcal{R}\mathrm{A}$is achievable via secure hardware components. For low-end (bare metal) devices, minimalistic hybrid (hardware/-software)$\mathcal{R}\mathrm{A}$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$\mathcal{R}\mathrm{A}$. HYDRA [1] 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$\mathcal{P}\text{ARseL}$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$\mathcal{P}\text{ARseL}$, We use formal verification to obtain several security properties for the isolated$\mathcal{R}\mathrm{A}$TCB, including: memory safety, functional correctness, and secret independence. We implement$\mathcal{P}\text{ARseL}$in$F^{\ast}$and specify/prove expected properties using Hoare logic. Next, we automatically translate the$F^{\ast}$implementation to C using KaRaM eL, which preserves verified properties of$\mathcal{P}\text{ARseL}$, C implementation (atop seL4). Finally, we instantiate and evaluate$\mathcal{P}\text{ARseL}$on a commodity platform - a SabreLite embedded device.
Ivan Oliveira Nunes, Seoyeon Hwang, Sashidhar Jakkamsetti, Norrathep Rattanavipanon, Gene Tsudik
ICCAD1
2023 ISC-FLAT: On the Conflict Between Control Flow Attestation and Real-Time Operations
abstract
The wide adoption of IoT gadgets and CyberPhysical Systems (CPS) makes embedded devices increasingly important. While some of these devices perform mission-critical tasks, they are usually implemented using Micro-Controller Units (MCUs) that lack security mechanisms on par with those available to general-purpose computers, making them more susceptible to remote exploits that could corrupt their software integrity. Motivated by this problem, prior work has proposed techniques to remotely assess the trustworthiness of embedded MCU software. Among them, Control Flow Attestation (CFA) enables remote detection of runtime abuses that illegally modify the program’s control flow during execution (e.g., control flow hijacking and code reuse attacks). Despite these advances, current CFA methods share a fundamental limitation: they preclude interrupts during the execution of the software operation being attested. Simply put, existing CFA techniques are insecure unless interrupts are disabled on the MCU. On the other hand, we argue that the lack of interruptability can obscure CFA usefulness, as most embedded applications depend on interrupts to process asynchronous events in real-time. To address this limitation, we propose Interrupt-Safe Control Flow Attestation (ISC-FLAT): a CFA technique that is compatible with existing MCUs (i.e., does not require hardware changes) and enables interrupt handling without compromising the authenticity of CFA reports. Similar to other CFA techniques that do not require customized hardware modifications, ISC-FLAT leverages a Trusted Execution Environment (TEE) (in particular, our prototype is built on ARM TrustZone-M) to securely generate unforgeable CFA reports without precluding applications from processing interrupts. We implement a fully functional ISC-FLAT prototype on the ARM Cortex-M33 MCU and demonstrate that it incurs minimal runtime overhead when compared to existing TEE-based CFA methods that do not support interrupts.
Antonio Joia, Ivan Oliveira Nunes
RTAS2
2023 ACFA: Secure Runtime Auditing & Guaranteed Device Healing via Active Control Flow Attestation
Adam Caulfield, Norrathep Rattanavipanon, Ivan Oliveira Nunes
USENIX Security Symposium3
2022 ASAP: reconciling asynchronous real-time operations and proofs of execution in simple embedded systems
abstract
Embedded devices are increasingly ubiquitous and their importance is hard to overestimate. While they often support safety-critical functions (e.g., in medical devices and sensor-alarm combinations), they are usually implemented under strict cost/energy budgets, using low-end microcontroller units (MCUs) that lack sophisticated security mechanisms. Motivated by this issue, recent work developed architectures capable of generating Proofs of Execution (PoX) for the correct/expected software in potentially compromised low-end MCUs. In practice, this capability can be leveraged to provide "integrity from birth" to sensor data, by binding the sensed results/outputs to an unforgeable cryptographic proof of execution of the expected sensing process. Despite this significant progress, current PoX schemes for low-end MCUs ignore the real-time needs of many applications. In particular, security of current PoX schemes precludes any interrupts during the execution being proved. We argue that lack of asynchronous capabilities (i.e., interrupts within PoX) can obscure PoX usefulness, as several applications require processing real-time and asynchronous events. To bridge this gap, we propose, implement, and evaluate an Architecture for Secure Asynchronous Processing in PoX (ASAP). ASAP is secure under full software compromise, enables asynchronous PoX, and incurs less hardware overhead than prior work.
Adam Caulfield, Norrathep Rattanavipanon, Ivan Oliveira Nunes
DAC3
2022 CASU: Compromise Avoidance via Secure Update for Low-End Embedded Systems
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 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.
Ivan Oliveira Nunes, Sashidhar Jakkamsetti, Gene Tsudik
ICCAD1
2022 Privacy-from-Birth: Protecting Sensed Data from Malicious Sensors with VERSA
abstract
With the growing popularity of the Internet-of-Things (IoT), massive numbers of specialized devices are deployed worldwide, in many everyday settings, including homes, offices, vehicles, public spaces, and factories. Such devices usually perform sensing and/or actuation. Many of them handle sensitive and personal data. If left unprotected, ambient sensing (e.g., of temperature, motion, audio, or video) can leak very private information. At the same time, some IoT devices use low-end computing platforms with few (or no) security features.There are many well-known techniques to secure sensed data, 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 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.
Ivan Oliveira Nunes, Seoyeon Hwang, Sashidhar Jakkamsetti, Gene Tsudik
SP1
2022 GAROTA: Generalized Active Root-Of-Trust Architecture (for Tiny Embedded Devices)
Esmerald Aliaj, Ivan Oliveira Nunes, Gene Tsudik
USENIX Security Symposium2
2021 On the TOCTOU Problem in Remote Attestation
abstract
Much attention has been devoted to verifying software integrity of remote embedded (IoT) devices. Many techniques, with different assumptions and security guarantees, have been proposed under the common umbrella of so-called Remote Attestation (RA). Aside from executable's integrity verification, RA serves as a foundation for many security services, such as proofs of memory erasure, system reset, software update, and verification of runtime properties. Prior RA techniques verify the remote device's binary at the time when RA functionality is executed, thus providing no information about the device's binary before current RA execution or between consecutive RA executions. This implies that presence of transient malware (in the form of modified binary) may be undetected. In other words, if transient malware infects a device (by modifying its binary), performs its nefarious tasks, and erases itself before the next attestation, its temporary presence will not be detected. This important problem, called Time-Of-Check-Time-Of-Use ( TOCTOU ), is well-known in the research literature and remains unaddressed in the context of hybrid RA.
Ivan Oliveira Nunes, Sashidhar Jakkamsetti, Norrathep Rattanavipanon, Gene Tsudik
CCS1
2021 DIALED: Data Integrity Attestation for Low-end Embedded Devices
abstract
Verifying integrity of software execution in low-end microcontroller 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 (ℛA) 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 (CFA) 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.
Ivan Oliveira Nunes, Sashidhar Jakkamsetti, Gene Tsudik
DAC1
2021 Tiny-CFA: Minimalistic Control-Flow Attestation Using Verified Proofs of Execution
abstract
The design of tiny trust anchors attracted much attention over the past decade, to secure low-end MCU-s that cannot afford more 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, and 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 for the cheapest mitigation techniques 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 technique, while relying on a formally verified PoX 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.
Ivan Oliveira Nunes, Sashidhar Jakkamsetti, Gene Tsudik
DATE1
2021 On the Root of Trust Identification Problem
abstract
Trusted Execution Environments (TEEs) are becoming ubiquitous and are currently used in many security applications: from personal IoT gadgets to banking and databases. Prominent examples of such architectures are Intel SGX, ARM TrustZone, and Trusted Platform Modules (TPMs). A typical TEE relies on a dynamic Root of Trust (RoT) to provide security services such as code/data confidentiality and integrity, isolated secure software execution, remote attestation, and sensor auditing. Despite their usefulness, there is currently no secure means to determine whether a given security service or task is being performed by the particular RoT within a specific physical device. We refer to this as the Root of Trust Identification (RTI) problem and discuss how it inhibits security for applications such as sensing and actuation.
Ivan Oliveira Nunes, Xuhua Ding, Gene Tsudik
IPSN1
2021 Delegated attestation: scalable remote attestation of commodity CPS by blending proofs of execution with software attestation
abstract
Remote Attestation (RA) is an interaction between a trusted verifier (Vrf) and one or more remote and potentially compromised devices (provers or Prv-s) that allow the former to measure the software state of the latter. RA is particularly relevant to safety-critical cyber-physical systems (CPS) where a set of low-end micro-controllers (MCUs), operate under the control of a remote and more powerful controller. In such cases, RA is an effective and relatively efficient means to detect software compromise, e.g., malware infections, on these low-end MCUs that cannot support expensive security mechanisms.
Mahmoud Ammar, Bruno Crispo, Ivan Oliveira Nunes, Gene Tsudik
WISEC3
2020 APEX: A Verified Architecture for Proofs of Execution on Remote Devices under Full Software Compromise
Ivan Oliveira Nunes, Karim M. El Defrawy, Norrathep Rattanavipanon, Gene Tsudik
USENIX Security Symposium1
2019 PURE: Using Verified Remote Attestation to Obtain Proofs of Update, Reset and Erasure in low-End Embedded Systems
abstract
Remote Attestation ( RA) is a security service that enables a trusted verifier ( Vrf) to measure current memory state of an untrusted remote prover ( Prv). If correctly implemented, RA allows Vrf to remotely detect if Prv's memory reflects a compromised state. However, RA by itself offers no means of remedying the situation once P rv is determined to be compromised. In this work we show how a secure RA architecture can be extended to enable important and useful security services for low-end embedded devices. In particular, we extend the formally verified RA architecture, VRASED, to implement provably secure software update, erasure, and system-wide resets. When (serially) composed, these features guarantee to Vrf that a remote Prv has been updated to a functional and malware-free state, and was properly initialized after such process. These services are provably secure against an adversary (represented by malware) that compromises Prv and exerts full control of its software state. Our results demonstrate that such services incur minimal additional overhead (0.4% extra hardware footprint, and 100-s milliseconds to generate combined proofs of update, erasure, and reset), making them practical even for the lowest-end embedded devices, e.g., those based on MSP430 or AVR ATMega micro-controller units (MCUs). All changes introduced by our new services to VRASED trusted components are also formally verified.
Ivan Oliveira Nunes, Karim M. El Defrawy, Norrathep Rattanavipanon, Gene Tsudik
ICCAD1
2019 Towards Systematic Design of Collective Remote Attestation Protocols
abstract
Networks of and embedded (IoT) devices are becoming increasingly popular, particularly, in settings such as smart homes, factories and vehicles. These networks can include numerous (potentially diverse) devices that collectively perform certain tasks. In order to guarantee overall safety and privacy, especially in the face of remote exploits, software integrity of each device must be continuously assured. This can be achieved by Remote Attestation (RA) - a security service for reporting current software state of a remote and untrusted device. While RA of a single device is well understood, collective RA of large numbers of networked embedded devices poses new research challenges. In particular, unlike single-device RA, collective RA has not benefited from any systematic treatment. Thus, unsurprisingly, prior collective RA schemes are designed in an ad hoc fashion. Our work takes the first step toward systematic design of collective RA, in order to help place collective RA onto a solid ground and serve as a set of design guidelines for both researchers and practitioners. We explore the design space for collective RA and show how the notions of security and effectiveness can be formally defined according to a given application domain. We then present and evaluate a concrete collective RA scheme systematically designed to satisfy these goals.
Ivan Oliveira Nunes, Ghada Dessouky, Ahmad Ibrahim 0002, Norrathep Rattanavipanon, Ahmad-Reza Sadeghi, Gene Tsudik
ICDCS1
2019 VRASED: A Verified Hardware/Software Co-Design for Remote Attestation
Ivan Oliveira Nunes, Karim M. El Defrawy, Norrathep Rattanavipanon, Michael Steiner 0001, Gene Tsudik
USENIX Security Symposium1
2019 SNUSE: A secure computation approach for large-scale user re-enrollment in biometric authentication systems
Ivan Oliveira Nunes, Karim M. El Defrawy, Tancrède Lepoint
Future Gener. Comput. Syst.1
2018 KRB-CCN: Lightweight Authentication and Access Control for Private Content-Centric Networks
Ivan Oliveira Nunes, Gene Tsudik
ACNS1
2017 ST-Drop: A novel buffer management strategy for D2D opportunistic networks
abstract
In D2D opportunistic networks, nodes need to cooperate acting as relays for transmitting messages to other nodes according to an opportunistic routing algorithm. To store these messages until they are propagated, each node uses a buffer with limited capacity. However, when multiple messages are forwarded in the network, the number of incoming messages may exceed the nodes' capacity, causing a buffer overflow. In this scenario, message dropping policies are very important to this problem, because when a message is dropped, there is a chance that other copies of this message still exist in the network. In this work, we propose a new buffer management algorithm for opportunistic routing in D2D networks named ST-Drop (Space-Time-Drop). We have evaluated our solution in three different types of opportunistic routing algorithms: epidemic-based, probabilistic, and social-aware. We have conducted simulations using two different publicly available data sources and considered different network traffic loads. Compared to other message drop policies, ST-Drop obtained the highest message delivery ratio in all considered scenarios and the lowest overhead when applied to the state-of-art social-aware and probabilistic routing algorithms, namely, Bubble Rap and Prophet.
Michael D. Silva, Ivan Oliveira Nunes, Raquel A. F. Mini, Antonio Alfredo Ferreira Loureiro
ISCC2
2017 Namespace Tunnels in Content-Centric Networks
abstract
Content-Centric Networking (CCN) is a candidate next-generation Internet architecture that offers an alternative to the current IP-based model. CCN emphasizes scalable and efficient content distribution by making content explicitly named and addressable. It also offers some appealing privacy features, such as lack of source and destination addresses in packets. However, to be considered a fully viable Internet architecture, CCN must support private and anonymous communication that is at least on par with IP. Within this space, a VPN is an important and popular tool that enables users to communicate across insecure public networks as if they were connected over a private network. At present, VPN support is also absent from the repertoire of CCN research. To fill this void, we design, implement and evaluate CCVPN - a content-centric analog to IP-based VPNs of the current Internet architecture. To the best of our knowledge, CCVPN is the first such CCN-based design. Though functionally equivalent to IP-based VPNs, CCVPN offers better privacy due to unlinkability of encapsulated packets to the originating network. We analyze security of CCVPN and experimentally assess its performance.
Ivan Oliveira Nunes, Gene Tsudik, Christopher A. Wood
LCN1
2017 GRM: Group Regularity Mobility Model
abstract
In this work we propose, implement, and evaluate Group Regularity Model (GRM), a novel mobility model that accounts for the role of group meetings regularity in human mobility. We show that existing mobility models for humans do not capture the regularity of human group meetings present in real mobility traces. We characterize the statistical properties of such group meetings in real mobility traces and design GRM accordingly. We show that GRM maintains the typical pairwise contact properties of real traces, such as contact duration and inter-contact time distributions. In addition, GRM accounts for the role of group mobility, presenting group meetings regularity and social communities' structure. Finally, we evaluate state-of-art social-aware protocols for opportunistic routing and show that their performance in synthetic traces generated by GRM is similar to their performance in real-world traces.
Ivan Oliveira Nunes, Clayson Celes, Michael D. Silva, Pedro O. S. Vaz de Melo, Antonio Alfredo Ferreira Loureiro
MSWiM1
2017 GROUPS-NET: Group meetings aware routing in multi-hop D2D networks
Ivan Oliveira Nunes, Clayson Celes, Pedro O. S. Vaz de Melo, Antonio Alfredo Ferreira Loureiro
Comput. Networks1
2016 Group mobility: Detection, tracking and characterization
abstract
In the era of mobile computing, understanding human mobility patterns is crucial in order to better design protocols and applications. Many studies focus on different aspects of human mobility such as people's points of interests, routes, traffic, individual mobility patterns, among others. In this work, we propose to look at human mobility through a social perspective, i.e., analyze the impact of social groups in mobility patterns. We use the MIT Reality Mining proximity trace to detect, track and investigate group's evolution throughout time. Our results show that group meetings happen in a periodical fashion and present daily and weekly periodicity. We analyze how groups' dynamics change over day hours and find that group meetings lasting longer are those with less changes in members composition and with members having stronger social bonds with each other. Our findings can be used to propose meeting prediction algorithms, opportunistic routing and information diffusion protocols, taking advantage of those revealed properties.
Ivan Oliveira Nunes, Pedro O. S. Vaz de Melo, Antonio Alfredo Ferreira Loureiro
ICC1
2016 AoT: Authentication and Access Control for the Entire IoT Device Life-Cycle
abstract
The consumer electronics industry is witnessing a surge in Internet of Things (IoT) devices, ranging from mundane artifacts to complex biosensors connected across disparate networks. As the demand for IoT devices grows, the need for stronger authentication and access control mechanisms is greater than ever. Legacy authentication and access control mechanisms do not meet the growing needs of IoT. In particular, there is a dire need for a holistic authentication mechanism throughout the IoT device life-cycle, namely from the manufacturing to the retirement of the device. As a plausible solution, we present Authentication of Things (AoT), a suite of protocols that incorporate authentication and access control during the entire IoT device life span. Primarily, AoT relies on Identity- and Attribute-Based Cryptography to cryptographically enforce Attribute-Based Access Control (ABAC). Additionally, AoT facilitates secure (in terms of stronger authentication) wireless interoperability of new and guest devices in a seamless manner. To validate our solution, we have developed AoT for Android smartphones like the LG G4 and evaluated all the cryptographic primitives over more constrained devices like the Intel Edison and the Arduino Due. This included the implementation of an Attribute-Based Signature (ABS) scheme. Our results indicate AoT ranges from highly efficient on resource-rich devices to affordable on resource-constrained IoT-like devices. Typically, an ABS generation takes around 27 ms on the LG G4, 282 ms on the Intel Edison, and 1.5 s on the Arduino Due.
Antonio Maia, Artur L. F. Souza, Ítalo S. Cunha, Michele Nogueira Lima, Ivan Oliveira Nunes, Leonardo Cotta, Nicolas Gentille, Antonio Alfredo Ferreira Loureiro, Diego F. Aranha, Harsh Kupwade Patil, Leonardo B. Oliveira
SenSys5