Provable Execution in Real-Time Embedded Systems

• URL: http://arxiv.org/abs/2505.13842v1
• Date: Tue, 20 May 2025 02:31:13 GMT
• Title: Provable Execution in Real-Time Embedded Systems
• Abstract summary: We develop Provable Execution Architecture for Real-Time Systems (PEARTS)<n>PEARTS is the first PoX system that can be directly deployed alongside a commodity embedded real-time operating system (FreeRTOS)
• Score: 8.816934283264633
• License: http://creativecommons.org/licenses/by/4.0/
• 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. 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.

Related papers

• Prezta: Provable Remote Execution of Zero-Trust Authorization using SNARKs [4.597186239326157]
  We propose Provable Remote Execution of Zero-Trust Authorization (Prezta)<n>Prezta eliminates gateways by evaluating policies within a zero-knowledge virtual machine (zkVM) running on the client.<n>We implement a prototype built using the RISC Zero zkVM that supports XACML 3.0 policies and JWT identity claims.
  arXiv  Detail & Related papers  (2026-07-13T12:21:08Z)
• Resolving Conflicts Between RTOS Timekeeping and Uninterruptable Trusted Computing [10.10879231972864]
  This paper introduces a Secure-driven time synchronization mechanism in which the Secure World measures elapsed time and compensates the Non-Secure RTOS.<n>This approach restores a consistent, monotonic notion of time across worlds and enables secure coexistence of trusted computing services and RTOS-s on microcontrollers.
  arXiv  Detail & Related papers  (2026-04-27T10:10:29Z)
