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