  Side-channel attacks impose a serious threat to cryptographic algorithms,
including widely employed ones, such as AES and RSA. These attacks take
advantage of the algorithm implementation in hardware or software to extract
secret information via side channels. Software masking is a mitigation approach
against power side-channel attacks aiming at hiding the secret-revealing
dependencies from the power footprint of a vulnerable implementation. However,
this type of software mitigation often depends on general-purpose compilers,
which do not preserve non-functional properties. Moreover, microarchitectural
features, such as the memory bus and register reuse, may also leak secret
information. These abstractions are not visible at the high-level
implementation of the program. Instead, they are decided at compile time. To
remedy these problems, security engineers often sacrifice code efficiency by
turning off compiler optimization and/or performing local, post-compilation
transformations. This paper proposes Secure by Construction Code Generation
(SecCG), a constraint-based compiler approach that generates optimized yet
secure against power side channels code. SecCG controls the quality of the
mitigated program by efficiently searching the best possible low-level
implementation according to a processor cost model. In our experiments with
twelve masked cryptographic functions up to 100 lines of code on Mips32 and ARM
Thumb, SecCG speeds up the generated code from 75% to 8 times compared to
non-optimized secure code with an overhead of up to 7% compared to non-secure
optimized code at the expense of a high compilation cost. In summary, this
paper proposes a formal model to generate power side channel free low-level
code.
