PROOFS 2024

The workshop takes place on Wednesday September 4 in the morning (local time).

Abstract: True random number generators (TRNGs) are essential in cryptography. They are used to generate cryptographic keys, but also nonces (numbers used once), padding values, and masks in countermeasures against side-channel attacks. Designing a good TRNG remains a challenge, starting with the choice of a robust physical source of randomness, selection of the randomness extraction method, the in-depth analysis of the principle and continuing with the design and verification of the parameterized stochastic model ensuring the high level of entropy and or the dedicated online tests based on the model. We will illustrate this TRNG development process on many positive and negative examples.

Bio: Viktor Fischer is an emeritus professor at Jean Monnet University in Saint-Etienne, France and part-time professor at Czech Technical University in Prague, Czech republic. His research interests include security of cryptographic embedded systems and in particular of random number generators aimed at cryptographic applications.

Abstract: In this talk, we recall our long and winding journey towards side-channel secure implementations of PQC, at the example of CRYSTALS-Kyber (ML-KEM) and CRYSTALS-Dilithium (ML-DSA). Starting from the first results in 2018, we discuss the challenges we faced, false assumptions and how to overcome them, and our interactions with the official NIST standardization effort.

Bio: Tobias Schneider is a principal security concept engineer at NXP Semiconductors. His research interests include the physical security of cryptographic implementations, in particular of post-quantum cryptography, and cyber resilience.

Abstract: This study presents a formal verification method for Galois field arithmetic circuits based on computer algebra. While previous studies have explored computer-algebra-based techniques for verifying the equivalence of circuit specifications and netlists for arithmetic circuits over GF(2^m), these methods primarily focused on verifying combinational circuit components and have not been applied to sequential circuit components involving control-related states (that is, registers). To address this issue, this study proposes an extension of a computer-algebra-based method for equivalence checking of arithmetic circuits that incorporate sequential circuit parts associated with behavior control. Our approach involves integrating a circuit function representation based on zero-suppressed binary decision diagrams (ZDD) with a symbolic execution method. Through verification experiments conducted on a series of sequential multipliers with parallel output (SMPO) over GF(2^m), we demonstrate the effectiveness of our proposed method in verifying sequential arithmetic circuits within a practical timeframe.

Abstract: Numerous machines using DRAM chips as main memory are vulnerable to the Rowhammer attack, which can be used as a tool for privilege escalation. The existing mitigation techniques either require complex hardware implementation or have a high performance cost. A potential improvement would be to implement a detection mechanism and trigger performance-costly mitigation only in the case of attack detection. In this paper, we study this defence method on three systems using Intel Skylake, Tiger Lake and Alder Lake processors, and DDR4 and DDR5 DRAM chips as main memory. We execute four variants of the attack code on these machines and observe their traces in the hardware. We use the PAPI library and perf to periodically read the generated traces from the machines' hardware performance counters. Finally, we train machine learning models such as logistic regression and decision trees to distinguish attack and no-attack behaviour. Our best models achieve accuracy above 99.6% and perform the classification of both 50us and 1ms samples in software fast enough (less than 0.5us per sample) to detect the attack before completion.

Abstract: Side Channel Attacks (SCA) consist in leakage analysis on a device running a cryptographic algorithm. This paper provides a new approach to perform such attacks. Unlike most SCA that are based on statistical attacks, this paper provides a new approach based on wavelet analysis. This approach holds in mono- and multivariate contexts. Its interest lies in the efficiency of this attack compared to the most known attacks (correlation power analysis and template attacks). Furthermore, compared to these attacks, our approach is better in term of computational complexity and in term number of traces to recover the key. In fact the time complexity was at least quasilinear in the number of possible subkeys whereas it is linear with our approach. The attack was experimented on two cards, an 8-bits ATMega 163 smart card and a 16-bits MSP430 platform, that run a software AES.