arXiv subjects

Ivan De Oliveira Nunes

Publications and source records attributed to Ivan De Oliveira Nunes.

At least 19 recordsLinked to original sources

arXiv2026

Extending Layered Attestation into ARM Application Run-Times

Modern mobile and edge platforms provide hardware-backed attestation of application and platform integrity at load-time. However, they offer little support once application execution begins. We present ARA, an Application-Runtime Anchor for ARM that extends this load-time chain of trust into execution. ARA bootstraps from the underlying ARM platform Root of Trust (RoT) through a measured loading chain and establishes an attested protected run-time within the application address space using recently introduced ARM Permission Overlay Extensions (POE). The resulting run-time domain can host programmable RoTs for Measurement and Storage (RTM/RTS), enabling application run-time integrity verification, attestation evidence generation, and protected use of secrets while retaining efficient access to application run-time state. As exemplary uses, we instantiate ARA for protected media decryption and application control flow measurement. Our prototype and evaluation show that ARA supports frequent run-time RoT-backed operations at near in-process cost, with roughly 10x and 50x lower overhead than out-of-process equivalents. This offers a practical bridge from layered attestation to application run-time trusted computing on ARM.

cs.CR↗

arXiv2026

Resolving Conflicts Between RTOS Timekeeping and Uninterruptable Trusted Computing

Trusted Execution Environments (TEEs) on low-power microcontrollers (e.g., ARM TrustZone-M) enable isolation of Secure and Non-Secure software but still require both worlds to share resources, including interrupt controllers. In this model, real-time applications and real-time operating systems (RTOS-s) are executed in the Non-Secure sub-system, whereas the Secure sub-system is typically reserved for a small set of pre-defined security (e.g., cryptographic) operations referred to as trusted computing services. However, many RTOS-s rely on periodic interrupts (SysTicks) to advance their own notion of time (time-keeping), and the delivery of this interrupt is essential for preserving real-time behavior. On the other hand, the security of many trusted computing services requires atomicity vis-a-vis the Non-Secure sub-system (where the RTOS resides), precluding SysTick handling. This paper first characterizes this conflict and then introduces a Secure-driven time synchronization mechanism in which the Secure World measures elapsed time and compensates the Non-Secure RTOS by unobtrusively updating the RTOS time-keeping data structures with the appropriate number of missed ticks before re-enabling interrupts and resuming the execution of the Non-Secure system. This approach restores a consistent, monotonic notion of time across worlds and enables secure coexistence of trusted computing services and RTOS-s on microcontrollers. Importantly, the proposed approach requires no modifications to the underlying RTOS and yields no significant run-time overhead.

cs.CR↗

arXiv2026

Verifiable and Confidential DNN Inference on Low-End Edge Devices

Deploying deep neural network (DNN) inference on low-end edge devices raises two key challenges: protecting model confidentiality against a potentially compromised edge system and enabling verifiable inference without incurring prohibitive overhead. Existing approaches either house partial models and inference software within trusted execution environments (TEEs), resulting in high cost and an application-dependent trusted computing base (TCB), or execute in untrusted environments, providing little security. In this work, we present VECODI, a framework for verifiable and confidential DNN inference on constrained edge devices. At its core, VECODI introduces SHANGRI-LA, a new execution abstraction on TrustZone-M TEEs that establishes a third runtime environment with privileges strictly between the Secure and Non-Secure Worlds. VECODI leverages SHANGRI-LA to execute untrusted inference code in the Non-Secure World while using minimal application-agnostic Secure-World support to protect model confidentiality and enable verifiability (with respect to proper execution of inference code and model parameters) of inference results. We realize VECODI on a real-world NUCLEO-L552ZE-Q development board and open-source its prototype. Our results show VECODI's small TCB, memory footprint, and runtime overhead, making it a practical option for secure inference in low-end edge devices.

cs.CR↗

arXiv2026

Boosting Device Utilization in Control Flow Auditing

