Formal modelling and analysis of Bitflips in ARM assembly code

René Rydhof Hansen (), Kim Guldstrand Larsen (), Mads Chr. Olesen () and Erik Ramsgaard Wognsen ()
Additional contact information
René Rydhof Hansen: Aalborg University
Kim Guldstrand Larsen: Aalborg University
Mads Chr. Olesen: Aalborg University
Erik Ramsgaard Wognsen: Aalborg University

Information Systems Frontiers, 2016, vol. 18, issue 5, No 6, 909-925

Abstract: Abstract Bitflips, or single-event upsets (SEUs) as they are more formally known, may occur for instance when a high-energy particle such as a proton strikes a CPU and thereby corrupting the contents of an on-chip register, e.g., by randomly flipping one or more bits in that register. Such random changes in central registers may lead to critical failure in the execution of a program, which is especially problematic for safety- or security-critical applications. Even though SEUs are well studied in the literature, relatively little attention have been given to the formal modelling of SEUs and the application of formal methods to mitigate the consequences of SEUs. In this paper we develop a formal semantic framework for easy formal modelling of a large variety of SEUs in a core assembly language capturing the essential features of the ARM assembly language. Based on the semantic framework, we derive and formally prove correct a static analysis that enforces so-called blue/green separation in a given program. Static blue/green separation is a language-based fault detection technique relying on inlined replication of critical code. A program that has proper blue/green separation is shown to be fault-tolerant with respect SEUs in data registers. However, this technique requires specialised hardware support in order to achieve full coverage. We therefore use our semantic framework to further develop so-called gadgets, essentially small code fragments that emulate the behaviour of blue/green instructions in a safe manner. The gadgets allow us to achieve partial blue/green separation without specialised hardware support. Finally, we show how our semantic framework can be used to extract timed-automata models of ARM assembler code programs. We then apply statistical model checking to these timed-automata models enabling us to model, analyse, and quantify program behaviour in the presence of fault models that go well beyond data-flow SEUs, e.g., bitflips in program counters or in the code itself. We use this approach to provide evidence that our suggested program modifications, i.e., the use of gadgets, significantly decrease the probability of such faults going undetected.

Keywords: Single-event upsets; Biflips; Static analysis; Model checking (search for similar items in EconPapers)
Date: 2016
References: View complete reference list from CitEc
Citations: View citations in EconPapers (1)

Downloads: (external link)
http://link.springer.com/10.1007/s10796-016-9665-7 Abstract (text/html)
Access to the full text of the articles in this series is restricted.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:spr:infosf:v:18:y:2016:i:5:d:10.1007_s10796-016-9665-7

Ordering information: This journal article can be ordered from
http://www.springer.com/journal/10796

DOI: 10.1007/s10796-016-9665-7

Access Statistics for this article

Information Systems Frontiers is currently edited by Ram Ramesh and Raghav Rao

More articles in Information Systems Frontiers from Springer
Bibliographic data for series maintained by Sonal Shukla () and Springer Nature Abstracting and Indexing ().