Project topics and materials
Get Complete Project Material File(s) Now! »
Dual-rail with Precharge Logic
Balancing (or hiding) countermeasures have been employed against side channels since early 2004, with dual-rail with precharge logic. The DPL countermeasure consists in computing on a redundant representation: each bit y is implemented as a pair (yFalse, yTrue). The bit pair is then used in a protocol made up of two phases:
1. a precharge phase, during which all the bit pairs are zeroized (yFalse, yTrue) = (0, 0), such that the computation starts from a known reference state;
2. an evaluation phase, during which the (yFalse, yTrue) pair is equal to (1, 0) if it carries the logical value 0, or (0, 1) if it carries the logical value 1.
The value (yFalse, yTrue) = (1, 1) is unused. As suggested in [MAM+03], it can serve as a canary to detect a fault. Besides, if a fault turns a (1, 0) or (0, 1) value into either (0, 0) or (1, 1), then the previous functional value has been forgiven. It is a type of infection, already mentioned in [IPSW06, SBG+09]. Unlike other infective countermeasure, DPL is not scary [BG13], in that it consists in an erasure. Indeed, the mutual information between the erased and the initial data is zero (provided only one bit out of a dual pair is modified).
State of the Art
Various DPL styles for electronic circuits have been proposed. Some of them, implementing the same logical and functionality, are represented in Fig. 4.1; many more variants exist, but these four are enough to illustrate our point. The reason for the multiplicity of styles is that the indistinguishability hypothesis on the two resources holding yFalse and yTrue values happens to be violated for various reasons, which leads to the development of dedicated hardware. A first asymmetry comes from the gates driving yFalse and yTrue. In Wave Dynamic Differential Logic (WDDL) [TV04a], these two gates are different: logical or versus logical and. Other logic styles are balanced with this respect. Then, the load of the gate shall also be similar. This can be achieved by careful place-and-route constraints [TV04b, GHMP05], that take care of having lines of the same length, and that furthermore do not interfere one with the other (phenomenon called “crosstalk”). As those are complex to implement exactly for all secure gates, the Masked Dual-rail with Precharge Logic (MDPL) [PM05] style has been proposed: instead of balancing exactly the lines carrying yFalse and yTrue, those are randomly swapped, according to a random bit, represented as a pair (mFalse,mTrue) to avoid it from leaking. Therefore, in this case, not only the computing gates are the same (viz. a majority), but the routing is balanced thanks to the extra mask. However, it appeared that another asymmetry could be fatal to WDDL and MDPL: the gates pair could evaluate at different dates, depending on their input. It is important to mention that side-channel acquisitions are very accurate in timing (off-the-shelf oscilloscopes can sample at more than 1Gsample/s, i.e., at a higher rate than the clock period), but very inaccurate in space (i.e., it is difficult to capture the leakage of an area smaller than about 1mm2 without also recording the leakage from the surrounding logic). Therefore, two bits can hardly be measured separately. To avoid this issue, every gate has to include some synchronization logic. In Fig. 4.1, the “computation part” of the gates is represented in a grey box. The rest is synchronization logic. In SecLib [GCS+08], the synchronization can be achieved by Muller C-elements (represented with a symbol C [SEE98]), and act as a decoding of the inputs configuration. Another implementation, Balanced Cellbased Differential Logic (BCDL) [NBD+10], parallelize the synchronization with the computation.
Generation of DPL Protected Assembly Code
Here we present a generic method to protect assembly code against power analysis.
To achieve that we implemented a tool (See App. B.1) which transforms assembly code to make it compliant with the DPL protocol described in Sec. 4.2.2. To be as universal as possible the tool works with a generic assembly language presented in Sec. 4.3.1. The details of the code transformation are given in Sec. 4.3.2. Finally, a proof of the correctness of this transformation is presented in Sec. 4.3.3. We implemented paioli1 using the OCaml3 programming language, which type safety helps to prevent many bugs. On our present case-study, it runs in negligible time (≪ 1 second), both for DPL transformation and simulation, including balance verification. The unprotected (resp. DPL) bitslice AVR assembly file consists of 641 (resp. 1456) lines of code. We use nibble-wise jumps in each present operation, and an external loop over all rounds.
Table of contents :
0x0 Avant-propos
0.1 Contexte
0.2 Remerciements
0.3 Motivation
0x2 Abstracts
2.1 Résumé en français
2.2 Abstract
0x3 Introduction
3.1 Information Security
3.2 Cryptology
3.3 Side Channels
3.4 Fault Injection
3.5 Formal Methods
3.6 Goals of this Thesis
0x4 Formally Proved Security of Assembly Code Against Power Analysis
4.1 Introduction
4.2 Dual-rail with Precharge Logic
4.3 Generation of DPL Protected Assembly Code
4.4 Formally Proving the Absence of Leakage
4.5 Case Study: present on an ATmega163 AVR Micro-Controller
4.6 Conclusions and Perspectives
Appendices
4.A Characterization of the Atmel ATmega163 AVR Micro-Controller
4.B DPL Macro for the AVR Micro-Controller
4.C Attacks
0x5 Formal Proof of CRT-RSA Countermeasures Against Fault Attacks
5.1 Introduction
5.2 CRT-RSA and the BellCoRe Attack
5.3 Formal Methods
5.4 Study of an Unprotected CRT-RSA Computation
5.5 Study of Shamir’s Countermeasure
5.6 Study of Aumüller et al.’s Countermeasure
5.7 Conclusions and Perspective
0x6 Formal Analysis of CRT-RSA Vigilant’s Countermeasure
6.1 Introduction
6.2 Vigilant’s Countermeasure Against the BellCoRe Attack
6.3 Formal Methods
6.4 Analysis of Vigilant’s Countermeasure
6.5 Conclusions and Perspectives
Appendices
6.A Practical Feasibility of the Identified Attacks
6.B Vigilant’s Original Countermeasure
6.C Fixed Vigilant’s Countermeasure
0x7 High-Order Countermeasures Against Fault Attacks on CRT-RSA
7.1 Introduction
7.2 Fault Model
7.3 Classifying Countermeasures
7.4 The Essence of a Countermeasure
7.5 Building Better Countermeasures
7.6 Discussion: Limitations of our Formalism
7.7 Conclusions and Perspectives
Appendices
7.A Recovering d and e from (p, q, dp, dq, iq)
7.B Infective Aumüller CRT-RSA
0x8 Protecting Asymmetric Cryptography Against Fault Attacks
8.1 Introduction
8.2 Integrity Verification
8.3 The enredo Compiler
8.4 Practical Case Study: Protecting an ECSM Implementation
8.5 Conclusion and Perspectives
0x9 Conclusions and Perspectives
9.1 Conclusions
9.2 Perspectives
0xA Bibliography
