Efficient Symbolic Execution of Software under Fault Attacks

• URL: http://arxiv.org/abs/2503.15825v1
• Date: Thu, 20 Mar 2025 03:19:48 GMT
• Title: Efficient Symbolic Execution of Software under Fault Attacks
• Authors: Yuzhou Fang, Chenyu Zhou, Jingbo Wang, Chao Wang,
• Abstract summary: Fault attacks leverage physically injected hardware faults to break the safety of a software program.<n>Existing methods for analyzing the impact of faults on software suffer from inaccurate fault modeling and inefficient analysis algorithms.<n>We propose a fault modeling technique that leverages program transformation to add symbolic variables to the program, to accurately model the fault-induced program behavior.<n>Second, we propose a redundancy pruning technique that leverages the weakest precondition and fault saturation to mitigate path explosion.
• Score: 6.333695701603308
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We propose a symbolic method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware faults to break the safety of a software program. While there are existing methods for analyzing the impact of faults on software, they suffer from inaccurate fault modeling and inefficient analysis algorithms. We propose two new techniques to overcome these problems. First, we propose a fault modeling technique that leverages program transformation to add symbolic variables to the program, to accurately model the fault-induced program behavior. Second, we propose a redundancy pruning technique that leverages the weakest precondition and fault saturation to mitigate path explosion, which is a performance bottleneck of symbolic execution that is exacerbated by the fault-induced program behavior. We have implemented the method and evaluated it on a variety of benchmark programs. The experimental results show that our method significantly outperforms the state-of-the-art method. Specifically, it not only reveals many previously-missed safety violations but also reduces the running time drastically. Compared to the baseline, our optimized method is 2.0$\times$ faster on average.

Related papers

• SmartFL: Semantics Based Probabilistic Fault Localization [15.481820762877897]
  Testing-based fault localization has been a research focus in software engineering in the past decades. It is crucial to model program semantics in fault localization approaches. Our key idea is: by modeling only the correctness of program values but not their full semantics, a balance could be reached between effectiveness and scalability.
  arXiv  Detail & Related papers  (2025-03-29T21:00:51Z)
• Divide and Conquer based Symbolic Vulnerability Detection [0.16385815610837165]
  This paper presents a vulnerability detection approach based on symbolic execution and control flow graph analysis. Our approach employs a divide-and-conquer algorithm to eliminate irrelevant program information.
  arXiv  Detail & Related papers  (2024-09-20T13:09:07Z)
• Improving Program Debloating with 1-DU Chain Minimality [47.73151075716047]
  We present RLDebloatDU, an innovative debloating technique that employs 1-DU chain minimality within abstract syntax trees. Our approach maintains essential program data dependencies, striking a balance between aggressive code reduction and the preservation of program semantics.
  arXiv  Detail & Related papers  (2024-02-01T02:00:32Z)
• Divide, Conquer and Verify: Improving Symbolic Execution Performance [0.14999444543328289]
  Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. We present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects.
  arXiv  Detail & Related papers  (2023-10-05T15:21:10Z)
• FuzzyFlow: Leveraging Dataflow To Find and Squash Program Optimization Bugs [92.47146416628965]
  FuzzyFlow is a fault localization and test case extraction framework designed to test program optimizations. We leverage dataflow program representations to capture a fully reproducible system state and area-of-effect for optimizations. To reduce testing time, we design an algorithm for minimizing test inputs, trading off memory for recomputation.
  arXiv  Detail & Related papers  (2023-06-28T13:00:17Z)
• Fast and Accurate Error Simulation for CNNs against Soft Errors [64.54260986994163]
  We present a framework for the reliability analysis of Conal Neural Networks (CNNs) via an error simulation engine. These error models are defined based on the corruption patterns of the output of the CNN operators induced by faults. We show that our methodology achieves about 99% accuracy of the fault effects w.r.t. SASSIFI, and a speedup ranging from 44x up to 63x w.r.t.FI, that only implements a limited set of error models.
  arXiv  Detail & Related papers  (2022-06-04T19:45:02Z)
• Revisiting and Advancing Fast Adversarial Training Through The Lens of Bi-Level Optimization [60.72410937614299]
  We propose a new tractable bi-level optimization problem, design and analyze a new set of algorithms termed Bi-level AT (FAST-BAT) FAST-BAT is capable of defending sign-based projected descent (PGD) attacks without calling any gradient sign method and explicit robust regularization.
  arXiv  Detail & Related papers  (2021-12-23T06:25:36Z)
• Adaptive Perturbation for Adversarial Attack [50.77612889697216]
  We propose a new gradient-based attack method for adversarial examples. We use the exact gradient direction with a scaling factor for generating adversarial perturbations. Our method exhibits higher transferability and outperforms the state-of-the-art methods.
  arXiv  Detail & Related papers  (2021-11-27T07:57:41Z)
• Generating Adversarial Computer Programs using Optimized Obfuscations [43.95037234252815]
  We investigate principled ways to adversarially perturb a computer program to fool such learned models. We use program obfuscations, which have conventionally been used to avoid attempts at reverse engineering programs. We show that our best attack proposal achieves a $52%$ improvement over a state-of-the-art attack generation approach.
  arXiv  Detail & Related papers  (2021-03-18T10:47:15Z)
• Excursion Search for Constrained Bayesian Optimization under a Limited Budget of Failures [62.41541049302712]
  We propose a novel decision maker grounded in control theory that controls the amount of risk we allow in the search as a function of a given budget of failures. Our algorithm uses the failures budget more efficiently in a variety of optimization experiments, and generally achieves lower regret, than state-of-the-art methods.
  arXiv  Detail & Related papers  (2020-05-15T09:54:09Z)

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.