Micro-Controller Units (MCUs) are widely used in safety-critical systems, making them attractive targets for attacks. This calls for lightweight defenses that remain effective despite software compromise. Control Flow Auditing (CFAud) is one such mechanism wherein a remote verifier (Vrf) is guaranteed to received evidence about the control flow path taken on a prover (Prv) MCU, even when Prv software is compromised. Despite promising benefits, current CFAud architectures unfortunately require a ``busy-wait'' phase where a hardware-anchored root-of-trust (RoT) in Prv retains execution control to ensure delivery of control flow evidence to Vrf. This drastically reduces the CPU utilization on Prv. In this work, we addresses this limitation with an architecture for Contention Avoidance in Runtime Auditing with Minimized Execution Latency (CARAMEL). CARAMEL is a hardware-software RoT co-design that enables Prv applications to resume while control flow evidence is transmitted to Vrf. This significantly reduces contention due to transmission delays and improves CPU utilization without giving up on security. Key to CARAMEL is our design of a new RoT with a self-contained (and minimal) dedicated communication interface. CARAMEL's implementation and accompanying evaluation are made open-source. Our results show substantially improved CPU utilization at a modest hardware cost.

cs.CR↗

arXiv2025

Towards Browser Controls to Protect Cookies from Malicious Extensions

Cookies maintain state across related web traffic. As such, cookies are commonly used for authentication by storing a user's session ID and replacing the need to re-enter credentials in subsequent traffic. These so-called ``session cookies'' are prime targets for attacks that aim to steal them to gain unauthorized access to user accounts. To mitigate these attacks, the Secure and HttpOnly cookie attributes limit a cookie's accessibility from malicious networks and websites. However, these controls overlook browser extensions: third-party HTML/JavaScript add-ons with access to privileged browser APIs and the ability to operate across multiple websites. Thus malicious or compromised extensions can provide unrestricted access to a user's session cookies. In this work, we first analyze the prevalence of extensions with access to ``risky'' APIs (those that enable cookie modification and theft) and find that they have hundreds of millions of users. Motivated by this, we propose a mechanism to protect cookies from malicious extensions by introducing two new cookie attributes: BrowserOnly and Monitored. The BrowserOnly attribute prevents extension access to cookies altogether. While effective, not all cookies can be made inaccessible. Thus cookies with the Monitored attribute remain accessible but are tied to a single browser and any changes made to the cookie are logged. As a result, stolen Monitored cookies are unusable outside their original browser and servers can validate the modifications performed. To demonstrate the proposed functionalities, we design and implement CREAM (Cookie Restrictions for Extension Abuse Mitigation) a modified version of the open-source Chromium browser realizing these controls. Our evaluation indicates that CREAM effectively protects cookies from malicious extensions while incurring little run-time overheads.

cs.CR↗

arXiv2025

Efficient Control Flow Attestation by Speculating on Control Flow Path Representations

Control Flow Attestation (CFA) allows remote verification of run-time software integrity in embedded systems. However, CFA is limited by the storage/transmission costs of generated control flow logs (CFlog). Recent work has proposed application-specific optimizations by speculating on likely sub-paths in CFlog and replacing them with reserved symbols at runtime. Albeit effective, prior approaches do not consider the representation of addresses in a control flow path for speculation. This work proposes RESPEC-CFA, an architectural extension for CFA allowing for speculation on (1) the locality of control flows and (2) their Huffman encoding. Alone, RESPEC-CFA reduces CFlog sizes by up to 90.1%. Combined with prior methods, RESPEC-CFA yields reductions of up to 99.7%, representing a significant step toward practical CFA.

cs.CR↗

arXiv2025

On the Verification of Control Flow Attestation Evidence

Remote run-time attestation methods, including Control Flow Attestation (CFA) and Data Flow Attestation (DFA), have been proposed to generate precise evidence of execution's control flow path (in CFA) and optionally execution data inputs (in DFA) on a remote and potentially compromised embedded device, hereby referred to as a Prover (Prv). Recent advances in run-time attestation architectures are also able to guarantee that a remote Verifier (Vrf) reliably receives this evidence from Prv, even when Prv's software state is fully compromised. This, in theory, enables secure "run-time auditing" in addition to best-effort attestation, i.e., it guarantees that Vrf can examine execution evidence to identify previously unknown compromises as soon as they are exploited, pinpoint their root cause(s), and remediate them. However, prior work has for the most part focused on securely implementing Prv's root of trust (responsible for generating authentic run-time evidence), leaving Vrf 's perspective in this security service unexplored. In this work, we argue that run-time attestation and auditing are only truly useful if Vrf can effectively analyze received evidence. From this premise, we characterize different types of evidence produced by existing run-time attestation/auditing architectures in terms of Vrf 's ability to detect and remediate (previously unknown) vulnerabilities. As a case study for practical uses of run-time evidence by Vrf, we propose SABRE: a Security Analysis and Binary Repair Engine. SABRE showcases how Vrf can systematically leverage run-time evidence to detect control flow attacks, pinpoint corrupted control data and specific instructions used to corrupt them, and leverage this evidence to automatically generate binary patches to buffer overflow and use-after-free vulnerabilities without source code knowledge.

