PROOFS: Security Proofs for Embedded Systems

Program

The program is aligned in terms of coffee breaks and lunch with that of the 4th workshop on secure hardware and security evaluation (TRUDEVICE).

Access to the papers requires the password given at the workshop.

Wednesday September 16, 2015
17:30 – 22:00	Welcome dinner in Rennes (see details at the bottom of the page)
Thursday September 17, 2015
8:30 – 8:50	Registration
8:50 – 9:00	Opening (slides)
9:00 – 10:00	First keynote Chair: Sylvain Guilley Jean-Louis Lanet, "Black hat can also benefits from formal method" (Presentation slides)
10:00 – 10:30	Coffee break
10:30 – 12:00	First session Chair: Sylvain Guilley Shoei Nashimoto, Naofumi Homma, Yu-Ichi Hayashi and Takafumi Aoki, "Buffer Overflow Attack with Multiple Fault Injection and a Proven Countermeasure" (Presentation slides) Bruno Robisson, Michel Agoyan, Patrick Soquet, Sébastien Le-Henaff, Franck Wajsbürt, Pirouz Bazargan-Sabet and Guillaume Phan, "Smart Security Management in Secure Devices" (Presentation slides) Florian Lugou, Ludovic Apvrille and Aurélien Francillon, "Toward a Methodology for Unified Verification of Hardware/Software Co-designs" (Presentation slides)
12:00 – 13:30	Lunch
13:30 – 14:30	Second keynote Chair: Bruno Robisson Pascal Cuoq, "Formal verification at the source level that execution time does not depends on secrets — inasmuch as this means anything" (Presentation slides (TXT format))
14:30 – 15:00	Coffee break
15:00 – 15:40	Second session Chair: Naofumi Homma Sabine Azzi, Bruno Barras, Maria Christofi and David Vigilant, "Using Linear Codes as a Fault Countermeasure for Nonlinear Operations: Application to AES and Formal Verification" (Presentation slides) Laurent Sauvage, Tarik Graba and Thibault Porteboeuf, "Multi-Level Formal Verification, a New Approach Against Fault Injection Attack" (Presentation slides)
15:40 - 15:45	Farewell (slides)

Two keynote talks:

Jean-Louis Lanet, INRIA, Rennes
- Title: Black hat can also benefits from formal method
- Abstract: The Pole Excellence Cyber (PEC) in Brittany promotes researches in the Cyber Security field and in particular vulnerability threat analysis. In this presentation, we will in a first part develop a new software attack to retrieve a key in a smart card. This is based on several assumptions and in the second part we will evaluate the coverage of this hypotheses. One of them relies on fault attack. We will present how designed-for-polymorphism code can be a good candidate to implement this attack. Then, we will try to consider how this could be applicable at the native layers.
Pascal Cuoq, TrustInSoft
- Title: Formal verification at the source level that execution time does not depends on secrets — inasmuch as this means anything
- Abstract: Among all the side-channel attacks applicable to software cryptographic implementations running on general-purpose hardware, timing attacks are the ones that the community can hope to address in practice. And the community needs to address these, since unlike other, less practical side-channels, time can be measured remotely and without special equipment. This presentation will retrace the history of the mechanical verification of the non-dependence on secrets of the execution time of a piece of cryptographic software since Adam Langley's ctgrind, and review current issues with cryptographic implementations ranging from add-xor-rol ciphers with secret-independent execution time by design to more complex primitives and protocols with their many trade-offs. An open-source tool for C based on sound static analysis will be introduced.

Welcome dinner organization

17:30 : Bus shuttle leaves from the "grand large convention center" to Rennes.
18:30 : Welcome cocktail & dinner, while enjoying music with a DJ and an open bar.
21:00 & 21:30 : Two bus shuttle services leave Rennes, and return to Saint-Malo. Drop off at specific hotels upon request.