A Formal Verification Approach to Safeguard Controller Variables from Single Event Upset
Ganesha, Sujit Kumar Chakrabarti
TL;DR
This paper tackles safeguarding control software from single event upsets by identifying conditionally relevant variables ($CRV$) whose perturbation would affect the safety property $Φ$. It combines static program slicing with formal verification, instrumenting the program to mimic SEUs and applying bounded model checking (via CBMC) to prune non-CRVs and reduce false positives. Experiments on several controller programs show that the CRV set is typically smaller than what static slicing alone would reveal, enabling finer-grained hardening and potential compiler-guided register allocation to cut hardware costs. The approach promises practical impact for embedded control in harsh environments by enabling partial hardening without compromising safety or performance, and lays out clear avenues for extending the method to multi-procedure programs and additional verification tools.
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.