Formal Verification of Masked Hardware Implementations in the Presence of Glitches

No abstract is available for this paper.

• Publication year

  2018

• Venue

  IACR Cryptology ePrint Archive

• Publication date

  2018-04-29

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.1007/978-3-319-78375-8_11
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Formal Verification of Side-channel Countermeasures via Elementary Circuit Transformations

  2018influential reference
• Composable Masking Schemes in the Presence of Physical Defaults and the Robust Probing Model

  2018cited by this paper
• Private Multiplication over Finite Fields

  2017cited by this paper
• Higher-Order Side-Channel Protected Implementations of KECCAK

  2017influential reference
• Reconciling d+1 Masking in Hardware and Software

  2017cited by this paper
• An Efficient Side-Channel Protected AES Implementation with Arbitrary Protection Order

  2017influential reference
• Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model

  2017cited by this paper
• Strong Non-Interference and Type-Directed Higher-Order Masking

  2016cited by this paper
• Randomness Complexity of Private Circuits for Multiplication

  2016cited by this paper
• A Methodology for the Characterisation of Leakages in Combinatorial Logic

  2016cited by this paper
• Detecting Flawed Masking Schemes with Leakage Detection Tests

  2016influential reference
• Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler

  2015cited by this paper
• Verified Proofs of Higher-Order Masking

  2015cited by this paper
• Consolidating Masking Schemes

  2015cited by this paper
• SMT-Based Verification of Software Countermeasures against Side-Channel Attacks

  2014cited by this paper
• QMS: Evaluating the side-channel resistance of masked software from source code

  2014cited by this paper
• Higher-Order Threshold Implementations

  2014cited by this paper
• Synthesis of Masking Countermeasures against Side Channel Attacks

  2014cited by this paper
• Sleuth: Automated Verification of Software Power Analysis Countermeasures

  2013cited by this paper
• Theory of masking with codewords in hardware: low-weight dth-order correlation-immune Boolean functions

  2013cited by this paper
• Yosys-A Free Verilog Synthesis Suite

  2013cited by this paper
• Fides: Lightweight Authenticated Cipher with Side-Channel Resistance for Constrained Hardware

  2013cited by this paper
• Analysis of Boolean Functions

  2012cited by this paper
• Compiler Assisted Masking

  2012cited by this paper
• A testing methodology for side ­ channel resistance validation

  2011cited by this paper
• Provably Secure Higher-Order Masking of AES

  2010cited by this paper
• Protecting Circuits from Leakage: the Computationally-Bounded and Noisy Cases

  2010cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Threshold Implementations Against Side-Channel Attacks and Glitches

  2006influential reference
• Pinpointing the Side-Channel Leakage of Masked AES Hardware Implementations

  2006cited by this paper
• Combinational Logic Design for AES SubByte Transformation on Masked Data

  2003influential reference
• Private Circuits: Securing Hardware against Probing Attacks

  2003influential reference
• ElectroMagnetic Analysis (EMA): Measures and Counter-Measures for Smart Cards

  2001cited by this paper
• Differential Power Analysis

  1999cited by this paper
• Towards Sound Approaches to Counteract Power-Analysis Attacks

  1999cited by this paper
• A spectral characterization of correlation-immune combining functions

  1988cited by this paper

• Combined Indistinguishability Analysis - Verifying random probing leakage under random faults

  2026cites this paper
• On Borrowed Time - Preventing Static Side-Channel Analysis

  2025cites this paper
• Netlist whisperer: extensive analysis of circuit leakage using LLMs

  2025cites this paper
• Pushing The Area Limit of Composable Gadgets Low-Area Hardware Masked Circuits with Fewer Sources of Randomness

  2025cites this paper
• Another Evidence to not Employ Customized Masked Hardware Identifying and Fixing Flaws in SCARV

  2024cites this paper
• Efficient Second-Order Masked Software Implementations of Ascon in Theory and Practice

  2024cites this paper
• Prover - Toward More Efficient Formal Verification of Masking in Probing Model

  2024influential citation
• Deep Learning Gradient Visualization-Based Pre-Silicon Side-Channel Leakage Location

  2024cites this paper
• Robust but Relaxed Probing Model

  2024cites this paper
