PoMMES: Prevention of Micro-architectural Leakages in Masked Embedded Software

被引:0
作者
Zeitschner, Jannik [1 ]
Moradi, Amir [2 ]
机构
[1] Ruhr University Bochum, Horst Görtz Institute for IT Security, Bochum
[2] Technische Universität Darmstadt, Darmstadt
来源
IACR Transactions on Cryptographic Hardware and Embedded Systems | 2024年 / 2024卷 / 03期
关键词
Compiler; Masking; Side-Channel Analysis; Software;
D O I
10.46586/tches.v2024.i3.342-376
中图分类号
学科分类号
摘要
Software solutions to address computational challenges are ubiquitous in our daily lives. One specific application area where software is often used is in embedded systems, which, like other digital electronic devices, are vulnerable to side-channel analysis attacks. Although masking is the most common countermeasure and provides a solid theoretical foundation for ensuring security, recent research has revealed a crucial gap between theoretical and real-world security. This shortcoming stems from the micro-architectural effects of the underlying micro-processor. Common security models used to formally verify masking schemes such as the d-probing model fully ignore the micro-architectural leakages that lead to a set of instructions that unintentionally recombine the shares. Manual generation of masked assembly code that remains secure in the presence of such micro-architectural recombinations often involves trial and error, and is non-trivial even for experts. Motivated by this, we present PoMMES, which enables inexperienced software developers to automatically compile masked functions written in a high-level programming language into assembly code, while preserving the theoretically proven security in practice. Compared to the state of the art, based on a general model for microarchitectural effects, our scheme allows the generation of practically secure masked software at arbitrary security orders for in-order processors. The major contribution of PoMMES is its micro-architecture aware register allocation algorithm, which is one of the crucial steps during the compilation process. In addition to simulation-based assessments that we conducted by open-source tools dedicated to evaluating masked software implementations, we confirm the effectiveness of the PoMMES-generated codes through experimental analysis. We present the result of power consumption based leakage assessments of several case studies running on a Cortex M0+ micro-controller, which is commonly deployed in industry. © 2024, Ruhr-University of Bochum. All rights reserved.
引用
收藏
页码:342 / 376
页数:34
相关论文
共 56 条
[1]  
Almeida Jose Bacelar, Barbosa Manuel, Barthe Gilles, Blot Arthur, Gregoire Benjamin, Laporte Vincent, Oliveira Tiago, Pacheco Hugo, Schmidt Benedikt, Strub Pierre-Yves, Jasmin: High-assurance and high-speed cryptography, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 1807-1823, (2017)
[2]  
Abromeit Arnold, Bache Florian, Becker Leon A., Gourjon Marc, Guneysu Tim, Jorn Sabrina, Moradi Amir, Orlt Maximilian, Schellenberg Falk, Automated masking of software implementations on industrial microcontrollers, DATE 2021, (2021)
[3]  
Barthe Gilles, Belaid Sonia, Cassiers Gaetan, Fouque Pierre-Alain, Gregoire Benjamin, Standaert Francois-Xavier, maskverif: Automated verification of higher-order masking in presence of physical defaults, ESORICS 2019, volume 11735 of LNCS, pp. 300-318, (2019)
[4]  
Barthe Gilles, Belaid Sonia, Dupressoir Francois, Fouque Pierre-Alain, Gregoire Benjamin, Strub Pierre-Yves, Verified proofs of higher-order masking, EUROCRYPT 2015, volume 9056 of LNCS, pp. 457-485, (2015)
[5]  
Barthe Gilles, Belaid Sonia, Dupressoir Francois, Fouque Pierre-Alain, Gregoire Benjamin, Strub Pierre-Yves, Zucchini Rebecca, Strong noninterference and type-directed higher-order masking, CCS 2016, pp. 116-129, (2016)
[6]  
Bronchain Olivier, Cassiers Gaetan, Bitslicing arithmetic/boolean masking conversions for fun and profit with application to lattice-based kems, IACR Trans. Cryptogr. Hardw. Embed. Syst, 2022, 4, pp. 553-588, (2022)
[7]  
Belaid Sonia, Coron Jean-Sebastien, Prouff Emmanuel, Rivain Matthieu, Taleb Abdul Rahman, Random Probing Security: Verification, Composition, Expansion and New Constructions, CRYPTO 2020, volume 12170 of LNCS, (2020)
[8]  
Barthe Gilles, Gourjon Marc, Gregoire Benjamin, Orlt Maximilian, Paglialonga Clara, Porth Lars, Masking in fine-grained leakage models: Construction, implementation and verification, IACR Trans. Cryptogr. Hardw. Embed. Syst, 2021, 2, pp. 189-228, (2021)
[9]  
Blomer Johannes, Guajardo Jorge, Krummel Volker, Provably secure masking of AES, Selected Areas in Cryptography, 11th International Workshop, SAC 2004, Waterloo, Canada, August 9-10, 2004, Revised Selected Papers, volume 3357 of Lecture Notes in Computer Science, pp. 69-83, (2004)
[10]  
Belaid Sonia, Mercadier Darius, Rivain Matthieu, Taleb Abdul Rahman, Ironmask: Versatile verification of masking security, IEEE S & P 2022, pp. 142-160, (2022)