Formally verified software countermeasures for control-flow integrity of smart card C code

Abstract : Fault attacks can target smart card programs to disrupt an execution and take control of the data or the embedded functionalities. Among all possible attacks, control-flow attacks aim at disrupting the normal execution flow. Identifying harmful control-flow attacks and designing countermeasures at the software level are tedious and tricky for developers. In this paper, we propose a methodology to detect harmful inter- and intra-procedural jump attacks at the source code level and automatically inject formally proven countermeasures into a C code. The proposed software countermeasures protect the integrity of individual statements at the granularity of single C statements. They support many control-flow constructs of the C language. The countermeasure scheme can detect an attack early either inside a control-flow construct or only at its exit. The secured source code defeats 100% of attacks that jump over at least two C source code statements. Experiments showed that the resulting code is also hardened against unexpected function calls and jump attacks at the assembly code level. Securing a source code automatically and extensively with our scheme degrades the performance. The performance overhead of our countermeasures on three well-known encryption algorithms available in C ranged from +41% to +138% on an x86 platform and from +45% to +217% on an ARM-v7 platform. However, combining code rewriting with hardening of sensitive code regions identified by the weakness detection step enables an application to be fully hardened while limiting the overhead.
Document type :
Journal articles
Complete list of metadatas

Cited literature [57 references]  Display  Hide  Download

https://hal.sorbonne-universite.fr/hal-02123836
Contributor : Karine Heydemann <>
Submitted on : Tuesday, June 4, 2019 - 10:24:11 PM
Last modification on : Friday, July 5, 2019 - 3:26:03 PM

File

HAL-heydemann-COSE19.pdf
Files produced by the author(s)

Identifiers

Citation

Karine Heydemann, Jean-François Lalande, Pascal Berthomé. Formally verified software countermeasures for control-flow integrity of smart card C code. Computers and Security, Elsevier, 2019, 85, pp.202-224. ⟨10.1016/j.cose.2019.05.004⟩. ⟨hal-02123836⟩

Share

Metrics

Record views

93

Files downloads

30