scholarly journals A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs

2021 ◽  
Vol 30 (3) ◽  
pp. 1-42
Author(s):  
Pengfei Gao ◽  
Hongyi Xie ◽  
Fu Song ◽  
Taolue Chen

Side-channel attacks, which are capable of breaking secrecy via side-channel information, pose a growing threat to the implementation of cryptographic algorithms. Masking is an effective countermeasure against side-channel attacks by removing the statistical dependence between secrecy and power consumption via randomization. However, designing efficient and effective masked implementations turns out to be an error-prone task. Current techniques for verifying whether masked programs are secure are limited in their applicability and accuracy, especially when they are applied. To bridge this gap, in this article, we first propose a sound type system, equipped with an efficient type inference algorithm, for verifying masked arithmetic programs against higher-order attacks. We then give novel model-counting-based and pattern-matching-based methods that are able to precisely determine whether the potential leaky observable sets detected by the type system are genuine or simply spurious. We evaluate our approach on various implementations of arithmetic cryptographic programs. The experiments confirm that our approach outperforms the state-of-the-art baselines in terms of applicability, accuracy, and efficiency.

Author(s):  
Annapurna Valiveti ◽  
Srinivas Vivek

Masking using randomised lookup tables is a popular countermeasure for side-channel attacks, particularly at small masking orders. An advantage of this class of countermeasures for masking S-boxes compared to ISW-based masking is that it supports pre-processing and thus significantly reducing the amount of computation to be done after the unmasked inputs are available. Indeed, the “online” computation can be as fast as just a table lookup. But the size of the randomised lookup table increases linearly with the masking order, and hence the RAM memory required to store pre-processed tables becomes infeasible for higher masking orders. Hence demonstrating the feasibility of full pre-processing of higher-order lookup table-based masking schemes on resource-constrained devices has remained an open problem. In this work, we solve the above problem by implementing a higher-order lookup table-based scheme using an amount of RAM memory that is essentially independent of the masking order. More concretely, we reduce the amount of RAM memory needed for the table-based scheme of Coron et al. (TCHES 2018) approximately by a factor equal to the number of shares. Our technique is based upon the use of pseudorandom number generator (PRG) to minimise the randomness complexity of ISW-based masking schemes proposed by Ishai et al. (ICALP 2013) and Coron et al. (Eurocrypt 2020). Hence we show that for lookup table-based masking schemes, the use of a PRG not only reduces the randomness complexity (now logarithmic in the size of the S-box) but also the memory complexity, and without any significant increase in the overall running time. We have implemented in software the higher-order table-based masking scheme of Coron et al. (TCHES 2018) at tenth order with full pre-processing of a single execution of all the AES S-boxes on a ARM Cortex-M4 device that has 256 KB RAM memory. Our technique requires only 41.2 KB of RAM memory, whereas the original scheme would have needed 440 KB. Moreover, our 8-bit implementation results demonstrate that the online execution time of our variant is about 1.5 times faster compared to the 8-bit bitsliced masked implementation of AES-128.


Author(s):  
Prasanna Ravi ◽  
Sujoy Sinha Roy ◽  
Anupam Chattopadhyay ◽  
Shivam Bhasin

In this work, we demonstrate generic and practical EM side-channel assisted chosen ciphertext attacks over multiple LWE/LWR-based Public Key Encryption (PKE) and Key Encapsulation Mechanisms (KEM) secure in the chosen ciphertext model (IND-CCA security). We show that the EM side-channel information can be efficiently utilized to instantiate a plaintext checking oracle, which provides binary information about the output of decryption, typically concealed within IND-CCA secure PKE/KEMs, thereby enabling our attacks. Firstly, we identified EM-based side-channel vulnerabilities in the error correcting codes (ECC) enabling us to distinguish based on the value/validity of decrypted codewords. We also identified similar vulnerabilities in the Fujisaki-Okamoto transform which leaks information about decrypted messages applicable to schemes that do not use ECC. We subsequently exploit these vulnerabilities to demonstrate practical attacks applicable to six CCA-secure lattice-based PKE/KEMs competing in the second round of the NIST standardization process. We perform experimental validation of our attacks on implementations taken from the open-source pqm4 library, running on the ARM Cortex-M4 microcontroller. Our attacks lead to complete key-recovery in a matter of minutes on all the targeted schemes, thus showing the effectiveness of our attack.