• Boosting Device Utilization in Control Flow Auditing [47.36491265793223]
  Control Flow (CFAud) is a 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.<n>Current CFAud requires a busy-wait'' phase where root-of-anchored root-of-RoT in Prv retains execution to ensure delivery of flow evidence to Vrf.<n>CARAMEL is a hardware RoT co-design that enables Prv to resume while control flow evidence is transmitted to Vrf.
  arXiv  Detail & Related papers  (2026-03-02T18:26:17Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• OAMAC: Origin-Aware Mandatory Access Control for Practical Post-Compromise Attack Surface Reduction [0.0]
  Execution origin is a missing abstraction in modern operating system security models.<n>We introduce origin-aware mandatory access control (OAMAC)<n> OAMAC treats execution origin as a first-class security attribute.
  arXiv  Detail & Related papers  (2026-01-20T14:40:26Z)
• CaMeLs Can Use Computers Too: System-level Security for Computer Use Agents [60.98294016925157]
  AI agents are vulnerable to prompt injection attacks, where malicious content hijacks agent behavior to steal credentials or cause financial loss.<n>We introduce Single-Shot Planning for CUAs, where a trusted planner generates a complete execution graph with conditional branches before any observation of potentially malicious content.<n>Although this architectural isolation successfully prevents instruction injections, we show that additional measures are needed to prevent Branch Steering attacks.
  arXiv  Detail & Related papers  (2026-01-14T23:06:35Z)
• Towards a Multi-Layer Defence Framework for Securing Near-Real-Time Operations in Open RAN [4.240433132593161]
  Securing the near-real-time (near-RT) control operations in Open Radio Access Networks (Open RAN) is increasingly critical.<n>New runtime threats target the control loop while the system is operational.<n>We propose a multi-layer defence framework designed to enhance the security of near-RT RAN Intelligent Controller (RIC) operations.
  arXiv  Detail & Related papers  (2025-12-01T12:13:32Z)
• Resolving Availability and Run-time Integrity Conflicts in Real-Time Embedded Systems [13.829082181692876]
  PAIR monitors real-time tasks for run-time integrity violations and maintains an Availability Region (AR) of all tasks that are safe to continue.<n>With its hardware approach, PAIR does not cause any run-time overhead to the executing tasks, integrates with real-time operating systems (RTOSs), and is affordable to low-end microcontroller units (MCUs) by incurring +2.3% overhead in memory and hardware usage.
  arXiv  Detail & Related papers  (2025-11-18T03:16:50Z)
• Performance and Storage Analysis of CRYSTALS Kyber as a Post Quantum Replacement for RSA and ECC [49.1574468325115]
  CRYSTALS-Kyber is a post-quantum cryptographic solution standardized by NIST in 2022.<n>This study evaluates Kyber's practical viability through performance testing across various implementation schemes.
  arXiv  Detail & Related papers  (2025-08-03T09:53:45Z)
• DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
  Large Language Models (LLMs) are increasingly central to agentic systems due to their strong reasoning and planning capabilities.<n>This interaction also introduces the risk of prompt injection attacks, where malicious inputs from external sources can mislead the agent's behavior.<n>We propose a Dynamic Rule-based Isolation Framework for Trustworthy agentic systems, which enforces both control and data-level constraints.
  arXiv  Detail & Related papers  (2025-06-13T05:01:09Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  Code generation with large language models (LLMs) is increasingly adopted in production but fails to ensure code quality.<n>We propose REAL, a reinforcement learning framework that incentivizes LLMs to generate production-quality code.
  arXiv  Detail & Related papers  (2025-05-28T17:57:47Z)
• Extending Lifetime of Embedded Systems by WebAssembly-based Functional Extensions Including Drivers [46.538276603099916]
  We present Wasm-IO, a framework designed to facilitate peripheral I/O operations within WebAssembly (Wasm) containers.<n>We detail synchronous I/O and methods for embedding platform-independent peripheral configurations within Wasm binaries.
  arXiv  Detail & Related papers  (2025-03-10T17:22:00Z)
• ENOLA: Efficient Control-Flow Attestation for Embedded Systems [4.974696231180418]
  We present ENOLA, an efficient control-flow attestation solution for low-end embedded systems.<n> ENOLA introduces a novel authenticator that achieves linear space complexity.<n>We have developed the ENOLA compiler through LLVM passes and attestation engine on the ARMv8.1-M architecture.
  arXiv  Detail & Related papers  (2025-01-20T00:41:58Z)
• EILID: Execution Integrity for Low-end IoT Devices [12.193184827858326]
  EILID is a hybrid architecture that ensures software execution integrity on low-end devices.<n>It is built atop CASU, a prevention-based (i.e., active) hybrid Root-of-Trust (RoT) that guarantees software immutability.
  arXiv  Detail & Related papers  (2025-01-16T00:31:39Z)
• T-Edge: Trusted Heterogeneous Edge Computing [11.859343440194944]
  This paper proposes a practical trusted execution environment design for ARM/FPGA System-on-Chip platforms.<n>The design features a dedicated security controller within the ARM TrustZone, overseeing FPGA reconfiguration and managing communication between CPU cores and FPGA fabrics.<n>We employ an automated protocol verifier, ProVerif, to validate its compliance with essential security requirements.
  arXiv  Detail & Related papers  (2024-12-18T14:45:07Z)
• Code-as-Monitor: Constraint-aware Visual Programming for Reactive and Proactive Robotic Failure Detection [56.66677293607114]
  We propose Code-as-Monitor (CaM) for both open-set reactive and proactive failure detection.<n>To enhance the accuracy and efficiency of monitoring, we introduce constraint elements that abstract constraint-related entities.<n>Experiments show that CaM achieves a 28.7% higher success rate and reduces execution time by 31.8% under severe disturbances.
  arXiv  Detail & Related papers  (2024-12-05T18:58:27Z)
• ACRIC: Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  Recent security incidents in safety-critical industries exposed how the lack of proper message authentication enables attackers to inject malicious commands or alter system behavior.<n>These shortcomings have prompted new regulations that emphasize the pressing need to strengthen cybersecurity.<n>We introduce ACRIC, a message authentication solution to secure legacy industrial communications.
  arXiv  Detail & Related papers  (2024-11-21T18:26:05Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
  Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs) TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks. We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
  arXiv  Detail & Related papers  (2024-01-17T00:56:23Z)
• Poster: Control-Flow Integrity in Low-end Embedded Devices [12.193184827858326]
  This work constructs an architecture that ensures integrity of software execution against run-time attacks. It is built atop a recently proposed CASU -- a low-cost active Root-of-Trust (RoT) that guarantees software immutability.
  arXiv  Detail & Related papers  (2023-09-19T07:52:43Z)
• Citadel: Simple Spectre-Safe Isolation For Real-World Programs That Share Memory [8.414722884952525]
  We introduce a new security property we call relaxed microarchitectural isolation (RMI)<n>RMI allows sensitive programs that are not-constant-time to share memory with an attacker while restricting the information leakage to that of non-speculative execution.<n>Our end-to-end prototype, Citadel, consists of an FPGA-based multicore processor that boots Linux and runs secure applications.
  arXiv  Detail & Related papers  (2023-06-26T17:51:23Z)
• Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
  This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool.
  arXiv  Detail & Related papers  (2022-09-28T12:19:13Z)
• Systematic Prevention of On-Core Timing Channels by Full Temporal Partitioning [13.313360308792198]
  We introduce the temporal fence instruction fence.t, which provides the required mechanisms by clearing vulnerable microarchitectural state.<n>We implement fence.t on an experimental version of the seL4 microkernel and CVA6, an open-source, in-order, application class, 64-bit RISC-V core.<n>We find that a complete, systematic, ISA-supported erasure of all non-architectural core components is the most effective implementation.
  arXiv  Detail & Related papers  (2022-02-24T11:17:34Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.