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
- Authors: Antonio Joia Neto, Norrathep Rattanavipanon, Ivan De Oliveira Nunes,
- 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
- 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) - 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) - 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)
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.