Author(s):  
Shivam Bhasin ◽  
Jan-Pieter D’Anvers ◽  
Daniel Heinz ◽  
Thomas Pöppelmann ◽  
Michiel Van Beirendonck

In this work, we are concerned with the hardening of post-quantum key encapsulation mechanisms (KEM) against side-channel attacks, with a focus on the comparison operation required for the Fujisaki-Okamoto (FO) transform. We identify critical vulnerabilities in two proposals for masked comparison and successfully attack the masked comparison algorithms from TCHES 2018 and TCHES 2020. To do so, we use first-order side-channel attacks and show that the advertised security properties do not hold. Additionally, we break the higher-order secured masked comparison from TCHES 2020 using a collision attack, which does not require side-channel information. To enable implementers to spot such flaws in the implementation or underlying algorithms, we propose a framework that is designed to test the re-encryption step of the FO transform for information leakage. Our framework relies on a specifically parametrized t-test and would have identified the previously mentioned flaws in the masked comparison. Our framework can be used to test both the comparison itself and the full decapsulation implementation.


2018 ◽  
Vol 28 (01) ◽  
pp. 1950003 ◽  
Author(s):  
E. Saeedi ◽  
M. S. Hossain ◽  
Y. Kong

The safety of cryptosystems, mainly based on algorithmic improvement, is still vulnerable to side-channel attacks (SCA) based on machine learning. Multi-class classification based on neural networks and principal components analysis (PCA) can be powerful tools for pattern recognition and classification of side-channel information. In this paper, an experimental investigation was conducted to explore the efficiency of various architectures of feed-forward back-propagation (FFBP) neural networks and PCA against side-channel attacks. The experiment is performed on the data leakage of an FPGA implementation of elliptic curve cryptography (ECC). Our results show that the proposed method is a promising method for SCA with an overall accuracy of 88% correct classification.


Author(s):  
Victor Lomné ◽  
Emmanuel Prouff ◽  
Matthieu Rivain ◽  
Thomas Roche ◽  
Adrian Thillard

2021 ◽  
pp. 173-185
Author(s):  
Yanbin Li ◽  
Yuxin Huang ◽  
Ming Tang ◽  
Shougang Ren ◽  
Huanliang Xu

2019 ◽  
Vol 9 (21) ◽  
pp. 4692
Author(s):  
Yoo-Jin Baek

With the growing threat of the side-channel attack (SCA) to the cryptographic algorithm’s implementations, the masking method has become one of the most promising SCA countermeasures for securely implementing, for example, block ciphers. The basic principle of the masking method is that if the sensitive variable (which, by definition, depends on sensitive information) is split into some random variables and they are manipulated in a secure manner, then the relationship between the random variables and the corresponding side-channel information may look independent from the outside world. However, after the introduction of the glitch attack, there has been a lot of concern about the security of the masking method itself. And, to mitigate the threat of the glitch attack, the threshold implementation (TI) and G-equivariant gates were independently introduced as countermeasures. In this paper, we consider the main notions of two such independent glitch attack’s countermeasures, say, non-completeness and G-equivariance, and investigate their relationship. The contribution of this paper is three-fold. First, we show that the widely-circulated proof that the non-complete TI with uniform inputs guarantees the security against the 1st order DPA even in the presence of glitches is not satisfactory. Next, using the extended notion of G-equivariance to the higher-order setting, we prove that non-completeness implies G-equivariance, which, in turn, means that the non-complete TI with uniform inputs has resistance against the glitch attack. Thirdly, we prove that the set of non-complete gates is a proper subset of the set of G-equivariant gates by showing there is a gate that is G-equivariant but not non-complete.


Author(s):  
Eric Peeters ◽  
François-Xavier Standaert ◽  
Nicolas Donckers ◽  
Jean-Jacques Quisquater

Sign in / Sign up

Export Citation Format

Share Document