PROOFS: Security Proofs for Embedded Systems

PROOFS 2013

Program

8h30 – 9h00 Registration at Corwin Pavilion lobby (same location as the CHES registration), coffee. The workshop will take place in Flying A Room
9h00 – 9h15 Opening — Welcome, presentation of PROOFS 2013 [slides]
9h15 – 10h15 Session 1: formal analysis of fault attacks   Chair: Rob Bekkers
• "Formal verification of a software countermeasure against instruction skip attacks", Abstract: Fault attacks against embedded circuits enabled to define many new attack paths against secure circuits. Every attack path relies on a specific fault model which defines the type of faults that the attacker can perform. On embedded processors, a fault model in which an attacker is able to skip an assembly instruction is practical and has been obtained by using several fault injection means. To handle this issue, some countermeasure schemes which rely on temporal redundancy have been proposed. Nevertheless, double fault injection in a long enough time interval is practical and can bypass those countermeasure schemes. Some fine-grained other countermeasure schemes have been proposed for specific instructions. However, to the best of our knowledge, no approach that enables to secure a generic assembly program in order to make it fault-tolerant to instruction skip attacks has been formally proven yet. In this paper, we provide a fault-tolerant replacement sequence for every instruction of the whole Thumb2 instruction set and provide a formal proof of this fault tolerance. This simple transformation enables to add a reasonably good security level to an embedded program and makes practical fault injection attacks much harder to achieve.
Keywords: microcontroller, fault attack, instruction skip, countermeasure, formal proof. by Karine Heydemann, Nicolas Moro, Emmanuelle Encrenaz and Bruno Robisson [slides].
• "A formal proof of countermeasures against fault injection attacks on CRT-RSA", Abstract: In this article, we describe a methodology that aims at either breaking or proving the security of CRT-RSA algorithms against fault injection attacks. In the specific case-study of BellCoRe attacks, our work bridges a gap between formal proofs and implementation-level attacks. We apply our results to three versions of CRT-RSA, namely the naive one, that of Shamir, and that of Aumüller et al. Our findings are that many attacks are possible on both the naive and the Shamir implementations, while the implementation of Aumüller et al. is resistant to all fault attacks with one fault. However, we show that the countermeasure is not minimal, since two tests out of seven are redundant and can simply be removed.
Keywords: RSA, CRT, fault injection, BellCoRe attack, formal proof, OCaml. by Pablo Rauzy and Sylvain Guilley [slides]
10h15 – 10h30 Coffee break
10h30 – 11h30 Session 2: formal analysis of countermeasures against side-channel attacks   Chair: Jean-Pierre Seifert
• "Towards Fresh Re-Keying with Leakage-Resilient PRFs: Cipher Design Principles and Analysis", Abstract: Leakage-resilient cryptography aims at developing new algorithms for which physical security against side-channel attacks can be formally analyzed. Following the work of Dziembowski and Pietrzak at FOCS 2008, several symmetric cryptographic primitives have been investigated in this setting. Most of them can be instantiated with a block cipher as underlying component. Such an approach naturally raises the question whether certain block ciphers are better suited for this purpose. In order to answer this question, we consider a leakage-resilient re-keying function, and evaluate its security at different abstraction levels. That is, we study possible attacks exploiting specific features of the algorithmic description, hardware architecture and physical implementation of this construction. These evaluations lead to two main outcomes. First, we complement previous works on leakage-resilient cryptography and further specify the conditions under which they actually provide physical security. Second, we take advantage of our analysis to extract new design principles for block ciphers to be used in leakage-resilient primitives. While our investigations focus on side-channel attacks in the first place, we hope these new design principles will trigger the interest of symmetric cryptographers to design new block ciphers combining good properties for secure implementations and security against black box (mathematical) cryptanalysis.
Keywords: resilience approaches to side-channel attacks, block cipher design, leakage-resilient PRFs, parallel implementations, electromagnetic analysis. by Sonia Belaid, Fabrizio De Santis, Johann Heyszl, Stefan Mangard, Marcel Medwed, Jörn-Marc Schmidt, François-Xavier Standaert and Stefan Tillich [slides].
• "Understanding the Limitations and Improving the Relevance of SPICE Simulations in Side-Channel Security Evaluations", Abstract: Simulation is a very powerful tool for hardware designers. It generally allows a preliminary evaluation of chips performances before their final tape out. As security against side-channel attacks is an increasingly important issue for cryptographic devices, simulation also becomes a desirable option for preliminary evaluation in this case. However, its relevance highly depends on the proper modeling of all the attack peculiarities. For example, several works in the literature directly exploit SPICE-like simulations without considering measurement peripherals. But the outcome of such analyses may be questionable, as witnessed by the recent results of Renauld et al. at CHES 2011, which showed how far the power traces of an AES S-box implemented using a dynamic and differential logic style fabricated in 65 nm CMOS technology can lie from their post-layout simulations. One important difference was found in the linear dependencies between the (simulated and actual) traces and the Sbox input and output bits. While simulations exhibited highly non-linear traces, actual traces were much more linear. As linearity is a crucial parameter for the application of non-profiled side-channel attacks (which are only possible under the assumption of “sufficiently linear leakages”), this observation motivated us to study the reasons of such differences. Consequently, this work further discusses the relevance of simulation in security evaluations and highlights its high dependency on the proper modeling of measurement setups. For this purpose, we present a generic approach to build an adequate model to represent measurements artifacts based upon real data from equipment providers for our AES S-box case study. Next, we illustrate the transformation of simulated leakages, from highly non-linear to reasonably linear, exploiting our model and regression-based side-channel analysis. While improving the relevance of simulations in security evaluations, our results also raise doubts regarding the possibility to design dual-rail implementations with highly non-linear leakages.
Keywords: formal verification of VLSI designs at netlist-level, Side-channel analysis, AES S-box, Equivalent circuit modeling. by Dina Kamel, Mathieu Renauld, Denis Flandre and François-Xavier Standaert [slides]
11h30 – 12h30 Invited keynote talk #1  
• "Better Provability through Computer Architecture", Abstract: Computer performance has doubled many times over during the past 40 years, but the very techniques used to achieve these performance gains have made it increasingly difficult to build hardware/software systems with cross-cutting properties such as determinism, real-time guarantees, and (perhaps most critically) security. As we move towards increasingly complex chips, with more and more hidden state (e.g., predictors, caches, modes), these properties are only becoming harder to realize. This trend significantly impedes progress in the development of our most safety-critical embedded systems such as those found in medical, avionic, and automotive systems. What if we started from scratch? What if we built processors from the ground up with an eye towards both the new complex reality in which we live and the radical improvements in automated formal methods we now have access to? How much better could we do? Dr. Sherwood will discuss his and his collaborators efforts to explore this question through the creation of a complete prototype system including: a new instruction set architecture, a synthesizable hardware designs, a new programming language and compiler, a custom micro-kernel generator, interfaces to existing I/O devices, and ultimately non-trivial trustworthy applications. by Timothy Sherwood
12h30 – 14h00 Lunch
14h00 – 15h00 Session 3: Formal design methods   Chair: Kris Gaj
• "Formal Design of Composite Physically Unclonable Function", Abstract: Physically Unclonable Function (PUF) in silicon is the embodiment of an instance-specific challenge-response mapping, that exploits random manufacturing process variation in an integrated circuit (IC) to determine the mapping. PUF designs proposed in the recent literature vary widely in diverse characteristics such as hardware resource requirement, reliability, entropy, and robustness against mathematical cloning. Most of the standalone PUF designs suffer from either poor performance profile or huge resource-overhead. This work presents a PUF design paradigm, termed as PUF Synthesis, that exploits the smaller PUFs (both strong and weak) as design building blocks to define a composite PUF having large challenge-space and good performance profile. A formal framework for PUF synthesis has also been developed to guide the composition in systematic fashion. The notion of PUF synthesis has been validated by the implementation of a composite PUF that combines two widely studied PUFs, Arbiter PUF (APUF) and Ring Oscillator PUF (ROPUF), and inherits the desirable characteristics of both. Resource requirement of this target design with 60-bit challenge is lesser than a standalone 10-bit ROPUF, while its robustness against model building attack is much superior compared to APUF. Implementation of the proposed design on Altera Cyclone-III Field Programmable Gate Array (FPGA) shows 47% uniqueness and 91% reliability on average.
Keywords: Physically Unclonable Function, PUF synthesis, composite PUF, optimized composition. by Durga Prasad Sahoo, Debdeep Mukhopadhyay and Rajat Subhra Chakraborty (short talk) [slides]
• "A hierarchical graph-based approach to generating formally-proofed Galois-field multipliers", Abstract: This paper presents a formal design of Galois-field multipliers based on a graph representation called Galois-Field Arithmetic Circuit Graph (GF-ACG). We focus on one of the optimal GF(2m) parallel multipliers, called Mastrovito Multiplier, and derive the hierarchical description from the original flatten description. The hierarchical description can be verified formally within a practical time even if the data width is more than 128. This paper also applies the hierarchical design to an automatic generation of formally-proofed GF parallel multipliers for any irreducible polynomial.
Keywords: arithmetic circuits, formal verification, hierarchical description, computer algebra. by Kotaro Okamoto, Naofumi Homma and Takafumi Aoki (short talk) [slides].
• "Trojan-Resilient Circuits", Abstract: Integrated circuits (ICs) can contain malicious logic or backdoors, known as hardware trojans, that may impede them from functioning properly. These hardware trojans include the recent bug attacks due to Biham et al. In order to protect ICs against such hardware trojans and the bug attacks, we present an effective method to efficiently construct "trojan-resilient" circuits. Therefore, we revisit the fundamental work on fault-tolerant circuits by Gál and Szegedy. We extend their attack model; and from this extended adversary scenario we derive a mathematical definition of "IC resilience" against well-defined hardware trojans. In our model we allow an all-powerful adversary to modify a constant fraction of the gates and wires at each level of the resilient circuit in an arbitrary way. We prove that every Boolean circuit can be transformed into another Boolean circuit with the same functionality as the original circuit even in the presence of an adversary tampering with the "resilient" circuit. The transformation is polynomial time computable and yields a circuit, which has a logarithmic depth in the size of the original circuit. To the best of our knowledge this is the first work to counteract hardware trojans with a rigorous mathematical security proof — backed up by a practical and meaningful model.
Keywords: bug attacks, error-correcting codes, hardware backdoors and trojans, probabilistically checkable proofs, reliable and secure circuits, resilient circuit design. by Christoph Bayer and Jean-Pierre Seifert (short talk) [slides].
15h00 – 15h25 "Work in Progress" session
15h25 – 15h30 Wrap-up [slides]

The full day agenda is also available as PDF there: proofs_program.pdf.

Submissions accepted for regular oral presentation:

Submissions accepted for short oral presentation: The invited talk will be given by:

PROOFS 2013


Sponsors


TELECOM-ParisTech
Secure-IC S.A.S.