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

International audienceFault 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