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

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

一、项目概述

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

1. SM3：根据 GM/T 0004—2012 标准建立 ghost model，为接口 API 建立 pre-condition、post-condition、loop invariant 和 assert，使用 WP 验证功能一致性；编写内存安全 spec，并结合 RTE 验证。
2. SM4：根据GM/T 0002—2012标准建立 ghost model，使用 WP 验证功能一致性；编写内存安全 spec，并结合 RTE 验证。 针对SM4 模式通过 测试驱动 + EVA 插件 验证 API 调用链，实现功能正确性与内存安全性。
3. 证明优化：针对证明超时问题，采用 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

三、如何运行

1. 配置环境与 Frama-c

sh install_frama-c.sh

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

2. 验证 SM3:

sh verify_sm3.sh

3. 验证 SM4:

sh verify_sm4.sh

4. 验证 SM4-CBC 模式:

sh verify_sm4_cbc.sh

5. 验证 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 运行脚本

1. SM3

• 文件：noasm_sm3.c noasm_sm3_ghost.h
• 验证点：置换函数$P_0,P_1$,布尔函数$F{F}_0,F{F}_1,G{G}_0,G{G}_1$, 压缩函数$ROUND$、消息扩展$EXPAND$、接口 API
  • 

2. SM4（分组/密钥拓展）

• 文件：crypt_sm4.c, crypt_sm4_ghost.h, sm4_key.c
• 验证点：S 盒、T 变换、轮函数、密钥扩展
  • 

3. SM4 模式（CBC/CFB）

• 策略：基于 API 的测试流 + EVA 分析
• 文件： sm4cbc.c, sm4cfb.c
• 验证点：调用链正确性、内存访问安全性
  • 

五、主要问题与规约设计

1. 嵌套宏定义：使用 Frama-c 的 Logic 逻辑函数表达这些操作

• 纯数学运算
• 没有副作用
• 

2. 64次循环：

• 先实现单轮压缩，循环使用递归实现，便于求解器归纳证明
• 用循环不变式验证循环正确性，包含
  • 循环变量：可终止
  • 循环不变量：满足程序要求
  • 明确循环中修改的内存：避免指针重名
• 

3. 验证功能一致性：有幽灵模型之后，规约“一致”

4. 内存安全的验证

• requires：指针非空、区间合法、输入输出分离
• assigns：精确声明修改集
• ensures：功能等价关系与不变式
• loop invariant：索引范围、已处理前缀等价性
• assert：约束溢出与位运算值域
  

5. sm4 模式的验证：基于包装好的 API，使用 EVA 验证函数调用链

• 函数调用关系图