密码实现安全形式化验证发展现状与展望

Status and Prospects of Formal Verification for Security of Cryptographic Implementations

密码是保障网络安全和信息安全的核心技术和基础支撑,但密码实现本身面临多种安全威胁,形式化验证是严格证明密码实现安全性的重要技术手段。文章回顾了国内外在密码实现的功能正确性和内存安全性、时间侧信道安全性、功耗侧信道安全性方面的形式化验证技术发展现状和应用情况,分析了当前面向密码实现的形式化验证技术的不足、挑战和发展趋势。鉴于中国密码实现的安全性需求和相应形式化验证技术积累的不足,建议以研制构建高性能、高可信密码库为目标,以国家重大任务为牵引,通过顶层设计,强化自主创新,统一中间表示语言,研制高效率、高精度、自动化的形式化验证平台及安全编译优化工具链,最小化可信计算基,构造高效率、高可信密码实现通用库,促进产学研融合发展,进一步提高国家网络安全和信息安全的发展质量。

Serving as a foundation,cryptography is the key technique for ensuring network and information security.However,cryptographic implementations suffer from various security threats.Formal verification is the most important technique for rigorously proving the security of cryptographic implementations.This article first reviews the development status and application of formal verification techniques for cryptographic implementations both in China and abroad in terms of functional correctness,memory security,and side-channel security including time and power consumption.Then the article summarizes the drawbacks,current challenges,and development trends of these formal verification techniques for cryptographic implementations.According to the security requirements and limited progress in formal verification techniques for cryptographic implementations in China,it is suggested that high-performance and high-assurance cryptographic libraries should be constructed.In addition,the article proposes to follow the top-down design principle,strengthen independent innovation,and unify intermediate representation language under the guidance of national key task,and it plans to develop a high-efficiency,high-precision,and full-automated formal verification platform and a secure compiler optimization toolchain,create high-performance and high-assurance common cryptographic library with minimized trusted computing base,and promote the integrated development of both academic and industrial communities,so as to improve national network and information security.