Top

Published in:

2019 | OriginalPaper | Chapter

Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs

Authors : Anja F. Karl, Robert Schilling, Roderick Bloem, Stefan Mangard

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

The increasing prevalence of soft errors and security concerns due to recent attacks like rowhammer have caused increased interest in the robustness of software against bit flips.

Arithmetic codes can be used as a protection mechanism to detect small errors injected in the program’s data. However, the accumulation of propagated errors can increase the number of bits flips in a variable - possibly up to an undetectable level.

The effect of error masking can occur: An error weight exceeds the limitations of the code and a new, valid, but incorrect code word is formed. Masked errors are undetectable, and it is crucial to check variables for bit flips before error masking can occur.

In this paper, we develop a theory of provably robust arithmetic programs. We focus on the interaction of bit flips that can happen at different locations in the program and the propagation and possible masking of errors. We show how this interaction can be formally modeled and how off-the-shelf model checkers can be used to show correctness. We evaluate our approach based on prominent and security relevant algorithms and show that even multiple faults injected at any time into any variables can be handled by our method.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Exploiting Pointer Analysis in Memory Models for Deductive Verification

next chapter Relatively Complete Pushdown Analysis of Escape Continuations

Ali, S., Mukhopadhyay, D., Tunstall, M.: Differential fault analysis of AES: towards reaching its limits. J. Cryptogr. Eng. 3, 73–97 (2013). https://doi.org/10.1007/s13389-012-0046-yCrossRef

Ball, T., Rajamani, S.K.: Bebop: a symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000). https://doi.org/10.1007/10722468_7CrossRefMATH

Bar-El, H., Choukri, H., Naccache, D., Tunstall, M., Whelan, C.: The sorcerer’s apprentice guide to fault attacks. Proc. IEEE 94, 370–382 (2006). https://doi.org/10.1109/JPROC.2005.862424CrossRef

Baumann, R.C.: Radiation-induced soft errors in advanced semiconductor technologies. IEEE Trans. Device Mater. Reliab. 5(3), 305–316 (2005)CrossRef

Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reason. 60(3), 299–335 (2018)MathSciNetCrossRef

Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16CrossRef

Boneh, D., DeMillo, R.A., Lipton, R.J.: On the importance of eliminating errors in cryptographic computations. J. Cryptol. 14, 101–119 (2001). https://doi.org/10.1007/s001450010016MathSciNetCrossRefMATH

Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63141-0_10CrossRef

Brown, D.T.: Error detecting and correcting binary codes for arithmetic operations. IRE Trans. Electron. Comput. 9, 333–337 (1960). https://doi.org/10.1109/TEC.1960.5219855CrossRef

10.

Diamond, J.M.: Checking codes for digital computers. Proc. IRE 43(4), 483–490 (1955). https://doi.org/10.1109/JRPROC.1955.277858CrossRef

11.

Fetzer, C., Schiffel, U., Süßkraut, M.: AN-encoding compiler: building safety-critical systems with commodity hardware. In: Buth, B., Rabe, G., Seyfarth, T. (eds.) SAFECOMP 2009. LNCS, vol. 5775, pp. 283–296. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04468-7_23CrossRef

12.

Given-Wilson, T., Heuser, A., Jafri, N., Lanet, J.L., Legay, A.: An automated and scalable formal process for detecting fault injection vulnerabilities in binaries (2017). https://hal.inria.fr/hal-01629135, working paper or preprint

13.

Golay, M.: Notes on digital coding. Proc. IRE 37(6), 657–657 (1949). https://doi.org/10.1109/JRPROC.1949.233620CrossRef

14.

Hamming, R.W.: Error detecting and error correcting codes. Bell Labs Tech. J. 29(2), 147–160 (1950)MathSciNetCrossRef

15.

Kim, Y., et al.: Flipping bits in memory without accessing them: an experimental study of DRAM disturbance errors. In: International Symposium on Computer Architecture – ISCA 2014, pp. 361–372 (2014)

16.

Larsson, D., Hähnle, R.: Symbolic fault injection. In: Beckert, B. (ed.) Proceedings of 4th International Verification Workshop in connection with CADE-21. CEUR Workshop Proceedings, Bremen, Germany, 15–16 July 2007, vol. 259. CEUR-WS.org (2007). http://ceur-ws.org/Vol-259/paper09.pdf

