Formal verification of masked hardware implementations in the presence of glitches

DOI10.1007/978-3-319-78375-8_11zbMATH Open1428.94062OpenAlexW2795180100MaRDI QIDQ1648840FDOQ1648840

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

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

zbMATH Keywords

side-channel analysisformal verificationmaskinghardware securityprivate circuitsthreshold implementations

Mathematics Subject Classification ID

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

Cited In (10)

• Secure and efficient software masking on superscalar pipelined processors
• Effective and efficient masking with low noise using small-Mersenne-prime ciphers
• Proving SIFA protection of masked redundant circuits
• Fast verification of masking schemes in characteristic two
• Handcrafting: improving automated masking in hardware with manual optimizations
• Towards tight random probing security
• SILVER -- statistical independence and leakage verification
• Formal verification of arithmetic masking in hardware and software
• Secure hardware implementation of nonlinear functions in the presence of glitches
• Automated verification of correctness for masked arithmetic programs

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)