cs.CR↗

arXiv2025

Provable Execution in Real-Time Embedded Systems

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. 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-M33 processor. We evaluate and report on PEARTS security and (modest) overheads.

cs.CR↗

arXiv2025

Poisoning Prevention in Federated Learning and Differential Privacy via Stateful Proofs of Execution

The rise in 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 (PoSX) for IoT/embedded devices' software. To realize the PoSX concept, we design SLAPP: a System-Level Approach for Poisoning Prevention. SLAPP leverages commodity security features of embedded devices - in particular ARM TrustZoneM 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 SLAPP's security and low overhead.

cs.CR↗

arXiv2024

SoK: Runtime Integrity

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.

cs.CR↗

arXiv2024

SpecCFA: Enhancing Control Flow Attestation/Auditing via Application-Aware Sub-Path Speculation

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 (Vrf) to remotely assess the run-time behavior of a prover MCU (Prv), generating an authenticated trace of all of Prv control flow transfers (CFLog). Further, Control Flow Auditing architectures augment CFA by guaranteeing the delivery of evidence to Vrf. 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 Vrf to securely speculate on likely control flow sub-paths for each attested program. At run-time, when a sub-path in CFLog matches 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 and one based on a commodity Trusted Execution Environment (ARM TrustZone-M). In both cases, SpecCFA significantly lowers storage/performance costs that are critical to resource-constrained MCUs.

cs.CR↗

arXiv2024

TRACES: TEE-based Runtime Auditing for Commodity Embedded Systems

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 CFLog to 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.

cs.CR↗

arXiv2024

UCCA: A Verified Architecture for Compartmentalization of Untrusted Code Sections in Resource-Constrained Devices

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 paper, we tackle this problem by proposing, demonstrating security, and formally verifying the implementation of UCCA: an Untrusted Code Compartment Architecture. 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 prior related work.

cs.CR↗

arXiv2024

Towards Remotely Verifiable Software Integrity in Resource-Constrained IoT Devices

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.

cs.CR↗

arXiv2023

ACFA: Secure Runtime Auditing & Guaranteed Device Healing via Active Control Flow Attestation

Low-end embedded devices are increasingly used in various smart applications and spaces. They are implemented under strict cost and energy budgets, using microcontroller units (MCUs) that lack security features available in general-purpose processors. In this context, Remote Attestation (RA) was proposed as an inexpensive security service to enable a verifier (Vrf) to remotely detect illegal modifications to a software binary installed on a low-end prover MCU (Prv). Since attacks that hijack the software's control flow can evade RA, Control Flow Attestation (CFA) augments RA with information about the exact order in which instructions in the binary are executed, enabling detection of control flow attacks. We observe that current CFA architectures can not guarantee that Vrf ever receives control flow reports in case of attacks. In turn, while they support exploit detection, they provide no means to pinpoint the exploit origin. Furthermore, existing CFA requires either binary instrumentation, incurring significant runtime overhead and code size increase, or relatively expensive hardware support, such as hash engines. In addition, current techniques are neither continuous (only meant to attest self-contained operations) nor active (offer no secure means to remotely remediate detected compromises). To jointly address these challenges, we propose ACFA: a hybrid (hardware/software) architecture for Active CFA. ACFA enables continuous monitoring of all control flow transfers in the MCU and does not require binary instrumentation. It also leverages the recently proposed concept of Active Roots-of-Trust to enable secure auditing of vulnerability sources and guaranteed remediation when a compromise is detected. We provide an open-source reference implementation of ACFA on top of a commodity low-end MCU (TI MSP430) and evaluate it to demonstrate its security and cost-effectiveness.

cs.CR↗

arXiv2023

DiCA: A Hardware-Software Co-Design for Differential Checkpointing in Intermittently Powered Devices

Intermittently powered devices rely on opportunistic energy-harvesting to function, leading to recurrent power interruptions. This paper introduces DiCA, a proposal for a hardware/software co-design to create differential check-points in intermittent devices. DiCA 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 nonmaskable interrupt. Experimental results show the cost-effectiveness and energy efficiency of DiCA, enabling extended application activity cycles in intermittently powered embedded devices.

cs.AR↗

arXiv2023

PARseL: Towards a Verified Root-of-Trust over seL4

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.

cs.CR↗

arXiv2022

CASU: Compromise Avoidance via Secure Update for Low-end Embedded Systems

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.

cs.CR↗