• Low-Latency Masked Gadgets Robust against Physical Defaults with Application to Ascon

  2024influential citation
• INDIANA - Verifying (Random) Probing Security through Indistinguishability Analysis

  2024cites this paper
• Security Aspects of Masking on FPGAs

  2024influential citation
• The propagation game: on simulatability, correlation matrices, and probing security

  2023cites this paper
• Gate-Level Masking of Streamlined NTRU Prime Decapsulation in Hardware

  2023cites this paper
• PROLEAD_SW - Probing-Based Software Leakage Detection for ARM Binaries

  2023cites this paper
• A Pre-Silicon Power Leakage Assessment Based on Generative Adversarial Networks

  2023cites this paper
• Efficient Low-Latency Masking of Ascon without Fresh Randomness

  2023cites this paper
• Smooth Passage with the Guards: Second-Order Hardware Masking of the AES with Low Randomness and Low Latency

  2023cites this paper
• Gadget-based Masking of Streamlined NTRU Prime Decapsulation in Hardware

  2023cites this paper
• Compositional Verification of First-Order Masking Countermeasures against Power Side-Channel Attacks

  2023cites this paper
• Netlist Whisperer: AI and NLP Fight Circuit Leakage!

  2023cites this paper
• Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks

  2023influential citation
• Offre de stage - Internship Offer Generation of Masking Countermeasures Against Side-Channel Attacks

  2023cites this paper
