Weitere Artikel dieser Ausgabe durch Wischen aufrufen
This work is based on an earlier work: “Formal Methods for Modelling and Analysis of Single-Event Upsets” published in the proceedings of the 3rd IEEE International Workshop on Formal Methods Integration (FMi 2015) (Hansen et al. 2015).
This work was partially funded by the SENSATION project (EU FP7 grant number 318490).
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.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
Alglave, J., Fox, A.C.J., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., & Nardelli, F.Z. (2009). The semantics of POWER and ARM multiprocessor machine code. In Proceedings of workshop on declarative aspects of multicore programming (DAMP) (pp. 13–24). ACM.
ARM Ltd. (2005). ARM Architecture Reference Manual. Issue I.
Balakrishnan, G., & Reps, T.W. (2004). Analyzing memory accesses in x86 executables. In Proceedings of compiler construction (CC), lecture notes in computer science, (Vol. 2985, pp. 5–23). Springer.
Borkar, S. (2005). Designing reliable systems from unreliable components: the challenges of transistor variability and degradation. IEEE Micro, 25(6), 10–16. CrossRef
Brumley, D., Jager, I., Avgerinos, T., & Schwartz, E.J. (2011). BAP: A binary analysis platform. In Proceedings of computer aided verification (CAV), lecture notes in computer science, (Vol. 6806, pp. 463–469). Springer.
David, A., Larsen, K.G., Legay, A., Mikucionis, M., & Wang, Z. (2011). Time for statistical model checking of real-time systems. In Proceedings of computer aided verification (CAV), lecture notes in computer science, (Vol. 6806, pp. 349–355). Springer.
Halevy, A.Y., Mumick, I.S., Sagiv, Y., & Shmueli, O. (2001). Static analysis in datalog extensions. Journal of the ACM, 48(5), 971–1012. CrossRef
Hansen, R.R., Larsen, K.G., Olesen, M.C., & Wognsen, E.R. (2015). Formal methods for modelling and analysis of single-event upsets. In Proceedings of the 3rd IEEE international workshop on formal methods integration (FMi 2015), (pp. 287–294). IEEE. doi: 10.1109/IRI.2015.54. Published as part of the proceedings of the IEEE International Conference on Information Reuse and Integration (IRI 2015).
Heintze, N., & Jaffar, J. (1990). A decision procedure for a class of set constraints (extended abstract). In Proceedings of logic in computer science (LICS), (pp. 42–51).
Larsen, K.G., Pettersson, P., & Yi, W. (1997). UPPAAL In a nutshell. International Journal on Software Tools for Technology Transfer (STTT), 1(1), 134–152. CrossRef
Meola, M.L., & Walker, D. (2010). Faulty logic: reasoning about fault tolerant programs. In Proceedings of programming languages and systems (ESOP), (pp. 468–487). Springer.
Nicolescu, B., & Velazco, R. (2003). Detecting soft errors by a purely software approach: method, tools and experimental results. In Proceedings of design, automation & test in Europe (DATE), (pp. 20,057–20,063).
Nielson, F., Nielson, H.R., & Hankin, C. (1999). Principles of program analysis: Springer.
Nielson, F., Nielson, H.R., & Seidl, H. (2002). A succinct solver for ALFP. Nordic Journal of Computing, 2002(9), 335–372.
Normand, E. (1996). Single event upset at ground level. IEEE Transactions on Nuclear Science, 43(6), 2742–2750. CrossRef
Oh, N., Shirvani, P.P., & McCluskey, E.J. (2002). Control-flow checking by software signatures. IEEE Transactions on Reliability, 51(1), 111–122. CrossRef
Oh, N., Shirvani, P.P., & McCluskey, E.J. (2002). Error detection by duplicated instructions in super-scalar processors. IEEE Transactions on Reliability, 51(1), 63–75. CrossRef
Pattabiraman, K., Nakka, N., Kalbarczyk, Z., & Iyer, R.K. (2008). SymPLFIED: Symbolic program-level fault injection and error detection framework. In Proceedings of dependable systems and networks (DSN), (pp. 472–481).
Perry, F., Mackey, L.W., Reis, G.A., Ligatti, J., August, D.I., & Walker, D. (2007). Fault-tolerant typed assembly language. In Proceedings of programming language design and implementation (PLDI), (pp. 42–53). ACM.
Perry, F., & Walker, D. (2008). Reasoning about control flow in the presence of transient faults. In Proceedings of static analysis symposium (SAS), lecture notes in computer science, (Vol. 5079, pp. 332–346). Springer.
Reis, G.A., Chang, J., Vachharajani, N., Rangan, R., & August, D.I. (2005). SWIFT: software implemented fault tolerance. In Proceedings of symposium on code generation and optimization (CGO), (pp. 243–254).
Swift, G.M., Fannanesh, F.F., Guertin, S.M., Irom, F., & Millward, D.G. (2001). Single-event upset in the powerPC750 microprocessor. IEEE Transactions on Nuclear Science, 48(6), 1822–1827. CrossRef
Underwood, C.I., Ecoffet, R., Duzeffier, S., & Faguere, D. (1993). Observations of single-event upset and multiple-bit upset in non-hardened high-density SRAMs in the TOPEX/poseidon orbit. In Radiation effects data IEEE workshop, (pp. 85–92).
Wang, F., & Agrawal, V.D. (2008). Single event upset: an embedded tutorial. In Proceedings of VLSI design (VLSID), (p. 429).
Wang, N.J., Quek, J., Rafacz, T.M., & Patel, S.J. (2004). Characterizing the effects of transient faults on a High-Performance processor pipeline. In Proceedings of dependable systems and networks (DSN), (pp. 61–71).
Zhang, M., Liu, Z., Morisset, C., & Ravn, A.P. (2009). Design and verification of fault-tolerant components. In Methods, models and tools for fault tolerance, lecture notes in computer science, (Vol. 5454, pp. 57–84). Springer.
- Formal modelling and analysis of Bitflips in ARM assembly code
René Rydhof Hansen
Kim Guldstrand Larsen
Mads Chr. Olesen
Erik Ramsgaard Wognsen
- Springer US
Neuer Inhalt/© ITandMEDIA, Best Practices für die Mitarbeiter-Partizipation in der Produktentwicklung/© astrosystem | stock.adobe.com