Advertisement

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

  • Anja F. KarlEmail author
  • Robert Schilling
  • Roderick Bloem
  • Stefan Mangard
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)

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.

Keywords

Formal verification Fault injection Error detection codes Arithmetic codes Error masking 

References

  1. 1.
    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-yCrossRefGoogle Scholar
  2. 2.
    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_7CrossRefzbMATHGoogle Scholar
  3. 3.
    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.862424CrossRefGoogle Scholar
  4. 4.
    Baumann, R.C.: Radiation-induced soft errors in advanced semiconductor technologies. IEEE Trans. Device Mater. Reliab. 5(3), 305–316 (2005)CrossRefGoogle Scholar
  5. 5.
    Beyer, D., Dangl, M., Wendler, P.: A unifying view on SMT-based software verification. J. Autom. Reason. 60(3), 299–335 (2018)MathSciNetCrossRefGoogle Scholar
  6. 6.
    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_16CrossRefGoogle Scholar
  7. 7.
    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/s001450010016MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    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_10CrossRefGoogle Scholar
  9. 9.
    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.5219855CrossRefGoogle Scholar
  10. 10.
    Diamond, J.M.: Checking codes for digital computers. Proc. IRE 43(4), 483–490 (1955).  https://doi.org/10.1109/JRPROC.1955.277858CrossRefGoogle Scholar
  11. 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_23CrossRefGoogle Scholar
  12. 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. 13.
    Golay, M.: Notes on digital coding. Proc. IRE 37(6), 657–657 (1949).  https://doi.org/10.1109/JRPROC.1949.233620CrossRefGoogle Scholar
  14. 14.
    Hamming, R.W.: Error detecting and error correcting codes. Bell Labs Tech. J. 29(2), 147–160 (1950)MathSciNetCrossRefGoogle Scholar
  15. 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)Google Scholar
  16. 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. 17.
    Massey, J.L.: Survey of residue coding for arithmetic errors. Int. Comput. Cent. Bull. 3(4), 3–17 (1964)MathSciNetGoogle Scholar
  18. 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_5CrossRefGoogle Scholar
  19. 19.
    Menezes, A., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)CrossRefGoogle Scholar
  20. 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_25CrossRefGoogle Scholar
  21. 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.219MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Peterson, W.W.: Error-Correcting Codes. MIT Press, Cambridge (1961)zbMATHGoogle Scholar
  23. 23.
    Rao, T.R.N.: Biresidue error-correcting codes for computer arithmetic. IEEE Trans. Comput. 19(5), 398–402 (1970)CrossRefGoogle Scholar
  24. 24.
    Rao, T.R.N., Garcia, O.N.: Cyclic and multiresidue codes for arithmetic operations. IEEE Trans. Inf. Theory 17(1), 85–91 (1971)MathSciNetCrossRefGoogle Scholar
  25. 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. 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. 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_18CrossRefGoogle Scholar
  28. 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)Google Scholar
  29. 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_12CrossRefGoogle Scholar
  30. 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. 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. 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

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Anja F. Karl
    • 1
    Email author
  • Robert Schilling
    • 1
    • 2
  • Roderick Bloem
    • 1
  • Stefan Mangard
    • 1
  1. 1.Graz University of TechnologyGrazAustria
  2. 2.Know-Center GmbHGrazAustria

Personalised recommendations