Automatic Detection, Validation and Repair of Race Conditions in
Interrupt-Driven Embedded Software
- URL: http://arxiv.org/abs/2305.17869v1
- Date: Mon, 29 May 2023 03:22:00 GMT
- Title: Automatic Detection, Validation and Repair of Race Conditions in
Interrupt-Driven Embedded Software
- Abstract summary: We present SDRacer, an automated framework that can detect, validate and repair race conditions in interrupt-driven embedded software.
We evaluate SDRacer on nine real-world embedded programs written in C language.
- Score: 17.564883311453134
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Interrupt-driven programs are widely deployed in safety-critical embedded
systems to perform hardware and resource dependent data operation tasks. The
frequent use of interrupts in these systems can cause race conditions to occur
due to interactions between application tasks and interrupt handlers (or two
interrupt handlers). Numerous program analysis and testing techniques have been
proposed to detect races in multithreaded programs. Little work, however, has
addressed race condition problems related to hardware interrupts. In this
paper, we present SDRacer, an automated framework that can detect, validate and
repair race conditions in interrupt-driven embedded software. It uses a
combination of static analysis and symbolic execution to generate input data
for exercising the potential races. It then employs virtual platforms to
dynamically validate these races by forcing the interrupts to occur at the
potential racing points. Finally, it provides repair candidates to eliminate
the detected races. We evaluate SDRacer on nine real-world embedded programs
written in C language. The results show that SDRacer can precisely detect and
successfully fix race conditions.
Related papers
- Reactive Peripheral Modeling for Faithful Firmware Rehosting [46.071436745445]
Reactive Peripheral Modeling ( RPM) is an abstraction that models hardware peripherals as reactive and stateful systems.<n>We implement RPM in Bluezz for BLE firmware rehosting and fuzzing, and show that reactive modeling is necessary to reach deep protocol states.<n>Bluezz achieves an average basic-block coverage more than 2.6 times that of prior state-of-the-art rehosting approaches.
arXiv Detail & Related papers (2026-08-30T11:54:37Z) - DISARM: Target Electronic Device Informed Mitigation of Software Runtime Side-Channel Vulnerabilities [2.537406035246369]
Program runtime or timing attacks exploit variations in a program's execution times to extract sensitive information.<n>We propose DISARM, a joint hardware-software methodology for mitigating runtime side-channel vulnerabilities.<n>We implement DISARM to support C, C++, and Java source codes and validate it across 22 standard benchmarks.
arXiv Detail & Related papers (2026-06-18T05:22:38Z) - VIBEPASS: Can Vibe Coders Really Pass the Vibe Check? [46.85901599242161]
We evaluate two coupled tasks: emphFault-Triggering Test Generation (FT-Test) and emphFault-targeted Program Repair (FPR)<n>We find that fault-targeted reasoning does not scale with general coding ability.<n>Test-guided repair reveals a complementary insight: when self-generated tests successfully witness a fault, the resulting repair matches or outperforms repair guided by externally provided tests, but tests that fail to witness the fault actively degrade repair below unguided baselines.
arXiv Detail & Related papers (2026-03-16T21:14:28Z) - Scaling Agentic Verifier for Competitive Coding [66.11758166379092]
Large language models (LLMs) have demonstrated strong coding capabilities but still struggle to solve competitive programming problems correctly in a single attempt.<n>Execution-based re-ranking offers a promising test-time scaling strategy, yet existing methods are constrained by either difficult test case generation or inefficient random input sampling.<n>We propose Agentic Verifier, an execution-based agent that actively reasons about program behaviors and searches for highly discriminative test inputs.
arXiv Detail & Related papers (2026-02-04T06:30:40Z) - Compiling Away the Overhead of Race Detection [4.072903728718951]
Dynamic data race detectors are indispensable for flagging errors in software, but their high runtime overhead limits their adoption.<n>We introduce a suite of interprocedural static analyses to eliminate instrumentation for provably race-free accesses.<n>Our approach significantly reduces race detection overhead, achieving a geomean speedup of 1.34x, with peak speedups reaching 2.5x under high thread contention.
arXiv Detail & Related papers (2025-12-05T09:26:08Z) - Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [84.30534714651093]
We present an innovative APR tool for Dafny, a verification-aware programming language.<n>We localize faults through a series of steps, which include using Hoare Logic to determine the state of each statement within the program.<n>We evaluate our approach using DafnyBench, a benchmark of real-world Dafny programs.
arXiv Detail & Related papers (2025-07-04T15:36:12Z) - Context Switching for Secure Multi-programming of Near-Term Quantum Computers [19.420764480790414]
Crosstalk from concurrent two-qubit CNOT gates poses security risks.
We design Zero Knowledge Tampering Attacks (ZKTAs), using which attackers can exploit crosstalk without knowledge of the hardware error profile.
We propose QONTEXTS: a context-switching technique that defends against ZKTAs by running programs across multiple contexts.
arXiv Detail & Related papers (2025-04-09T17:05:16Z) - HardRace: A Dynamic Data Race Monitor for Production Use [15.504566762273262]
Data races are critical issues in multithreaded program, leading to unpredictable, catastrophic and difficult-to-diagnose problems.
We introduce HardRace, a data race monitor to detect races on-the-fly while with sufficiently low runtime overhead and high detection capability.
arXiv Detail & Related papers (2024-10-24T03:59:02Z) - Optimistic Prediction of Synchronization-Reversal Data Races [6.407713444542916]
Dynamic data race detection has emerged as a key technique for ensuring reliability of concurrent software in practice.
In this work, we identify a class of data races, called Optimistic Sync(hronization)-Reversal races that can be detected in a tractable manner.
We also propose a sound algorithm OSR for detecting all optimistic sync-reversal data races in overall quadratic time.
arXiv Detail & Related papers (2024-01-11T03:34:21Z) - Navigating the Concurrency Landscape: A Survey of Race Condition Vulnerability Detectors [0.12289361708127873]
This paper focuses on the realm of race condition bug detectors.
We systematically categorize these detectors based on the diverse methodologies they employ.
We shed light on the application of fuzzing techniques in the detection of race condition vulnerabilities.
arXiv Detail & Related papers (2023-12-22T07:05:39Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
Learned transpilation offers an alternative to manual re-writing and engineering efforts.
Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness.
Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
arXiv Detail & Related papers (2023-09-25T15:42:18Z) - Using Machine Learning To Identify Software Weaknesses From Software
Requirement Specifications [49.1574468325115]
This research focuses on finding an efficient machine learning algorithm to identify software weaknesses from requirement specifications.
Keywords extracted using latent semantic analysis help map the CWE categories to PROMISE_exp. Naive Bayes, support vector machine (SVM), decision trees, neural network, and convolutional neural network (CNN) algorithms were tested.
arXiv Detail & Related papers (2023-08-10T13:19:10Z) - Tailoring Stateless Model Checking for Event-Driven Multi-Threaded
Programs [1.2948955292336792]
We present Event-DPOR, a DPOR algorithm tailored to event-driven programs.
It is based on Optimal-DPOR, an optimal DPOR algorithm for multi-threaded programs.
We prove correctness of Event-DPOR for all programs, and optimality for a large subclass.
arXiv Detail & Related papers (2023-07-29T08:43:49Z) - A survey on hardware-based malware detection approaches [45.24207460381396]
Hardware-based malware detection approaches leverage hardware performance counters and machine learning prowess.
We meticulously analyze the approach, unraveling the most common methods, algorithms, tools, and datasets that shape its contours.
The discussion extends to crafting mixed hardware and software approaches for collaborative efficacy, essential enhancements in hardware monitoring units, and a better understanding of the correlation between hardware events and malware applications.
arXiv Detail & Related papers (2023-03-22T13:00:41Z) - Software Testing for Machine Learning [13.021014899410684]
Machine learning has shown to be susceptible to deception, leading to errors and even fatal failures.
This circumstance calls into question the widespread use of machine learning, especially in safety-critical applications.
This summary talk discusses the current state-of-the-art of software testing for machine learning.
arXiv Detail & Related papers (2022-04-30T08:47:10Z) - SUPERNOVA: Automating Test Selection and Defect Prevention in AAA Video
Games Using Risk Based Testing and Machine Learning [62.997667081978825]
Testing video games is an increasingly difficult task as traditional methods fail to scale with growing software systems.
We present SUPERNOVA, a system responsible for test selection and defect prevention while also functioning as an automation hub.
The direct impact of this has been observed to be a reduction in 55% or more testing hours for an undisclosed sports game title.
arXiv Detail & Related papers (2022-03-10T00:47:46Z) - Sample-Efficient Safety Assurances using Conformal Prediction [57.92013073974406]
Early warning systems can provide alerts when an unsafe situation is imminent.
To reliably improve safety, these warning systems should have a provable false negative rate.
We present a framework that combines a statistical inference technique known as conformal prediction with a simulator of robot/environment dynamics.
arXiv Detail & Related papers (2021-09-28T23:00:30Z) - Improving Compositionality of Neural Networks by Decoding
Representations to Inputs [83.97012077202882]
We bridge the benefits of traditional and deep learning programs by jointly training a generative model to constrain neural network activations to "decode" back to inputs.
We demonstrate applications of decodable representations to out-of-distribution detection, adversarial examples, calibration, and fairness.
arXiv Detail & Related papers (2021-06-01T20:07:16Z) - Online Learning Probabilistic Event Calculus Theories in Answer Set
Programming [70.06301658267125]
Event Recognition (CER) systems detect occurrences in streaming time-stamped datasets using predefined event patterns.
We present a system based on Answer Set Programming (ASP), capable of probabilistic reasoning with complex event patterns in the form of rules weighted in the Event Calculus.
Our results demonstrate the superiority of our novel approach, both terms efficiency and predictive.
arXiv Detail & Related papers (2021-03-31T23:16:29Z)
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.