17.

Massey, J.L.: Survey of residue coding for arithmetic errors. Int. Comput. Cent. Bull. 3(4), 3–17 (1964)MathSciNet

18.

Medwed, M., Schmidt, J.-M.: Coding schemes for arithmetic and logic operations - how robust are they? In: Youm, H.Y., Yung, M. (eds.) WISA 2009. LNCS, vol. 5932, pp. 51–65. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10838-9_5CrossRef

19.

Menezes, A., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)CrossRef

20.

Meola, M.L., Walker, D.: Faulty logic: reasoning about fault tolerant programs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 468–487. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6_25CrossRef

21.

Pattabiraman, K., Nakka, N., Kalbarczyk, Z.T., Iyer, R.K.: SymPLFIED: symbolic program-level fault injection and error detection framework. IEEE Trans. Comput. 62(11), 2292–2307 (2013). https://doi.org/10.1109/TC.2012.219MathSciNetCrossRefMATH

22.

Peterson, W.W.: Error-Correcting Codes. MIT Press, Cambridge (1961)MATH

23.

Rao, T.R.N.: Biresidue error-correcting codes for computer arithmetic. IEEE Trans. Comput. 19(5), 398–402 (1970)CrossRef

24.

Rao, T.R.N., Garcia, O.N.: Cyclic and multiresidue codes for arithmetic operations. IEEE Trans. Inf. Theory 17(1), 85–91 (1971)MathSciNetCrossRef

25.

Rink, N.A., Castrillón, J.: Extending a compiler backend for complete memory error detection. In: Dencker, P., Klenk, H., Keller, H.B., Plödereder, E. (eds.) Automotive - Safety and Security 2017 - Sicherheit und Zuverlässigkeit für automobile Informations technik. LNI, Stuttgart, Germany, 30–31 Mai 2017, vol. P-269, pp. 61–74. Gesellschaft für Informatik, Bonn (2017). https://dl.gi.de/20.500.12116/147

26.

Schiffel, U.: Hardware error detection using AN-codes. Ph.D. thesis, Dresden University of Technology (2011). http://nbn-resolving.de/urn:nbn:de:bsz:14-qucosa-69872

27.

Schiffel, U.: Safety transformations: sound and complete? In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP 2013. LNCS, vol. 8153, pp. 190–201. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40793-2_18CrossRef

28.

Schilling, R., Werner, M., Mangard, S.: Securing conditional branches in the presence of fault attacks. In: Design, Automation and Test in Europe Conference and Exhibition – DATE 2018, pp. 1586–1591 (2018)

29.

Selmke, B., Brummer, S., Heyszl, J., Sigl, G.: Precise laser fault injections into 90 nm and 45 nm SRAM-cells. In: Homma, N., Medwed, M. (eds.) CARDIS 2015. LNCS, vol. 9514, pp. 193–205. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-31271-2_12CrossRef

30.

Sharma, V.C., Haran, A., Rakamaric, Z., Gopalakrishnan, G.: Towards formal approaches to system resilience. In: IEEE 19th Pacific Rim International Symposium on Dependable Computing, PRDC 2013, Vancouver, BC, Canada, 2–4 December 2013, pp. 41–50. IEEE Computer Society (2013). https://doi.org/10.1109/PRDC.2013.14

31.

Walker, D., Mackey, L.W., Ligatti, J., Reis, G.A., August, D.I.: Static typing for a faulty lambda calculus. In: Reppy, J.H., Lawall, J.L. (eds.) Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, 16–21 September 2006, pp. 38–49. ACM (2006). https://doi.org/10.1145/1159803.1159809

32.

Werner, M., Unterluggauer, T., Schaffenrath, D., Mangard, S.: Sponge-based control-flow protection for IoT devices. CoRR abs/1802.06691 (2018). http://arxiv.org/abs/1802.06691

Title: Small Faults Grow Up - Verification of Error Masking Robustness in Arithmetically Encoded Programs
Authors: Anja F. Karl
Robert Schilling
Roderick Bloem
Stefan Mangard
Publisher: Springer International Publishing
Book: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-11244-8

Electronic ISBN: 978-3-030-11245-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-11245-5_9

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner