Formal verification of masked hardware implementations in the presence of glitches

DOI10.1007/978-3-319-78375-8_11MaRDI QIDQ1648840zbMATH OpenOpenAlexFDO

Authors Roderick Bloem, Hannes Gross, Rinat Iusupov, Bettina Könighofer, Stefan Mangard, Johannes Winter

Publication date 9 July 2018

Full work available at URL https://doi.org/10.1007/978-3-319-78375-8_11

zbMATH Keywords

formal verificationhardware securitymaskingprivate circuitsside-channel analysisthreshold implementations

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Cryptography (94A60)

Recommendations

• Formal verification of side-channel countermeasures via elementary circuit transformations
• SILVER -- statistical independence and leakage verification
• Secure Hardware Implementation of Non-linear Functions in the Presence of Glitches
• Secure hardware implementation of nonlinear functions in the presence of glitches
• Detecting flawed masking schemes with leakage detection tests

Cited in

(17)

• Formal verification of side-channel countermeasures via elementary circuit transformations
• A methodology for the characterisation of leakages in combinatorial logic
• Fast verification of masking schemes in characteristic two
• Towards tight random probing security
• Proving SIFA protection of masked redundant circuits
• The first thorough side-channel hardware Trojan
• Formal verification of side-channel countermeasures using self-composition
• SILVER -- statistical independence and leakage verification
• Detecting flawed masking schemes with leakage detection tests
• Effective and efficient masking with low noise using small-Mersenne-prime ciphers
• Handcrafting: improving automated masking in hardware with manual optimizations
• Secure and efficient software masking on superscalar pipelined processors
• Formal verification of arithmetic masking in hardware and software
• Automated verification of correctness for masked arithmetic programs
• Secure hardware implementation of nonlinear functions in the presence of glitches
• ProverNG: efficient verification of compositional masking for cryptosystem's side-channel security
• INDIANA -- verifying (random) probing security through indistinguishability analysis

Describes a project that uses

Uses Software

• z3
• EasyCrypt
• REBECCA
• Yosys
• acrt

This page was built for publication: Formal verification of masked hardware implementations in the presence of glitches

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1648840)