ICE-TCS seminar: Formal Methods for Modelling and Analysis of Single-Event Upsets
Date/Time: Friday, 11 September 2015 at 2pm
Place: Room M.102
Speaker: Mads Chr. Olesen (Aalborg University, Denmark)
Title: Formal Methods for Modelling and Analysis of Single-Event Upsets
Abstract: When a high-energy particle such as a proton strikes a CPU, the impact may result in the corruption of a data register on the CPU.
Such a single-event upset (SEU), in which a random bit is flipped in the content of a data register, can lead to critical errors in the execution of a program. This is particularly problematic for security- or safety-critical systems where such errors may have grave consequences.
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.
We use this framework to formally prove the soundness of a static analysis enforcing so-called blue/green separation in a given program.
Blue/green separation is a replication based technique for making a program fault-tolerant with respect to data-flow SEUs; however, full coverage requires special hardware support. We further use our semantic framework for deriving program fragments, so-called gadgets, for partial blue/green separation without special hardware. Finally, we illustrate how to apply statistical model checking in our framework to model and quantify faults that go well beyond data-flow SEUs and can provide statistics on the level of fault-tolerance of a program. We use this to provide evidence that our suggested program modifications significantly decrease the probability of such errors going undetected.
(Joint work with: René Rydhof Hansen, Kim Guldstrand Larsen and Erik Ramsgaard Wognsen)