VerMI: Verification Tool for Masked Implementations

被引:0
|
作者
Arribas, Victor [1 ]
Nikova, Svetla [1 ]
Rijmen, Vincent [1 ]
机构
[1] Katholieke Univ Leuven, Imec COSIC, Leuven, Belgium
基金
欧盟地平线“2020”;
关键词
VerMI; Masking; Side-Channel Analysis; Glitches; Formal Verification; Logic Simulator; Non-completeness; Uniformity;
D O I
暂无
中图分类号
TM [电工技术]; TN [电子技术、通信技术];
学科分类号
0808 ; 0809 ;
摘要
Masking is a widely used countermeasure against Side-Channel Attacks, nonetheless, the implementation of these countermeasures is challenging. Experimental security evaluation requires special equipment, a considerable amount of time, and extensive technical knowledge. Therefore, to automate and to speed up this process, a formal verification can be performed to asses the security of a design. In this work we present VerMI, a verification tool in the form of a logic simulator that checks the properties defined in Threshold Implementations to address the security of a hardware implementation for meaningful orders of security. The tool is designed so that any masking scheme can be evaluated. It accepts combinational and sequential logic and is able to analyze an entire cipher in short time. With the tool we have managed to spot a flaw in the round-based KECCAK implementation by Gross et al., published in DSD 2017.
引用
收藏
页码:381 / 384
页数:4
相关论文
共 50 条
  • [1] Formal Verification of Masked Hardware Implementations in the Presence of Glitches
    Bloem, Roderick
    Gross, Hannes
    Iusupov, Rinat
    Koenighofer, Bettina
    Mangard, Stefan
    Winter, Johannes
    ADVANCES IN CRYPTOLOGY - EUROCRYPT 2018, PT II, 2018, 10821 : 321 - 353
  • [2] COCO: Co-Design and Co-Verification of Masked Software Implementations on CPUs
    Gigerl, Barbara
    Hadzic, Vedad
    Primas, Robert
    Mangard, Stefan
    Bloem, Roderick
    PROCEEDINGS OF THE 30TH USENIX SECURITY SYMPOSIUM, 2021, : 1469 - 1486
  • [3] On the Security of Partially Masked Software Implementations
    Barenghi, Alessandro
    Pelosi, Gerardo
    2014 11TH INTERNATIONAL CONFERENCE ON SECURITY AND CRYPTOGRAPHY (SECRYPT), 2014, : 492 - 499
  • [4] Secure Context Switching of Masked Software Implementations
    Gigerl, Barbara
    Primas, Robert
    Mangard, Stefan
    PROCEEDINGS OF THE 2023 ACM ASIA CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, ASIA CCS 2023, 2023, : 980 - 992
  • [5] Does Coupling Affect the Security of Masked Implementations?
    De Cnudde, Thomas
    Bilgin, Begul
    Gierlichs, Benedikt
    Nikov, Ventzislav
    Nikova, Svetla
    Rijmen, Vincent
    CONSTRUCTIVE SIDE-CHANNEL ANALYSIS AND SECURE DESIGN, 2017, 10348 : 1 - 18
  • [6] Successfully attacking masked AES hardware implementations
    Mangard, S
    Pramstaller, N
    Oswald, E
    CRYPTOGRAPHIC HARDWARE AND EMBEDDED SYSTEMS - CHES 2005, PROCEEDINGS, 2005, 3659 : 157 - 171
  • [7] Design verification of FPGA implementations
    Chen, XT
    Huang, WK
    Park, N
    Meyer, FJ
    Lombardi, F
    IEEE DESIGN & TEST OF COMPUTERS, 1999, 16 (02): : 66 - 73
  • [8] Design verification of FPGA implementations
    Fudan University, Shanghai, China
    不详
    不详
    不详
    IEEE Des Test Comput, 2 (66-73):
  • [9] Runtime verification of statechart implementations
    Pintér, G
    Majzik, I
    ARCHITECTING DEPENDABLE SYSTEMS III, 2005, 3549 : 148 - 172
  • [10] Modeling and verification of ISA implementations
    Shen, XW
    Arvind
    PROCEEDINGS OF THE 3RD AUSTRALASIAN COMPUTER ARCHITECTURE CONFERENCE, ACAC'98, 1998, 20 (04): : 157 - 168