A Formal Verification Approach to Safeguard Controller Variables from Single Event Upset

• URL: http://arxiv.org/abs/2505.06648v1
• Date: Sat, 10 May 2025 13:56:02 GMT
• Title: A Formal Verification Approach to Safeguard Controller Variables from Single Event Upset
• Authors: Ganesha, Sujit Kumar Chakrabarti,
• Abstract summary: We present a method based on program analysis and formal verification to identify conditionally relevant variables (CRVs)<n>CRVs could lead to violation of safety properties in control software when affected by single event upsets (SEUs)
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a method based on program analysis and formal verification to identify conditionally relevant variables (CRVs) - variables which could lead to violation of safety properties in control software when affected by single event upsets (SEUs). Traditional static analysis can distinguish between relevant and irrelevant variables. However, it would fail to take into account the conditions specific to the control software in question. This can lead to false positives. Our algorithm employs formal verification to avoid false positives. We have conducted experiments that demonstrate that CRVs indeed are fewer in number than what traditional static analysis can detect and that our algorithm is able to identify this fact. The information provided by our algorithm could prove helpful to a compiler while it does register allocation during the compilation of the control software. In turn, this could cause significant reduction in the cost of controller chips.

Related papers

• CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
  We propose CANTXSec, the first deterministic Intrusion Detection and Prevention system based on physical ECU activations.<n>It detects and prevents classical attacks in the CAN bus, while detecting advanced attacks that have been less investigated in the literature.<n>We prove the effectiveness of our solution on a physical testbed, where we achieve 100% detection accuracy in both classes of attacks while preventing 100% of FIAs.
  arXiv  Detail & Related papers  (2025-05-14T13:37:07Z)
• Checkification: A Practical Approach for Testing Static Analysis Truths [0.0]
  We propose a method for testing abstract interpretation-based static analyzers.<n>The main advantage of our approach lies in its simplicity, which stems directly from framing it within the Ciao assertion-based validation framework.<n>We have applied our approach to the CiaoPP static analyzer, resulting in the identification of many bugs with reasonable overhead.
  arXiv  Detail & Related papers  (2025-01-21T12:38:04Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs.
  arXiv  Detail & Related papers  (2024-07-21T07:30:30Z)
• Geospatial Trajectory Generation via Efficient Abduction: Deployment for Independent Testing [1.8877926393541125]
  We show that we can abduce movement trajectories efficiently through an informed (i.e., A*) search.<n>We also report on our own experiments showing that we not only provide exact results but also scale to very large scenarios.
  arXiv  Detail & Related papers  (2024-07-08T23:11:47Z)
• Automatically Adaptive Conformal Risk Control [49.95190019041905]
  We propose a methodology for achieving approximate conditional control of statistical risks by adapting to the difficulty of test samples.<n>Our framework goes beyond traditional conditional risk control based on user-provided conditioning events to the algorithmic, data-driven determination of appropriate function classes for conditioning.
  arXiv  Detail & Related papers  (2024-06-25T08:29:32Z)
• BEC: Bit-Level Static Analysis for Reliability against Soft Errors [0.26107298043931204]
  We propose a bit-level error coalescing (BEC) static program analysis to understand and improve program reliability against soft errors. BEC analysis tracks each bit corruption in the register file and classifies the effect of the corruption by its semantics at compile time. The proposed method is generic and not limited to a specific computer architecture.
  arXiv  Detail & Related papers  (2024-01-11T09:03:47Z)
• Conformal Policy Learning for Sensorimotor Control Under Distribution Shifts [61.929388479847525]
  This paper focuses on the problem of detecting and reacting to changes in the distribution of a sensorimotor controller's observables. The key idea is the design of switching policies that can take conformal quantiles as input. We show how to design such policies by using conformal quantiles to switch between base policies with different characteristics.
  arXiv  Detail & Related papers  (2023-11-02T17:59:30Z)
• Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version) [1.3749490831384268]
  We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the problem into (a) proving that the program only leaks information via assume annotations already widely used in deductive program verification. We also show how condition (a) can be enforced by an extension of the existing program logic SecCSL, and how (b) can be checked by proving a set of simple entailments.
  arXiv  Detail & Related papers  (2023-09-07T01:51:41Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. We use state-of-the-art verification techniques to provide guarantees on the interval Markov decision process and compute a controller for which these guarantees carry over to the original control system.
  arXiv  Detail & Related papers  (2023-01-04T10:40:30Z)
• Learning Robust Output Control Barrier Functions from Safe Expert Demonstrations [50.37808220291108]
  This paper addresses learning safe output feedback control laws from partial observations of expert demonstrations. We first propose robust output control barrier functions (ROCBFs) as a means to guarantee safety. We then formulate an optimization problem to learn ROCBFs from expert demonstrations that exhibit safe system behavior.
  arXiv  Detail & Related papers  (2021-11-18T23:21:00Z)
• Learn then Test: Calibrating Predictive Algorithms to Achieve Risk Control [67.52000805944924]
  Learn then Test (LTT) is a framework for calibrating machine learning models. Our main insight is to reframe the risk-control problem as multiple hypothesis testing. We use our framework to provide new calibration methods for several core machine learning tasks with detailed worked examples in computer vision.
  arXiv  Detail & Related papers  (2021-10-03T17:42:03Z)

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.