侧信道掩码的形式化验证综述OA

To mitigate the impact of side-channel attacks,some masking schemes that are efficient and are proven to be secure under some attack models,such as the probing model,have been put up with by many researchers.Initially,some trivial masking schemes may be proved by hand-made proof.Nevertheless,it is difficult and error-prone to prove some complex masking schemes by hand.Thus,formal verification tools are proposed and improved.These tools use a computer to automatically assist in proving if masking schemes satisfy the security requirements.In all these tools,the two most commonly adopted formal verification approaches are static analysis and probabilistic analysis.Static analysis is generally considered efficient,but it may yield false positives.In contrast,probabilistic analysis does not produce false positives,but it is significantly less efficient.Some relatively refined formal verification tools,such as maskVerif,SILVER,IronMask,etc,are proposed and presented.This study first systematically introduce side-channel attacks,side-channel countermeasures(mostly mask-ing).Then,it presents commonly used attack/security models in the formal verification community.Following this,a comprehensive review is conducted of formal verification tools,analyzing their fea-tures,underlying technologies,scalability,and advantages and disadvantages.After presenting such comparative analysis of these tools,findings and discussions of potential future research directions are summarized finally.