IACR Cryptology ePrint Archive · 2020 · 11 citations · 0 references
ComputingComputer ScienceCybersecurityCompilersCryptographyFormal MethodsCryptographic ImplementationSecure System DesignSide-channel AnalysisSide-channel AttacksFormal Verification
Cryptographic implementations deployed in real world devices often aim at (provable) security against the powerful class of side-channel attacks while keeping reasonable performances. Last year at Asiacrypt, a new formal verification tool named tightPROVE was put forward to exactly determine whether a masked implementation is secure in the well-deployed probing security model for any given security order t. Also recently, a compiler named Usuba was proposed to automatically generate bitsliced implementations of cryptographic primitives.