a858208a创建于 2025年10月16日历史提交

基于 Frama-C 的国密算法形式化验证

本项目旨在使用形式化验证工具 Frama-C 对国密算法 SM3 和 SM4 的 C 语言实现进行严格的软件安全和功能正确性分析。

一、项目概述

本项目旨在利用 Frama-C 对 openHiTLS 实现的 SM3/SM4进行形式化验证，确保算法实现与国密标准一致，且具备内存安全性。
主要完成内容：

SM3：根据 GM/T 0004—2012 标准建立 ghost model，为接口 API 建立 pre-condition、post-condition、loop invariant 和 assert，使用 WP 验证功能一致性；编写内存安全 spec，并结合 RTE 验证。
SM4：根据GM/T 0002—2012标准建立 ghost model，使用 WP 验证功能一致性；编写内存安全 spec，并结合 RTE 验证。针对SM4 模式通过 测试驱动 + EVA 插件 验证 API 调用链，实现功能正确性与内存安全性。
证明优化：针对证明超时问题，采用 lemma + ghost 混合建模 方法，复杂轮函数与 S 盒变换拆分为可复用的 lemma，优化证明代价。

二、环境要求

项目的环境需求为：

系统：Ubuntu 20.04+
编译器：OCaml 5.3.0
包管理器：opam 2.4.1
验证工具：Frama-C 31.0
求解器：Z3 4.15.3 - 64 bit, alt-ergo 2.6.2

三、如何运行

配置环境与 Frama-c

sh install_frama-c.sh

首先拉取 openHiTLS 的源码，并自动安装 OCaml、opam 和 Frama-c，如果失败，可以访问 https://www.frama-c.com/html/get-frama-c.html 手动进行安装。

验证 SM3:

sh verify_sm3.sh

验证 SM4:

sh verify_sm4.sh

验证 SM4-CBC 模式:

sh verify_sm4_cbc.sh

验证 SM4-CFB 模式:

sh verify_sm4_cfb.sh

若出现can't find file错误，请修改对应命令脚本中的-cpp-extra-args, Frama-c 通过此参数引导 gcc 找到头文件。

四、验证对象与范围

.
├── install_frama-c.sh    # 安装脚本
├── LICENSE               
├── README.md             # 项目说明文档
├── verify_sm3            
│   ├── noasm_sm3_ghost.h # SM3 的 Ghost Model
│   └── noasm_sm3.c       # SM3 验证规约 
├── verify_sm3.sh         # SM3 验证运行脚本
├── verify_sm4            
│   ├── crypt_sm4_ghost.h # SM4 的 Ghost Model
│   ├── crypt_sm4.c       # SM4 核心实现（验证目标）
│   ├── crypt_sm4.h       # SM4 头文件：SM4 算法的函数声明和宏定义
│   ├── noasm_sm4_cbc.c   # CBC 模式的 API
│   ├── noasm_sm4_cfb.c   # CFB 模式的 API
│   ├── sm4_ghost.h       # SM4 API 的 Ghost Model
│   ├── sm4_key.c         # SM4 密钥处理
│   ├── sm4cbc.c          # 调用 CBC 模式 API 的样例
│   └── sm4cfb.c          # 调用 CFB 模式 API 的样例
├── verify_sm4_cbc.sh     # SM4 CBC 模式验证脚本
├── verify_sm4_cfb.sh     # SM4 CFB 模式验证脚本
└── verify_sm4.sh         # SM4 运行脚本

文件：noasm_sm3.c noasm_sm3_ghost.h
验证点：置换函数 $P_{0}, P_{1}$ ,布尔函数 $F F_{0}, F F_{1}, G G_{0}, G G_{1}$ , 压缩函数 $R O U N D$ 、消息扩展 $E X P A N D$ 、接口 API