PROOFS: Security Proofs for Embedded Systems



Thursday September 28, 2017
20:00 – 22:00 Welcome dinner at the Ambassador Hotel (more details below)
Friday September 29, 2017
08:15 – 08:50 Registration
08:50 – 09:00 Opening
09:00 – 10:00 Invited Talk 1   Chair: Jean-Luc Danger
10:00 – 10:30 Coffee break
10:30 – 12:00 First session: Formal security analysis  Chair: Amir Moradi
  • "Compositional Verification of Security Properties for Embedded Execution Platforms", by Christoph Baumann, Oliver Schwarz, and Mads Dam. (Slides)
  • "An Automated Framework for Exploitable Fault Identification in Block Ciphers – A Data Mining Approach", by Sayandeep Saha, Ujjawal Kumar, Debdeep Mukhopadhyay, and Pallab Dasgupta. (Slides)
  • "Symbolic Approach for Side-Channel Resistance Analysis of Masked Assembly Codes", by Inès Ben El Ouahma, Quentin Meunier, Karine Heydemann, and Emmanuelle Encrenaz. (Slides)
12:00 – 13:15 Lunch
13:15 – 14:15 Invited Talk 2   Chair: Ulrich Kühne
14:15 – 15:15 Second session: Secure-by construction hardware design  Chair: Ulrich Kühne
  • "Automatic Generation of HCCA Resistant Scalar Multiplication Algorithm by Proper Sequencing of Field Multiplier Operands", by Poulami Das, Debapriya Basu Roy, and Debdeep Mukhopadhyay. (Slides)
  • "Why Attackers Lose: Design and Security Analysis of Arbitrarily Large XOR Arbiter PUFs," by Nils Wisiol, Christoph Graebnitz, Marian Margraf, Tudor Soroceanu, and Benjamin Zengin. (Slides)
15:15 – 15:20 Closing

Welcome dinner

The welcome dinner takes place at the Ming Garden Restaurant at the Ambassador Hotel. The hotel is in 5 minutes walk distance of the Regent Taipei hotel, which is the venue of CHES and PROOFS:

Invited Talk 1

Oscar Reparaz
Evaluating Masking Schemes

Abstract: Masking is a popular countermeasure to thwart side-channel attacks on embedded systems. Contrary to other heuristic, ad-hoc approaches, masking carries a proof of security. However, masking is notoriously difficult to implement properly, and some proposed masking schemes, even carrying "security proofs", are eventually broken because they are flawed by design. In this talk we will revisit the security validation process of masking schemes with emphasis on tools to detect flawed schemes and flawed implementations.

Invited Talk 2

Johann Heyszl
High-Precision Hardware Attacks - Crypto under High-Precision Laser Fire and EM SCA Eavesdropping

Abstract: Hardware attacks such as side-channel analyses and fault attacks are a major threat to cryptographic implementations. Equipment of vastly different quality is used by attackers and researchers. At Fraunhofer AISEC in Munich, we focus on very high-precision laser fault injections and EM side-channel measurements. This talk introduces, highlights, and discusses the implications of such high-precision attacks on cryptographic implementations. It will feature recent results from laser-based fault injections as well as side-channel analyses and show how they brake cryptographic implementations. It will conclude by looking at implications and necessary countermeasures from such attacks.


Institut Mines-Telecom

Secure-IC S.A.S.