• Offre de th`ese - PhD Thesis Offer Generation of Masking Countermeasures Against Side-Channel Attacks

  2023cites this paper
• Unifying Freedom and Separation for Tight Probing-Secure Composition

  2023cites this paper
• Automated Verification of Correctness for Masked Arithmetic Programs

  2023cites this paper
• Threshold Implementations in Software: Micro-architectural Leakages in Algorithms

  2023cites this paper
• A Threshold Implementation-Based Neural Network Accelerator With Power and Electromagnetic Side-Channel Countermeasures

  2023cites this paper
• Challenges and Opportunities of Security-Aware EDA

  2022cites this paper
• Transitional Leakage in Theory and Practice - Unveiling Security Flaws in Masked Circuits

  2022cites this paper
• Composable Gadgets with Reused Fresh Masks First-Order Probing-Secure Hardware Circuits with only 6 Fresh Masks

  2022cites this paper
• Low-Latency Hardware Private Circuits

  2022cites this paper
• IronMask: Versatile Verification of Masking Security

  2022cites this paper
• Formal Verification of Arithmetic Masking in Hardware and Software

  2022cites this paper
• Don’t CWEAT It: Toward CWE Analysis Techniques in Early Stages of Hardware Design

  2022cites this paper
• Handcrafting: Improving Automated Masking in Hardware with Manual Optimizations

  2022cites this paper
• SoC Root Canal! Root Cause Analysis of Power Side-Channel Leakage in System-on-Chip Designs

  2022cites this paper
• A Survey and Perspective on Artificial Intelligence for Security-Aware Electronic Design Automation

  2022cites this paper
• PROLEAD A Probing-Based Hardware Leakage Detection Tool

  2022cites this paper
• TSCL: A time-space crossing location for side-channel leakage detection

  2022cites this paper
• Effective and Efficient Masking with Low Noise using Small-Mersenne-Prime Ciphers

  2022cites this paper
• VERICA - Verification of Combined Attacks: Automated formal verification of security against simultaneous information leakage and tampering

  2022cites this paper
• A relation calculus for reasoning about t-probing security

  2022cites this paper
• Secure and Efficient Software Masking on Superscalar Pipelined Processors

  2021cites this paper
• Fast Verification of Masking Schemes in Characteristic Two

  2021cites this paper
• Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification

  2021cites this paper
• An Instruction Set Extension to Support Software-Based Masking

  2021cites this paper
• Intrinsic Resiliency of S-Boxes Against Side-Channel Attacks–Best and Worst Scenarios

  2021cites this paper
• MIRACLE: MIcRo-ArChitectural Leakage Evaluation

  2021cites this paper
• Automated Generation of Masked Hardware

  2021cites this paper
• Circuit Masking: From Theory to Standardization, A Comprehensive Survey for Hardware Security Researchers and Practitioners

  2021influential citation
• A Novel Completeness Test and its Application to Side Channel Attacks and Simulators

  2021cites this paper
• Towards Tight Random Probing Security - extended version

  2021cites this paper
• Proving SIFA protection of masked redundant circuits

  2021influential citation
• Towards Tight Random Probing Security

  2021cites this paper
• On robust strong-non-interferent low-latency multiplications

  2021cites this paper
• COCOALMA: A Versatile Masking Verifier

  2021influential citation
• Formal Evaluation and Construction of Glitch-resistant Masked Functions

  2021influential citation
• Cryptographic Fault Diagnosis using VerFI

  2020cites this paper
• A pre-silicon logic level security verification flow for higher-order masking schemes against glitches on FPGAs

  2020cites this paper
• Automated Verification of Higher-Order Masking in Presence of Physical Defaults

  2020influential citation
• Coco: Co-Design and Co-Verification of Masked Software Implementations on CPUs

  2020influential citation
• Reducing risks through simplicity: high side-channel security for lazy engineers

  2020cites this paper
• The Area-Latency Symbiosis: Towards Improved Serial Encryption Circuits

  2020cites this paper
• Deliverable D 1 . 5 White Paper : Assurance in Security Evaluations

  2020cites this paper
• Real-World Snapshots vs. Theory: Questioning the t-Probing Security Model

  2020cites this paper
• On the spectral features of robust probing security

  2020cites this paper
• Formal Verification of Masking Countermeasures for Arithmetic Programs

  2020influential citation
• A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs

  2020influential citation
• SILVER - Statistical Independence and Leakage Verification

  2020influential citation
• SCRIPT

  2020cites this paper
• SNI-in-the-head: Protecting MPC-in-the-head Protocols against Side-channel Analysis

  2020cites this paper
• Hardware Private Circuits: From Trivial Composition to Full Verification

  2020cites this paper
• Deliverable L2.2 Formal methods for the verification of countermeasures

  2020cites this paper
• Verifying and Quantifying Side-channel Resistance of Masked Software Implementations

  2019influential citation
• State of the Art of formal Verification Techniques

  2019cites this paper
• Rosita: Towards Automatic Elimination of Power-Analysis Leakage in Ciphers

  2019cites this paper
• First-Order Masking with Only Two Random Bits

  2019cites this paper
• Formal Verification of Digital Circuits Using Simulator with Mathematical Foundation

  2019cites this paper
• A Survey of Leakage-Resilient Cryptography

  2019cites this paper
• Leakage Resilience of the Duplex Construction

  2019cites this paper
• Mitigating power side channels during compilation

  2019cites this paper
• maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults

  2019cites this paper
• Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks

  2019cites this paper
• Shuffle and Mix: On the Diffusion of Randomness in Threshold Implementations of Keccak

  2019cites this paper
• Consolidating Security Notions in Hardware Masking

  2019cites this paper
• Glitch-Resistant Masking Revisited - or Why Proofs in the Robust Probing Model are Needed

  2019cites this paper
• Generic Low-Latency Masking in Hardware

  2018cites this paper
• maskVerif : automated analysis of software and hardware higher-order masked implementations

  2018influential citation
• Sharing Independence & Relabeling: Efficient Formal Verification of Higher-Order Masking

  2018influential citation
• Masking the AES with Only Two Random Bits

  2018cites this paper
• SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks

  2018cites this paper
• Towards efficient and automated side-channel evaluations at design time

  2018cites this paper
• Adversarial symbolic execution for detecting concurrency-related cache timing leaks

  2018cites this paper
• SCI nfer : Refinement-based Verification of Software Countermeasures against Side-Channel Attacks ?

  2018cites this paper
• Hardware Masking, Revisited

  2018cites this paper
• VerMI: Verification Tool for Masked Implementations

  2018influential citation
• A unified masking approach

  2018influential citation
• Composable Masking Schemes in the Presence of Physical Defaults and the Robust Probing Model

  2018cites this paper
• Tight Private Circuits: Achieving Probing Security with the Least Refreshing

  2018cites this paper