PROOFS: Security Proofs for Embedded Systems

Leuven, Belgium — Thursday, September 13rd, 2012

Program

8h15 – 9h00	Registration, at College de Valk
9h00 – 9h15	Opening — Welcome, presentation of PROOFS
9h15 – 10h15	Invited talk #1 Chair: Stefan Mangard
• "Understanding the reasons for the side-channel leakage is indispensable for secure design", by Werner Schindler
10h15 – 10h30	Coffee break
10h30 – 12h00	Submitted papers session Chair: Svetla Nikova
• "A formal study of two physical countermeasures against side channel attacks", by Sébastien Briais, Sylvain Guilley and Jean-Luc Danger
• "Formal verification of an implementation of CRT-RSA Vigilant's algorithm", by Maria Christofi, Boutheina Chetali, Louis Goubin and David Vigilant
• "Toward A Taxonomy of Communications Security Models", by Mark Brown
12h00 – 13h30	Lunch, at Alma cafeteria
13h30 – 14h30	Invited talk #2 Chair: Éliane Jaulmes
• "Toward Formal Design of Cryptographic Processors Based on Galois Field Arithmetic", by Naofumi Homma
14h30 – 15h30	Invited talk #3 Chair: Louis Goubin
• "Analysing Cryptographic Hardware Interfaces with Tookan", by Graham Steel
15h30 – 16h00	Coffee break
16h00 – 16h30	Round-table and Q&A with the audience
16h30 – 16h35	Wrap-up

Please click on the talk titles to access the presentation slides.

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

Accepted papers (which will be published in the issue 3 of Springer JCEN 2013):

"A formal study of two physical countermeasures against side channel attacks", by Sébastien Briais, Sylvain Guilley and Jean-Luc Danger.
DOI: 10.1007/s13389-013-0054-6.
"Toward A Taxonomy of Communications Security Models", by Mark Brown.
DOI: 10.1007/s13389-013-0058-2.
"Formal verification of an implementation of CRT-RSA Vigilant’s algorithm", by Maria Christofi, Boutheina Chetali, Louis Goubin and David Vigilant.
DOI: 10.1007/s13389-013-0049-3.

Invited talks will be given by:

Prof. Werner Schindler, BSI and CASED (Germany).
Title: "Understanding the reasons for the side-channel leakage is indispensable for secure design"
- Abstract: In the last one and a half decades side-channel analysis, and in particular power analysis, has become a very important topic in both academia and industry. Hardening security implementations against power attacks has become a matter of course. The strength of an implementation is usually rated on basis of its resistance against particular types of power attacks (e.g., DPA, CPA, template attacks). The stochastic approach combines engineering's expertise with advanced stochastic methods. Compared to template attacks this reduces the profiling workload drastically. Apart from (possibly) providing a successful attack the stochastic approach quantifies the side-channel leakage with regard to a vector space basis, and it allows to verify leakage model assumptions. This provides useful information, which supports target-oriented (re-)design.
Prof. Naofumi Homma, Associate Professor, Graduate School of Information Sciences, Tohoku University (Japan).
Title: "Toward Formal Design of Cryptographic Processors Based on Galois Field Arithmetic"
- Abstract: The importance of Galois field (GF) arithmetic circuits has been rapidly increasing as the application of such circuits to security primitives, such as cryptographic systems and error correction codes, has expanded together with the recent widespread adoption of embedded devices. This talk presents a formal approach to designing cryptographic processor datapaths on the basis of arithmetic circuits over GFs. The proposed method describes GF arithmetic circuits in the form of hierarchical graph structures, where nodes represent sub-circuits whose functions are defined by arithmetic formulae over GFs, and edges represent data dependency between nodes. The graph representation can be formally verified through symbolic computation techniques. The capability of the proposed approach is demonstrated through an experimental design of a 128-bit AES (Advanced Encryption Standard) datapath. The results show that the proposed method can describe the 128-bit datapath in a formal manner, as well as that complete verification of such a datapath can be carried out within a short period of time.
Dr. Graham Steel, Research Fellow, INRIA (France).
Title: "Analysing Cryptographic Hardware Interfaces with Tookan"
- Abstract: Cryptographic hardware offers access to its functionality via an application program interface (API). Designing such interfaces so that they offer flexible functionality but cannot be abused to reveal keys or secrets has proved to be extremely difficult, with a number of published vulnerabilities in widely-used APIs appearing over the last decade. This talk will discuss recent research on the use of formal methods to specify and verify cryptographic device interfaces in order to either detect flaws or prove security properties. We will focus on the example of RSA PKCS#11, the most widely used interface for cryptographic devices. We will demonstrate a tool, Tookan, which can reverse engineer the particular configuration of PKCS#11 in use on some device under test, construct a model of the device's functionality, and call a model checker to search for attacks. If an attack is found, it can be executed automatically on the device. Tookan can also be used to prove security in its abstract model. We will also discuss results on extending Tookan to test for padding oracle attacks.