Abstract
Bitflips form an increasingly serious problem for the correctness and security of software and hardware, whether they occur inadvertently as soft errors or on purpose as fault injections. Error Detection Codes add redundancy and make it possible to check for faults during runtime, making systems more resilient to bitflips. Codes require data integrity to be checked regularly. Such checks need to be used sparingly, because they cause runtime overhead.
In this paper, we show how to use static verification to minimize the number of runtime checks in encoded programs. We focus on loops, because this is where it is important to avoid unnecessary checks. We introduce three types of abstractions to decide correctness: depending on (i) whether we keep track of errors precisely or of their Hamming weights, (ii) how we check whether faults can still be detected, and (iii) whether we keep track of the data or not. We show that checks in loops induce simple and natural loop invariants that we can use to speed up the verification process.
The abstractions let us trade verification time against the number of required runtime checks, allowing us to find efficient sets of integrity checks for critical program fragments in reasonable time. Preliminary experimental data shows that we can reduce the number of runtime checks by up to a factor of ten.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Our scripts are available at https://extgit.iaik.tugraz.at/scos/rv20-fault-injection-checks.
References
Barenghi, A., Breveglieri, L., Koren, I., Naccache, D.: Fault injection attacks on cryptographic devices: theory, practice, and countermeasures. Proc. IEEE 100(11), 3056–3076 (2012)
Boneh, D., DeMillo, R.A., Lipton, R.J.: On the importance of checking cryptographic protocols for faults. In: Fumy, W. (ed.) EUROCRYPT 1997. LNCS, vol. 1233, pp. 37–51. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-69053-0_4
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_16
Leonardo Bonacci. Liber Abaci. 1202
Diamond, J.M.: Checking codes for digital computers. Proc. IRE 43(4), 483–490 (1955)
Garner, H.L.: Error codes for arithmetic operations. IEEE Trans. Electron. Comput. 15(5), 763–770 (1966)
Hamming, R.W.: Error detecting and error correcting codes. Bell Syst. Tech. J. 29(2), 147–160 (1950)
Karl, A.F., Schilling, R., Bloem, R., Mangard, S.: Small faults grow up - verification of error masking robustness in arithmetically encoded programs. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 183–204. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-11245-5_9
Lomné, V., Roche, T., Thillard, A.: On the need of randomness in fault attack countermeasures - application to AES. In: Bertoni, G., Gierlichs, B. (eds.) 2012 Workshop on Fault Diagnosis and Tolerance in Cryptography, Leuven, Belgium, 9 September 2012, pp. 85–94. IEEE Computer Society (2012)
De Meyer, L., Arribas, V., Nikova, S., Nikov, V., Rijmen, V.: M&M: Masks and macs against physical attacks. Cryptology ePrint Archive, Report 2018/1195 (2018). https://eprint.iacr.org/2018/1195
Massey, J.L.: Survey of residue coding for arithmetic errors. Int. Comput. Center Bull. 3(4), 3–17 (1964)
Mukherjee, S.S., Emer, J., Reinhardt, S.K.: The soft error problem: an architectural perspective. In: 11th International Symposium on High-Performance Computer Architecture, pp. 243–247 (2005)
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_5
Peterson, W.W.: On checking an adder. IBM J. Res. Dev. 2(2), 166–168 (1958)
Rao, T.R.N.: Biresidue error-correcting codes for computer arithmetic. IEEE Trans. Comput. 19(5), 398–402 (1970)
Rao, T.R.N., Garcia, O.N.: Cyclic and multiresidue codes for arithmetic operations. IEEE Trans. Inf. Theory 17(1), 85–91 (1971)
Seker, O., Fernandez-Rubio, A., Eisenbarth, T., Steinwandt, R.: Extending glitch-free multiparty protocols to resist fault injection attacks. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2018(3), 394–430 (2018)
Schilling, R., Werner, M., Mangard, S.: Securing conditional branches in the presence of fault attacks. In: 2018 Design, Automation & Test in Europe Conference & Exhibition, pp. 1586–1591. IEEE (2018)
Volder, J.: The cordic computing technique. In: Papers presented at the the 3–5 March 1959, Western Joint Computer Conference, pp. 257–261 (1959)
Werner, M., Unterluggauer, T., Schaffenrath, D., Mangard, S.: Sponge-based control-flow protection for IoT devices. In: 2018 IEEE European Symposium on Security and Privacy, pp. 214–226 (2018)
Yuce, B., Schaumont, P., Witteman, M.: Fault attacks on secure embedded software: threats, design, and evaluation. J. Hardware Syst. Secur. 2(2), 111–130 (2018)
Acknowledgements
We would like to thank Stefan Mangard and Robert Schilling for contributing their expertise on error correcting codes. We gratefully acknowledge the support of Graz University of Technology through the LEAD Project “Dependable Internet of Things in Adverse Environments”.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Maderbacher, B., Karl, A.F., Bloem, R. (2020). Placement of Runtime Checks to Counteract Fault Injections. In: Deshmukh, J., Ničković, D. (eds) Runtime Verification. RV 2020. Lecture Notes in Computer Science(), vol 12399. Springer, Cham. https://doi.org/10.1007/978-3-030-60508-7_13
Download citation
DOI: https://doi.org/10.1007/978-3-030-60508-7_13
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-60507-0
Online ISBN: 978-3-030-60508-7
eBook Packages: Computer ScienceComputer Science (R0)