抽象解释及其应用研究进展

陈立前; 范广生; 尹帮虎; 王戟

doi:10.7544/issn1000-1239.202220925

抽象解释及其应用研究进展

陈立前^1,,
范广生^{1, 3,},
尹帮虎^2, ,,
王戟^{1, 3,}

1.
国防科技大学计算机学院　长沙　410073
2.
国防科技大学系统工程学院　长沙　410073
3.
高性能计算国家重点实验室（国防科技大学）长沙　410073

基金项目: 国家重点研发计划项目(2022YFA1005101)；国家自然科学基金项目(61872445, 62032024, 62102432)；湖南省自然科学基金项目(2021JJ40697)

详细信息

作者简介:
陈立前: 1982年生. 博士，副教授，硕士生导师. CCF高级会员. 主要研究方向为程序分析与验证、程序自动修复、可信人工智能

范广生: 1997年生.博士研究生.主要研究方向为程序分析与验证

尹帮虎: 1989年生.博士，讲师.主要研究方向为程序分析与验证、可信人工智能、系统建模与仿真

王戟: 1969年生.博士，教授，博士生导师.CCF会士.主要研究方向为形式化方法、软件工程

通讯作者:
尹帮虎(bhyin@nudt.edu.cn)

中图分类号: TP391
计量
- 文章访问数: 1119
- HTML全文浏览量: 114
- PDF下载量: 338
出版历程
- 收稿日期: 2022-11-06
- 修回日期: 2022-12-24
- 网络出版日期: 2023-02-10
- 刊出日期: 2023-01-31

Research Progress on Abstract Interpretation and Its Application

Chen Liqian^1,,
Fan Guangsheng^{1, 3,},
Yin Banghu^2, ,,
Wang Ji^{1, 3,}

1.
College of Computer Science and Technology, National University of Defense Technology, Changsha 410073
2.
College of Systems Engineering, National University of Defense Technology, Changsha 410073
3.
State Key Laboratory of High Performance Computing (National University of Defense Technology), Changsha 410073

Funds: This work was supported by the National Key Research and Development Program of China (2022YFA1005101), the National Natural Science Foundation of China (61872445, 62032024, 62102432), and the Natural Science Foundation of Hunan Province (2021JJ40697).

摘要

摘要:
抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论. 抽象解释自20世纪70年代提出以来，在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用. 近年来，抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展. 基于此，系统综述了抽象解释及其应用的研究进展. 首先概述了抽象解释理论的基本概念，介绍了抽象解释理论、抽象域的研究进展；然后概述了基于抽象解释的程序分析方面的研究进展; 之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展；又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用进展进行了介绍；最后指明了抽象解释未来可能的研究方向.
- 抽象解释 /
- 程序语义 /
- 程序分析 /
- 形式验证 /
- 抽象域
Abstract:
Abstract interpretation is a theory of abstraction and approximation of the mathematical structures used in the formal description of complex systems and the inference or verification of their properties. Since being proposed in 1970 s, abstract interpretation has been widely applied to many fields, including semantic models, program analysis and verification, verification of hybrid systems, program transformation, analysis of systems biology models, etc. In recent years, abstract interpretation has made great progress in program analysis, neural network verification, completeness reasoning, improvement of abstract domains, etc. Based on this, we systematically review the research progress of abstract interpretation and its applications. Firstly, we outline the basic concepts of abstract interpretation theory, and review the recent research progress of abstract interpretation theory and abstract domains; then, we review the recent research progress in abstract interpretation-based program analysis, verification and robust training of neural networks, analysis of deep learning programs; after that, we also review the progress of some other applications of abstract interpretation, including trustworthiness assurance of smart contract, information security, and quantum computing; At last, potential future directions in the field of abstract interpretation are pointed out.
- abstract interpretation /
- program semantics /
- program analysis /
- formal verification /
- abstract domain

HTML全文

国密SM4算法^[1]是一种常用的分组密码算法，广泛应用于数据保护、加密通信等领域. SM4算法常见工作模式有ECB（electronic codebook），CBC（cipher block chaining）等，对于相同的明文块，ECB模式下会产生完全相同的密文，而在CBC模式下，当前的明文块会与前一块的密文异或后进行运算. 因此，即使是完全相同的明文输入也可能会有完全不同的密文输出. 相比于ECB模式，CBC模式提供了更高的安全性和抵抗攻击的能力，有着更高的应用需求. 提高SM4算法在CBC模式下的性能，对于在边缘设备中使用SM4算法是至关重要的. 但是，在CBC模式下存在着难以提高吞吐率的问题：每组的输入必须等待前一组运算结束后才能获得，因而难以使用流水线方法提升吞吐率.

文献[2]中提到了一种改进方法，将电路中的S盒以外的其他逻辑结构进行预计算，并把预计算的结果与S盒进行融合构成新的查找表，从而提高SM4算法在CBC模式下吞吐率. 本文基于此工作进一步优化了S盒的表示，并针对轮函数的迭代过程进行了优化，最终减少了轮函数关键路径上的2次异或运算，有效提高了算法的性能.

本文的设计针对CBC模式下的SM4算法，在TSMC 40 nm，SMIC 55 nm工艺下，使用Synopsys Design Compiler分别进行了ASIC综合. 综合结果显示，本文所提出的设计在CBC模式下的吞吐率达到了4.2 Gb/s，同时单位面积吞吐量达到了129.4 Gb·s⁻¹·mm⁻²，明显优于已发表的类似设计. 这些结果表明本文所提出的化简方法在改进SM4算法性能方面具有很大的潜力.

本文的结构为：首先介绍了SM4算法及其在CBC模式下存在的性能瓶颈问题. 然后，详细描述了本文提出的2个化简方法，并解释了它们在轮函数迭代和S盒置换过程中的作用. 接下来，介绍了实验设计并给出了实验结果分析和对比. 最后，对进一步改进和应用的方向进行了展望.

1. SM4算法介绍

SM4算法是一种对称密钥密码算法，被广泛应用于数据加密和保护领域，它是中国密码算法的标准之一，具有较高的安全性和良好的性能.

SM4采用了分组密码的设计思想，将明文数据划分为128 b的数据块，并通过密钥对每个数据块进行加密和解密操作. 对单组数据进行加解密的流程如所示，分为密钥扩展算法和加解密算法2部分. 中的 $FK$ 是系统预设的参数，与用户密钥进行异或运算后作为密钥扩展算法的输入. 加解密算法接受密钥扩展算法产生的32轮轮密钥 $r{k_i}$ 对明文进行加解密，最后经反序变换输出. 加解密使用的是同一套计算流程，唯一的区别是解密时使用轮密钥的顺序与加密过程相反.

图 1 SM4算法工作流程

Figure 1. Workflow of SM4 algorithm

下载: 全尺寸图片幻灯片

密钥扩展算法和加解密算法2部分均由32次轮函数迭代构成，整体结构均采用4路并行的Feistel结构，在计算过程中，以128 b数据为输入、128 b数据为输出，其内部的运算逻辑如图2所示. 输出中的前96 b数据等于输入中的后96 b数据，输出后的32 b数据通过轮函数运算产生.

图 2 4路并行的Feistel结构

Figure 2. Four parallel Feistel structure

下载: 全尺寸图片幻灯片

在密钥扩展算法中使用的密钥是算法给定的固定密钥，记作 $c{k_i}$ . 在加解密算法中使用的密钥是由密钥扩展算法通过用户给的密钥扩展出来的轮密钥，记作 $r{k_i}$ .

1.1 SM4密钥扩展算法

SM4密钥扩展算法结构如所示，密钥扩展的主要过程包括32轮密钥扩展的轮函数，其中，密钥为128 b， $FK$ 为SM4标准中规定的一个128 b常数. 二者异或后的值将会作为密钥扩展轮函数的首轮输入，并通过一个选择器进行循环迭代，总计迭代32轮产生32个轮密钥.

图 3 SM4的密钥扩展算法结构

Figure 3. Key expansion algorithm structure of SM4

下载: 全尺寸图片幻灯片

设用户输入的密钥为 $MK$ ，则该密钥对应的32轮轮密钥可以按照式（1）求出：

$\left\{ {\begin{aligned} & {({k_0},{k_1},{k_2},{k_3}) = MK \oplus FK}, \\ & {{k_{i + 4}} = {k_i} \oplus F({k_{i + 1}} \oplus {k_{i + 2}} \oplus {k_{i + 3}} \oplus c{k_i})}, \\ &{r{k_i} = {k_{i + 4}}} , \end{aligned}} \right.$

(1)

其中， $c{k_i}$ 是系统预设的32 b参数， $r{k_i}$ 代表第 $i$ 轮的轮密钥， $F$ 代表密钥扩展轮函数，其由S盒置换算法 $\tau :Z_2^{32} \to Z_2^{32}$ 和线性变换算法 $L(x) = x \oplus (x \lt \lt \lt 13) \oplus (x \lt \lt \lt 23)$ 组成，其中 $\lt \lt \lt$ 表示循环左移运算.

1.2 SM4加解密算法

SM4算法的加解密算法的整体结构与密钥扩展算法类似，均包含32轮的轮函数迭代，区别在于加解密算法中额外包含1次反序变换.

SM4算法的轮函数迭代流程如所示， ${X_1}$ ~ ${X_4}$ 为第1轮的输入， ${X_2}$ ~ ${X_5}$ 为第1轮的输出，同时也是第2轮的输入. $r{k_1}$ 为第1轮的轮密钥， $T$ 函数代表加解密模块的轮函数. 与密钥扩展部分的轮函数 $F$ 类似，由S盒置换算法 $\tau$ 和一个线性变换算法 $L'(x)=x\oplus (x \lt \lt \lt 2) \oplus (x \lt \lt \lt 10)$ $\oplus\, (x \lt \lt \lt 18) \oplus (x \lt \lt \lt 24)$ 组成.

图 4 SM4加解密模块轮函数结构

Figure 4. Round function structure of SM4 encryption and decryption modules

下载: 全尺寸图片幻灯片

2. 对SM4加解密算法关键路径的化简

通过多轮的迭代过程，SM4算法能够实现高强度的数据加密和解密. 然而，在CBC模式下，由于相邻数据之间的依赖关系，传统的流水线技术难以提高算法的吞吐率. 因此，针对这一问题，本文提出了2种化简方法，以减少关键路径上的运算，从而提高SM4算法在CBC模式下的性能.

2.1 轮函数优化

加解密模块的轮函数的结构如所示，若不考虑 $T$ 函数带来的时序延迟，单次轮函数迭代的关键路径上共包含3次异或运算. 以公式的形式描述SM4算法加解密轮函数的迭代关系可得到式（2）：

${X_{i + 4}} = {X_i} \oplus ({X_{i + 1}} \oplus {X_{i + 2}} \oplus {X_{i + 3}} \oplus r{k_i}) .$

(2)

若考虑相邻的2次轮函数迭代，则有：

$\left\{ {\begin{aligned} & {{X_{i + 4}} = {X_i} \oplus T({X_{i + 1}} \oplus {X_{i + 2}} \oplus {X_{i + 3}} \oplus r{k_i})}, \\ & {{X_{i + 5}} = {X_i} \oplus T({X_{i + 2}} \oplus {X_{i + 3}} \oplus {X_{i + 4}} \oplus r{k_{i + 1}})}. \end{aligned}} \right.$

(3)

观察式（1）~（3）不难发现，由于SM4采用了4条数据线路的Feistel结构进行设计，在相邻的2次轮函数迭代过程中，均有96 b的输入是完全一致的，在式（3）的计算过程中，相邻2轮的轮函数将 ${X_{i + 2}} \oplus {X_{i + 3}}$ 计算了2次.

因此，一个简单的优化思路便是，我们在轮函数之间传递数据时，额外传递 ${X_{i + 2}} \oplus {X_{i + 3}} \oplus r{k_{i + 1}}$ 的运算结果，并作用于下一次计算，得到的流程图如图5所示.

图 5 优化的轮函数结构

Figure 5. Optimized round function structure

下载: 全尺寸图片幻灯片

相比于图4的运算流程，在计算当前轮次的输出时，二次优化过后的轮函数通过提前获取下一轮次使用的密钥，并利用2轮之间相同的数据提前计算，可以使得在加解密的流程中总计节省32次异或运算的时间.

2.2 S盒性能优化

S盒是密码学领域的一个基本组件，其功能是实现数据的非线性变换，在DES，AES，SM1，SM4等算法中均有应用. 在SM4算法中，其提供了一个8 b到8 b的非线性变换.

在SM4算法中，S盒模块通常与另一个线性变换函数 $L'$ 组合使用，即图4和中的T函数，其位于加解密算法轮函数的关键路径上，因此，如果能找到优化 $T$ 函数关键路径的方法延时，也可以使得整个加解密模块的延时变小，进而提高运算效率. $T$ 函数的内部结构如所示，图中的 $\lt \lt \lt$ 表示对32 b数据进行循环左移，关键路径包括1个S盒和3次异或运算. 在硬件实现中，循环移位可以通过硬件连线来实现，不会带来额外的路径延时.

图 6 SM4加解密模块T函数结构

Figure 6. T function structure of SM4 encryption and decryption modules

下载: 全尺寸图片幻灯片

$T$ 函数中包含4次异或运算，反映到电路设计中，其关键路径上至少存在3次异或运算. 因此，一个优化思路便是，将算法中的S盒的输入输出修改为8 b输入、32 b输出^[2-3] ，并提前将 $L'$ 函数作用于图中的4个S盒，如图7所示. 中，通过编码的形式保存其运行结果，将中的SBox与后续的线性变换 $L'$ 组合形成exSBox，之后仅需要将4个exSBox的输出异或即可，从而减少了1次异或运算.

图 7 优化的T函数结构

Figure 7. Optimized T-function structure

下载: 全尺寸图片幻灯片

虽然修改后的S盒比原先的S盒输出了更多的数据，但在硬件实现中，仍然是通过相同数量的多路选择器查表输出. 因此修改前后的S盒的路径延时及其安全性并未改变.

2.3 S盒面积优化

以中的exSBox1为例，使用 $\rm 0xff$ 作为输入展示exSBox1的构造方式，首先获得 $\rm 0xff$ 作用于S盒后的运行结果 $\rm 0x48$ . 由于exSBox1的输入对应最高四位，因此，将其拓展为32 b数据为 $\rm 0x48000000$ . 在经过 $L'$ 函数后，得到的值是 $\rm 0x68492121$ . 如表1所示，表中前5行加粗部分表示传入的数据及其循环移位后所处位置，其余位置在任意输入下都恒等于0.

表 1 搜索空间降低比率和命中率

Table 1. Search Space Reduction Rate and Hit Rate

原数据	01001000	00000000	00000000	00000000
<<<2	00100000	00000000	00000000	00000001
<<<10	00000000	00000000	00000001	00100000
<<<18	00000000	00000001	00100000	00000000
<<<24	00000000	01001000	00000000	00000000
异或和	01101000	01001001	00100001	00100001
注：加粗部分表示传入的数据及其循环移位后所处位置.

下载: 导出CSV

| 显示表格

观察表1的运算结果不难发现，除最后一行加粗数字表示的第0~5位，第14，15位由异或运算产生，其余的24位均是输入的8位数据的排列组合，因此在硬件设计时，可以仅使用8 b输入、16 b输出的S盒实现. 对于图7中剩余的3个exSBox，在相同的输入下，可以通过对表1中的数据进行循环移位，得到对应的输出. 上述结论对4个位于不同部位的S盒均成立.

具体而言，令 $p$ 为输入的8 b数据， $\tau (p)$ 为标准SM4算法中S盒的输出. $X = ({x_0},{x_1}, \cdots ,{x_{15}})$ 为exSBox1中存储的16 b数据， $Y = ({y_0},{y_1}, \cdots, {y_{31}})$ 为优化后的 $T$ 函数中需要的32 b输出. $\tau$ 为SM4算法标准中使用的S盒置换函数，其对于8 b输入，产生对应的8 b输出，则 $X$ 可以由式（4）产生：

$\left\{ {\begin{aligned} & {({x_0},{x_1}, \cdots, {x_7}) = \tau (p)} ,\\ & {({x_8},{x_9}, \cdots ,{x_{15}}) = \tau (p) \oplus (\tau (p) \lt \lt \lt 2)} . \end{aligned}} \right.$

(4)

由可知， $Y$ 的取值实际上可以由 $X$ 经过排列组合得到，对于exSBox2，exSBox3，exSBox4的取值，可以通过 $Y$ 循环移位得到，且由于该过程中仅包含赋值运算，在电路设计中可以通过物理连线完成. 相比于文献[2]中的设计，节约了1/3的面积消耗. 具体的计算方式如式（5）所示.

$\left\{\begin{split} & (y_0,y_1,\cdots,y_5)=(x_8,x_9,\cdots,x_{13})， \\ &(y_6,y_7）=(x_6,x_7)， \\ &(y_8,y_9,\cdots,y_{13})=(x_0,x_1,\cdots,x_5)， \\ &(y_{14},y_{15}）=(x_{14},x_{15})， \\ &(y_{16},y_{17},\cdots,y_{21})=(x_2,x_3,\cdots,x_7)， \\ &(y_{22},y_{23}）=(x_0,x_1)， \\ &(y_{24},y_{25},\cdots,y_{29})=(x_2,x_3,\cdots,x_7)， \\ &(y_{30},y_{31}）=(x_0,x_1). \end{split} \right.$

(5)

3. 硬件实现与实验对比

现场可编程逻辑门阵列（FPGA）和专用集成电路（ASIC）是目前主流使用硬件电路实现密码算法的2个方式. FPGA虽然具有可编程性、灵活性和快速设计等优势，但ASIC相较于FPGA拥有更高的性能，与本文设计追求的高效率目标相符，所以选择在ASIC下实现.

3.1 硬件整体设计

SM4硬件系统的整体结构设计如所示，包括密钥扩展模块、加解密模块和适配CBC工作模式的组合逻辑. 对于单个加解密任务，若明文被分为 $n$ 组，会执行1次密钥扩展和 $n$ 次加解密. 因此，优化加解密算法的执行效率是优化SM4硬件设计的重点. 本文所提出的2种化简方法，对于每一组明文输入，可以减少64级异或门的延时，极大地提升了运算效率.

图 8 SM4硬件整体架构

Figure 8. Overall architecture of SM4 hardware

下载: 全尺寸图片幻灯片

3.2 加解密模块设计

SM4算法的硬件实现主要有2种方案：一种方案是流水线结构，即通过寄存器连接多个加解密模块同时工作以提高加解密的效率，如（a）所示；另一种方案是使用循环迭代的方式. 即一次性提取32个轮函数中的 $n$ 轮组合成一个组合电路，称为 $n$ 合1电路，如（b）所示. 流水线结构的优势是可以充分利用 $n$ 个加密核心的性能，在不影响整体工作频率的情况下加速运算. 对于SM4算法而言，在合理范围内堆叠流水线可以实现极高的吞吐量.

图 9 流水线结构与循环迭代结构

Figure 9. Pipeline architecture and loop iteration architecture

下载: 全尺寸图片幻灯片

然而，流水线结构仅适用于ECB等数据无前后依赖的工作模式. 在CBC工作模式下，由于需要将前一轮的输出与本轮的输入进行异或运算，相邻的数据存在依赖，故而无法使用流水线加速运算. 因此，在本设计中没有选用流水线结构.

虽然循环迭代结构会降低整体模块的工作频率，对吞吐量的提升较为有限，但可以同时兼容 ECB，CBC这 2种工作模式. 本设计最终选择了循环迭代的设计方式.

3.3 密钥扩展模块设计

在SM4算法中，密钥扩展与加解密算法类似，均包含32轮迭代. 密钥扩展模块采用图2所示的单轮组合逻辑电路循环32次来实现32轮迭代.

在密钥扩展模块的输出端，使用寄存器存放每一轮电路的轮密钥，标号为0~31，如所示. 标号从0开始的好处是：在解密时，使用到的密钥顺序相反的，加密的第 $k$ 轮使用的是第 $k - 1$ 号密钥，解密的第 $k$ 轮使用的是第 $32 - k$ 号密钥. 在二进制下，二者的标号可以通过取反操作相互转化.

图 10 轮密钥的存储与使用

Figure 10. Storage and usage of round keys

下载: 全尺寸图片幻灯片

为了保证运算结果的准确性，密钥扩展模块还会向加解密模块发出控制信号表明自己的工作状态，以避免在轮密钥尚未完全更新时使用错误的轮密钥进行加解密.

3.4 综合验证方案

在国家标准文档^[1]中，并没有针对CBC工作模式给出具体的测试用例. 因此，本文设计方案通过完整的Verilog HDL语言实现，通过在FPGA平台进行综合、仿真和上板验证，以确保功能正确并进行相关性能分析，如图11所示. 具体而言，通过PCIE上位机下发随机的明文数据到FPGA开发板，开发板完成加密后传回上位机，通过与软件对比实现功能验证. 若在循环验证多次后二者的输出均完全相同，则认为设计的SM4电路的功能正确.

图 11 测试流程

Figure 11. Testing procedures

下载: 全尺寸图片幻灯片

最终，本文的设计在Zynq 7020 FPGA开发板上完成了上板验证，确保了功能的正确性，工作频率最高可达95 MHz，吞吐量约为1.5 Gb/s.

3.5 ASIC综合结果

ASIC上主要针对2种工艺SMIC 55 nm与 TSMC 40 nm进行了测试、通过Synopsys公司的EDA工具DesignCompiler进行时序等综合约束，我们选择了芯片面积和芯片使用的逻辑门数量（gates）作为评估指标，其结果如表2和表3所示，在CBC模式下，本文的设计在3.97 mW的功耗下，单位面积吞吐率达129.4 Gb·s⁻¹·mm⁻²，明显优于同类设计. 此外，以使用逻辑门的数量为评估标准，本文提出的设计在该指标上也明显优于同类设计，单位面积吞吐率为0.205×10⁻³ Gb·s⁻¹·gates⁻¹.

表 2 SM4综合结果与面积效率对比

Table 2. Comparison of SM4 Synthesis Results and Area Efficiency

工艺节点	芯片面积/mm²	吞吐率/（Gb·s⁻¹）	单位面积吞吐率/ （Gb·s⁻¹·mm⁻²）	功耗/mW
40 nm^*	0.0335	4.34	129.40	3.97
55 nm^*	0.0877	4.41	50.30	10.88
65 nm^[2]	0.1260	5.24	41.59
180 nm^[4]	0.0790	0.10	1.27	5.31
55 nm^[5]	0.0870	0.40	4.59	4.35
350 nm^[6]	0.0270	0.412	15.26
注：*标注的表示本文的结果.

下载: 导出CSV

| 显示表格

表 3 SM4综合结果与门效率对比

Table 3. Comparison of SM4 Synthesis Results and Gates Efficiency

工艺节点	gates	吞吐率/（Gb·s⁻¹）	单位面积吞吐率/ （Gb·s⁻¹·gates⁻¹）
40 nm^*	21.2×10³	4.34	0.205×10⁻³
55 nm^*	21.1×10³	4.41	0.209×10⁻³
180 nm^[6]	32.0×10³	0.80	0.025×10⁻³
65 nm^[7]	31.0×10³	1.23	0.040×10⁻³
55 nm^[8]	22.0×10³	0.27	0.012×10⁻³
130 nm^[9]	22.0×10³	0.80	0.036×10⁻³
注：*标注的表示本文的结果.

下载: 导出CSV

| 显示表格

在不同工艺、电压下对该设计进行综合，可以得到本文设计在不同使用场景下的吞吐率. 在TSMC 40 nm、SMIC 55 nm、SMIC 130 nm下使用不同的工艺角分别对本文的设计进行综合，结果如表4所示.

表 4 不同工艺角下的SM4综合结果与效率对比

Table 4. Comparison of SM4 Synthesis Results and Efficiency with Different Process Corners

工艺节点	工艺角	面积/gates	吞吐率/（Gb·s⁻¹）	功耗/mW
40 nm	0.99V/125°C/SS	21.0×10³	2.40	2.55
	1.1V/25°C/TT	21.2×10³	4.34	3.97
	1.21V/0°C/FF	20.9×10³	6.96	8.35
55 nm	1V/25°C/TT	20.0×10³	2.78	4.10
	1.2V/25°C/TT	21.1×10³	4.41	10.88
	1.32V/0°C/FF	17.8×10³	6.84	33.59
130 nm	1.08V/125°C/SS	20.8×10³	1.11	6.86
	1.2V/25°C/TT	21.0×10³	1.75	15.70
	1.32V/0°C/FF	21.8×10³	2.45	23.03

下载: 导出CSV

| 显示表格

4. 结　　论

根据本文提出的2种对SM4加解密模块关键路径进行化简以及降低面积的方法，实现了4合1的SM4电路，并基于Zynq7020开发板进行了功能验证. 此外，ASIC综合结果表明本文的SM4电路相比于其他方案有更高的单位面积吞吐率和更低的功耗. 因此，这种对SM4算法进行的优化是有效的，并且对其他分组算法提高CBC模式下的单位面积吞吐率具有参考价值.

作者贡献声明：郝泽钰提出研究方案并完成了论文的撰写；代天傲、黄亦成、段岑林协助完成了ASIC平台上的验证实验；董进、吴世勇、张博、王雪岩、贾小涛提出指导意见并修改论文；杨建磊提出指导意见并讨论定稿.

表 1 基于抽象解释的程序分析工具

Table 1 Program Analyzers Based on Abstract Interpretation

工具	编写语言	目标程序	开源情况	主要特点
Astrée^[5]	OCaml	C/C++	商业化	组合多种抽象域、分析精度高
CGS^[80]	C	C	内部使用	基于分布式实现
Polyspace^[3]		C/C++, Ada	商业化	工具成熟、功能丰富
Sparrow^[81]	OCaml	C	商业化&开源	稀疏分析、可选择过程间敏感分析
IKOS^[82]	C++	C/C++	开源	并行不动点迭代、Gauge抽象域
Frama-C^[83]	OCaml	C	开源	值范围分析
Infer^[84]	OCaml	Java, C/C++ , Objective-C	开源	组合分析、增量分析
Goblint^[85]	OCaml	C	开源	中断、并发程序缺陷检测
Dai^[86]	OCaml	C	开源	需求驱动抽象解释
Clam^[87-88]	C++	LLVM字节码	开源	不变式生成
SPARTA^[89]	C++		开源	高性能抽象解释库
Mopsa^[90]	OCaml	C, Python	开源	模块化、多语言支持
MemCAD^[91]	OCaml	C	开源	形态分析
Interproc^[92]	OCaml	SPL	开源	不变式生成、上下文不敏感过程间分析、支持Apron抽象域库
CodeHawk^[93-94]	OCaml	C, Java字节码, 二进制程序	开源	多语言支持

下载: 导出CSV

参考文献(190)

[1]	Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[C] //Proc of the 4th ACM SIGACT-SIGPLAN Symp on Principles of Programming Languages. New York: ACM, 1977: 238−252
[2]	Cousot P. Principles of Abstract Interpretation[M]. Cambrideg, MA: MIT Press, 2021
[3]	MathWorks. Polyspace[EB/OL]. [2022-12-18]. https://ww2.mathworks.cn/products/polyspace.html
[4]	Blanchet B, Cousot P, Cousot R, et al. A static analyzer for large safety-critical software[C] //Proc of the 24th ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2003: 196−207
[5]	Absint. Astrée. [EB/OL]. [2022-12-18]. https://www.absint.com/astree/index.htm
[6]	Miné A. AstréeA: A static analyzer for large embedded multi-task software[C] //Proc of the 16th Int Conf on Verification, Model Checking, and Abstract Interpretation (VMCAI'15). Berlin: Springer, 2015, 8931: 3
[7]	Cousot P, Giacobazzi R, Ranzato F. A²I: Abstract² interpretation[J]. Proceedings of the ACM on Programming Languages, 2019, 3(POPL): 42:1−42:31
[8]	Bruni R, Giacobazzi R, Gori R, et al. A logic for locally complete abstract interpretations[C] //Proc of the 36th Annual ACM/IEEE Symp on Logic in Computer Science (LICS). Piscataway, NJ: IEEE, 2021: 1−13
[9]	Bruni R, Giacobazzi R, Gori R, et al. Abstract interpretation repair[C] //Proc of the 43rd ACM SIGPLAN Int Conf on Programming Language Design and Implementation. New York: ACM, 2022: 426−441
[10]	Campion M, Dalla Preda M, Giacobazzi R. Partial (In) completeness in abstract interpretation: Limiting the imprecision in program analysis[J]. Proceedings of the ACM on Programming Languages, 2022, 6(POPL): 59:1−59:31
[11]	Bonchi F, Ganty P, Giacobazzi R, et al. Sound up-to techniques and complete abstract domains[C] //Proc of the 33rd Annual ACM/IEEE Symp on Logic in Computer Science. Piscataway, NJ: IEEE, 2018: 175−184
[12]	Bruni R, Giacobazzi R, Gori R, et al. Abstract extensionality: On the properties of incomplete abstract interpretations[J]. Proceedings of the ACM on Programming Languages, 2019, 4(POPL): 28:1−28:28
[13]	Stein B, Chang B Y E, Sridharan M. Demanded abstract interpretation[C] //Proc of the 42nd ACM SIGPLAN Int Conf on Programming Language Design and Implementation. New York: ACM, 2021: 282−295
[14]	Wei Guannan, Chen Yuxuan, Rompf T. Staged abstract interpreters: Fast and modular whole-program analysis via meta-programming[J]. Proceedings of the ACM on Programming Languages, 2019, 3(OOPSLA): 1−32
[15]	Futamura Y. Partial evaluation of computation process—an approach to a compiler-compiler[J]. Systems, Computers, Controls, 1971, 2(5): 45−50
[16]	Feldman Y M Y, Sagiv M, Shoham S, et al. Property-directed reachability as abstract interpretation in the monotone theory[J]. Proceedings of the ACM on Programming Languages, 2022, 6(POPL): 15:1−31
[17]	Jeannet B, Miné A. APRON: A library of numerical abstract domains for static analysis[C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2009: 661−667
[18]	Singh G, Püschel M, Vechev M. A practical construction for decomposing numerical abstract domains[J]. Proceedings of the ACM on Programming Languages, 2017, 2(POPL): 55:1−55:28
[19]	Bagnara R, Hill P M, Zaffanella E. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems[J]. Science of Computer Programming, 2008, 72(1-2): 3−21 doi: 10.1016/j.scico.2007.08.001
[20]	Becchi A, Zaffanella E. PPLite: Zero-overhead encoding of NNC polyhedra[J]. Information and Computation, 2020, 275: 104620.
[21]	Boulmé S, Marechaly A, Monniaux D, et al. The verified polyhedron library: An overview[C] //Proc of the 20th Int Symp on Symbolic and Numeric Algorithms for Scientific Computing. Piscataway, NJ: IEEE, 2018: 9−17
[22]	Singh G, Püschel M, Vechev M. Making numerical program analysis fast[J]. ACM SIGPLAN Notices, 2015, 50(6): 303−313 doi: 10.1145/2813885.2738000
[23]	Singh G, Püschel M, Vechev M. Fast polyhedra abstract domain[C] //Proc of the 44th ACM SIGPLAN Symp on Principles of Programming Languages. New York: ACM, 2017: 46−59
[24]	Gange G, Ma Z, Navas J A, et al. A fresh look at zones and octagons[J]. ACM Transactions on Programming Languages and Systems, 2021, 43(3): 1−51
[25]	Chawdhary A, Robbins E, King A. Incrementally closing octagons[J]. Formal Methods in System Design, 2019, 54(2): 232−277 doi: 10.1007/s10703-017-0314-7
[26]	Chen Junjie, Cousot P. A binary decision tree abstract domain functor[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2015: 36−53
[27]	Chen Liqian, Yin Banghu, Wei Dengping, et al. An abstract domain to infer linear absolute value equalities[C] //Proc of the 2021 Int Symp on Theoretical Aspects of Software Engineering (TASE). Piscataway, NJ: IEEE, 2021: 47−54
[28]	Chen Liqian, Wei Dengping, Yin Banghu, et al. Static analysis of linear absolute value equalities among variables of a program[J]. Science of Computer Programming, 2023, Volume 225, Article 102906, 18 pages.
[29]	Gange G, Navas J A, Schachte P, et al. Disjunctive interval analysis[C]//Proc of the Int Static Analysis Symp. Berlin: Springer, 2021: 144−165
[30]	Gurfinkel A, Chaki S. Boxes: A symbolic abstract domain of boxes[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2010: 287−303
[31]	Maréchal A, Monniaux D, Périn M. Scalable minimizing-operators on polyhedra via parametric linear programming[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2017: 212−231
[32]	Becchi A, Zaffanella E. A direct encoding for NNC polyhedra[C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2018: 230−248
[33]	Bagnara R, Hill P M, Zaffanella E. Not necessarily closed convex polyhedra and the double description method[J]. Formal Aspects of Computing, 2005, 17(2): 222−257 doi: 10.1007/s00165-005-0061-1
[34]	Amato G, Scozzari F, Seidl H, et al. Efficiently intertwining widening and narrowing[J]. Science of Computer Programming, 2016, 120: 1−24 doi: 10.1016/j.scico.2015.12.005
[35]	Boutonnet R, Halbwachs N. Improving the results of program analysis by abstract interpretation beyond the decreasing sequence[J]. Formal Methods in System Design, 2018, 53(3): 384−406 doi: 10.1007/s10703-017-0310-y
[36]	Cha S, Jeong S, Oh H. Learning a strategy for choosing widening thresholds from a large codebase[C] //Proc of the Asian Symp on Programming Languages and Systems. Berlin: Springer, 2016: 25−41
[37]	Reps T, Sagiv M, Yorsh G. Symbolic implementation of the best transformer[C] //Proc of the Int Workshop on Verification, Model Checking, and Abstract Interpretation. Berlin: Springer, 2004: 252−266
[38]	Bjørner N, Phan A D, Fleckenstein L. ΝZ-AN optimizing SMT solver[C] //Proc of the Int conf on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2015: 194−199
[39]	Li Yi, Albarghouthi A, Kincaid Z, et al. Symbolic optimization with SMT solvers[J]. ACM SIGPLAN Notices, 2014, 49(1): 607−618 doi: 10.1145/2578855.2535857
[40]	Jiang Jiahong, Chen Liqian, Wu Xueguang, et al. Block-wise abstract interpretation by combining abstract domains with smt[C] //Proc of the Int Conf on Verification, Model Checking, and Abstract Interpretation. Berlin: Springer, 2017: 310−329
[41]	Yao Peisen, Shi Qingkai, Huang Heqing, et al. Program analysis via efficient symbolic abstraction[J]. Proceedings of the ACM on Programming Languages, 2021, 5(OOPSLA): 118:1−118:32
[42]	Farzan A, Kincaid Z. Compositional recurrence analysis[C] //Proc of the 2015 Formal Methods in Computer-Aided Design (FMCAD). Piscataway, NJ: IEEE, 2015: 57−64
[43]	Kincaid Z, Breck J, Boroujeni A F, et al. Compositional recurrence analysis revisited[J]. ACM SIGPLAN Notices, 2017, 52(6): 248−262 doi: 10.1145/3140587.3062373
[44]	Kincaid Z, Cyphert J, Breck J, et al. Non-linear reasoning for invariant synthesis[J]. Proceedings of the ACM on Programming Languages, 2017, 2(POPL): 54:1−54:33
[45]	Allamigeon X, Gaubert S, Goubault E, et al. A fast method to compute disjunctive quadratic invariants of numerical programs[J]. ACM Transactions on Embedded Computing Systems, 2017, 16(5s): 1−19
[46]	Yin Banghu, Chen Liqian, Liu Jiangchao, et al. Verifying numerical programs via Iterative abstract testing[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2019: 247−267
[47]	Toman J, Grossman D. Concerto: A framework for combined concrete and abstract interpretation[J]. Proceedings of the ACM on Programming Languages, 2019, 3(POPL): 43:1−43:29
[48]	Chen Tianyi, Heo K, Raghothaman M. Boosting static analysis accuracy with instrumented test executions[C] //Proc of the 29th ACM Joint Meeting on European Software Engineering Conf and Symp on the Foundations of Software Engineering. New York: ACM, 2021: 1154−1165
[49]	O'Hearn P W. Incorrectness logic[J]. Proceedings of the ACM on Programming Languages, 2019, 4(POPL): 10:1−10:32
[50]	Raad A, Berdine J, Dang H H, et al. Local reasoning about the presence of bugs: Incorrectness separation logic[C] //Proc of Int Conf on Computer Aided Verification. Berlin: Springer, 2020: 225−252
[51]	Raad A, Berdine J, Dreyer D, et al. Concurrent incorrectness separation logic[J]. Proceedings of the ACM on Programming Languages, 2022, 6(POPL): 34:1−34:29
[52]	Le Q L, Raad A, Villard J, et al. Finding real bugs in big programs with incorrectness logic[J]. Proceedings of the ACM on Programming Languages, 2022, 6(OOPSLA1): 81:1−81:27
[53]	Ascari F, Bruni R, Gori R. Limits and difficulties in the design of under-approximation abstract domains[C] //Proc of the Int Conf on Foundations of Software Science and Computation Structures. Berlin: Springer, 2022: 21−39
[54]	Kim S K, Venet A J, Thakur A V. Deterministic parallel fixpoint computation[J]. Proceedings of the ACM on Programming Languages, 2019, 4(POPL): 14:1−14:33
[55]	Brat G, Navas J A, Shi N, et al. IKOS: A framework for static analysis based on abstract interpretation[C] //Proc of the Int Conf on Software Engineering and Formal Methods. Berlin: Springer, 2014: 271−277
[56]	Ramalingam G. Identifying loops in almost linear time[J]. ACM Transactions on Programming Languages and Systems, 1999, 21(2): 175−188 doi: 10.1145/316686.316687
[57]	Kim S K, Venet A J, Thakur A V. Memory-efficient fixpoint computation[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2020: 35−64
[58]	Park J, Lee H, Ryu S. A survey of parametric static analysis[J]. ACM Computing Surveys, 2021, 54(7): 1−37
[59]	Heo K, Oh H, Yi K. Machine-learning-guided selectively unsound static analysis[C] //Proc of the IEEE/ACM 39th Int Conf on Software Engineering (ICSE). Piscataway, NJ: IEEE, 2017: 519−529
[60]	Heo K, Oh H, Yang H. Resource-aware program analysis via online abstraction coarsening[C] //Proc of the IEEE/ACM 41st Int Conf on Software Engineering (ICSE). Piscataway, NJ: IEEE, 2019: 94−104
[61]	Singh G, Püschel M, Vechev M. Fast numerical program analysis with reinforcement learning[C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2018: 211−229
[62]	He Jingxuan, Singh G, Püschel M, et al. Learning fast and precise numerical analysis[C] //Proc of the 41st ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2020: 1112−1127
[63]	Liu Jiangchao, Chen Liqian, Rival X. Automatic verification of embedded system code manipulating dynamic structures stored in contiguous regions[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2018, 37(11): 2311−2322 doi: 10.1109/TCAD.2018.2858462
[64]	Journault M, Miné A, Ouadjaout A. Modular static analysis of string manipulations in C programs[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2018: 243−262
[65]	Illous H, Lemerre M, Rival X. A relational shape abstract domain[J]. Formal Methods in System Design, 2021, 57(3): 343−400 doi: 10.1007/s10703-021-00366-4
[66]	Illous H, Lemerre M, Rival X. Interprocedural shape analysis using separation logic-based transformer summaries[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2020: 248−273
[67]	Li Huisong, Berenger F, Chang B Y E, et al. Semantic-directed clumping of disjunctive abstract states[J]. ACM SIGPLAN Notices, 2017, 52(1): 32−45 doi: 10.1145/3093333.3009881
[68]	Wang Di, Hoffmann J, Reps T. PMAF: An algebraic framework for static analysis of probabilistic programs[J]. ACM SIGPLAN Notices, 2018, 53(4): 513−528 doi: 10.1145/3296979.3192408
[69]	Chakarov A, Sankaranarayanan S. Expectation invariants for probabilistic program loops as fixed points[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2014: 85−100
[70]	Cousot P, Monerau M. Probabilistic abstract interpretation[C] //Proc of the European Symp on Programming. Berlin: Springer, 2012: 169−193
[71]	Monniaux D. Abstract interpretation of probabilistic semantics[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2000: 322−339
[72]	Gershuni E, Amit N, Gurfinkel A, et al. Simple and precise static analysis of untrusted Linux kernel extensions[C] //Proc of the 40th ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2019: 1069−1084
[73]	Ouadjaout A, Miné A, Lasla N, et al. Static analysis by abstract interpretation of functional properties of device drivers in TinyOS[J]. Journal of Systems and Software, 2016, 120: 114−132 doi: 10.1016/j.jss.2016.07.030
[74]	Carbonneaux Q, Hoffmann J, Shao Z. Compositional certified resource bounds[C] //Proc of the 36th ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2015: 467−478
[75]	Fan Guangsheng, Chen Taoqing, Yin Banghu, et al. Static bound analysis of dynamically allocated resources for C programs[C] //Proc of the 2021 IEEE 32nd Int Symp on Software Reliability Engineering (ISSRE). Piscataway, NJ: IEEE, 2021: 390−400
[76]	Çiçek E, Bouaziz M, Cho S, et al. Static resource analysis at scale[C] //Proc of Int Static Analysis Symp. Berlin: Springer, 2020: 3−6
[77]	Rivera J, Franchetti F, Püschel M. An interval compiler for sound floating-point computations[C] //Proc of the 2021 IEEE/ACM Int Symp on Code Generation and Optimization (CGO). Piscataway, NJ: IEEE, 2021: 52−64
[78]	Rivera J, Franchetti F, Püschel M. A compiler for sound floating-point computations using affine arithmetic[C] //Proc of the 2022 IEEE/ACM Int Symp on Code Generation and Optimization (CGO). Piscataway, NJ: IEEE, 2022: 66−78
[79]	Ye Yapeng, Zhang Zhuo, Shi Qingkai, et al. D-ARM: Disassembling ARM Binaries by Lightweight Superset Instruction Interpretation and Graph Modeling[C/OL] //Proc of the 2023 IEEE Symp on Security and Privacy (SP). [2022-12-18]. https://qingkaishi.github.io/public_pdfs/SP23DARM.pdf
[80]	Venet A, Brat G. Precise and efficient static array bound checking for large embedded C programs[J]. ACM SIGPLAN Notices, 2004, 39(6): 231−242 doi: 10.1145/996893.996869
[81]	Oh H, Heo K, Lee W, et al. Sparrow[EB/OL]. [2022-12-18]. https://github.com/ropas/sparrow
[82]	Brat G, Navas J A, Shi N, et al. IKOS[EB/OL]. [2022-12-18]. https://github.com/NASA-SW-VnV/ikos
[83]	Alberti M, Antignac T, Barany G, et al. Frama-C[EB/OL]. [2022-12-18]. https://frama-c.com/
[84]	Villard J, Berdine J, Blackshear S, et al. Infer[EB/OL]. [2022-12-18]. https://github.com/facebook/infer
[85]	Seidl H, Erhard J, Vojdani V, et al. Goblint[EB/OL]. [2022-12-18]. https://goblint.in.tum.de/home
[86]	Stein B, Chang B Y E, Sridharan M, et al. Dai[EB/OL]. [2022-12-18]. https://hub.nuaa.cf/cuplv/dai
[87]	Navas J A, Gurfinkel A, Kahsai T, et al. Clam[EB/OL]. [2022-12-18]. https://hub.nuaa.cf/seahorn/clam
[88]	Navas J A, Su Yusen, Kahsai T, et al. Crab[EB/OL]. [2022-12-18].https://hub.nuaa.cf/seahorn/crab
[89]	Chen Yuxuan, Gorski N, Arthaud M, et al. SPARTA[EB/OL]. [2022-12-18].https://github.com/facebook/SPARTA
[90]	Miné A, Milanese M, Bau G, et al. Mopsa[EB/OL]. [2022-12-18].https://gitlab.com/mopsa/mopsa-analyzer
[91]	Rival X, Illous H, Lemerre M, et al. MemCAD[EB/OL]. [2022-12-18].https://gitlab.inria.fr/memcad/memcad
[92]	Jeannet B. Interproc[EB/OL]. [2022-12-18]. http://pop-art.inrialpes.fr/interproc/interprocweb. cgi
[93]	Sipma H, Schuffelen A C, et al. CodeHawk[EB/OL]. [2022-12-18].https://github.com/static-analysis-engineering /codehawk
[94]	Kestrel Technology LLC. Kestrel Technology Products[EB/OL]. [2022-12-18]. http://kestreltechnology.com/technology. html
[95]	Cousot P, Cousot R, Feret J, et al. Why does Astrée scale up?[J]. Formal Methods in System Design, 2009, 35(3): 229−264 doi: 10.1007/s10703-009-0089-6
[96]	Cousot P, Cousot R, Feret J, et al. The ASTRÉE analyzer[C] //Proc of the European Symp on Programming. Berlin: Springer, 2005: 21−30
[97]	Oh H, Heo K, Lee W, et al. Design and implementation of sparse global analyses for C-like languages[C] //Proc of the 33rd ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2012: 229−238
[98]	Oh H, Heo K, Lee W, et al. Global sparse analysis framework[J]. ACM Transactions on Programming Languages and Systems, 2014, 36(3): 1−44
[99]	Oh H, Lee W, Heo K, et al. Selective context-sensitivity guided by impact pre-analysis[C] //Proc of the 35th ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2014: 475−484
[100]	Lee W, Lee W, Yi K. Sound non-statistical clustering of static analysis alarms[C] //Proc of Int Workshop on Verification, Model Checking, and Abstract Interpretation. Berlin: Springer, 2012: 299−314
[101]	Venet A J. The gauge domain: scalable analysis of linear inequality invariants[C] //Proc of Int Conf on Computer Aided Verification. Berlin: Springer, 2012: 139−154
[102]	Baudin P, Bobot F, Bühler D, et al. The dogged pursuit of bug-free C programs: The Frama-C software analysis platform[J]. Communications of the ACM, 2021, 64(8): 56−68 doi: 10.1145/3470569
[103]	Kirchner F, Kosmatov N, Prevosto V, et al. Frama-C: A software analysis perspective[J]. Formal Aspects of Computing, 2015, 27(3): 573−609 doi: 10.1007/s00165-014-0326-7
[104]	Distefano D, Fähndrich M, Logozzo F, et al. Scaling static analyses at Facebook[J]. Communications of the ACM, 2019, 62(8): 62−70 doi: 10.1145/3338112
[105]	Calcagno C, Distefano D. Infer: An automatic program verifier for memory safety of C programs[C] //Proc of NASA Formal Methods Symp. Berlin: Springer, 2011: 459−465
[106]	Calcagno C, Distefano D, Dubreil J, et al. Moving fast with software verification[C] //Proc of NASA Formal Methods Symp. Berlin: Springer, 2015: 3−11
[107]	Harman M, O'Hearn P. From start-ups to scale-ups: Opportunities and open problems for static and dynamic program analysis[C] //Proc of the 2018 IEEE 18th Int Working Conf on Source Code Analysis and Manipulation (SCAM). Piscataway, NJ: IEEE, 2018: 1−23
[108]	Calcagno C, Distefano D, O’hearn P W, et al. Compositional shape analysis by means of bi-abduction[J]. Journal of the ACM, 2011, 58(6): 1−66
[109]	Vojdani V, Apinis K, Rõtov V, et al. Static race detection for device drivers: The Goblint approach[C] //Proc of the 2016 31st IEEE/ACM Int Conf on Automated Software Engineering (ASE). Piscataway, NJ: IEEE, 2016: 391−402
[110]	Schwarz M, Saan S, Seidl H, et al. Improving thread-modular abstract interpretation[C] //Proc of Int Static Analysis Symp. Berlin: Springer, 2021: 359−383
[111]	Seidl H, Vogler R. Three improvements to the top-down solver[C] //Proc of the 20th Int Symp on Principles and Practice of Declarative Programming. New York: ACM, 2018: 1−14
[112]	Seidl H, Vogler R. Three improvements to the top-down solver[J]. Mathematical Structures in Computer Science, 2022, 1: 45
[113]	Vojdani V, Vene V. Goblint: Path-sensitive data race analysis[J]. ANNALES Universitatis Scientiarum Budapestinensis de Rolando Eötvös Nominatae Sectio Computatorica, 2009, 30: 141−155
[114]	Seidl H, Erhard J, Vogler R. Incremental abstract interpretation[M] //From Lambda Calculus to Cybersecurity Through Program Analysis. Berlin: Springer, 2020: 132−148
[115]	Erhard J, Saan S, Tilscher S, et al. Interactive abstract interpretation: Reanalyzing whole programs for cheap[J]. arXiv preprint, arXiv: 2209.10445, 2022
[116]	Monat R, Ouadjaout A, Miné A. A multilanguage static analysis of python programs with native C extensions[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2021: 323−345
[117]	Monat R, Ouadjaout A, Miné A. Static type analysis by abstract interpretation of Python programs[C] //Proc of the 34th European Conf on Object-Oriented Programming (ECOOP 2020). Dagstuhl: Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020（17）: 1−29
[118]	Fromherz A, Ouadjaout A, Miné A. Static value analysis of Python programs by abstract interpretation[C] //Proc of NASA Formal Methods Symp. Berlin: Springer, 2018: 185−202
[119]	Jeannet B. Interproc analyzer for recursive programs with numerical variables[J/OL].[2022-12-20] . https://pop-art. inrialpes.fr/~bjeannet/bjeannet-forge/interproc/manual.pdf
[120]	Gehr T, Mirman M, Drachsler-Cohen D, et al. AI²: Safety and robustness certification of neural networks with abstract interpretation[C] //Proc of the 2018 IEEE symp on Security and Privacy (SP). Piscataway, NJ: IEEE, 2018: 3−18
[121]	Liu Changliu, Arnon T, Lazarus C, et al. Algorithms for verifying deep neural networks [J]. arXiv preprint, arXiv: 1903.06758, 2019
[122]	Huang Xiaowei, Kroening D, Kwiatkowska M, et al. Safety and trustworthiness of deep neural networks: A survey [J]. arXiv preprint, arXiv: 1812.08342, 2018
[123]	卜磊, 陈立前, 董云卫, 等. 人工智能系统的形式化验证技术研究进展与趋势[R]. CCF 2019−2020中国计算机科学技术发展报告. 北京: 机械工业出版社, 2020: 91−539 Bu Lei, Chen Liqian, Dong Yunwei, et al. Research progress and trends on formal verification of artificial intelligence systems[R]. CCF 2019−2020 Progress Report on Chinese Computer Science and Technology. Beijing: China Machine Press, 2020, 491−539 (in Chinese)
[124]	Albarghouthi A. Introduction to neural network verification[J]. Foundations and Trends® in Programming Languages, 2021, 7(1–2): 1−157
[125]	Huang P S, Stanforth R, Welbl J, et al. Achieving Verified Robustness to Symbol Substitutions via Interval Bound Propagation[C] //Proc of the 2019 Conf on Empirical Methods in Natural Language Processing and the 9th Int Joint Conf on Natural Language Processing (EMNLP-IJCNLP 19). Stroudsburg, PA: Association for Computational Linguistics, 2019: 4081−4091.
[126]	Mirman M, Baader M, Vechev M. The fundamental limits of interval arithmetic for neural networks[J]. arXiv preprint, arXiv: 2112.05235, 2021
[127]	Wang Shiqi, Pei Kexin, Whitehouse J, et al. Formal security analysis of neural networks using symbolic intervals[C] //Proc of the 27th USENIX Security Symp (USENIX Security’18). Berkeley, CA: USENIX Association, 2018: 1599−1614
[128]	Wang Shiqi, Pei Kexin, Whitehouse J, et al. Efficient formal safety analysis of neural networks[C] //Proc of the 32nd Int Conf on Neural Information Processing Systems. Cambrideg, MA: MIT Press, 2018: 6369−6379
[129]	Yin Banghu, Chen Liqian, Liu Jiangchao, et al. Efficient complete verification of neural networks via layer-wised splitting and refinement[J]. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2022, 41(11): 3898−3909 doi: 10.1109/TCAD.2022.3197534
[130]	Baader M, Mirman M, Vechev M. Universal approximation with certified networks[J]. arXiv preprint, arXiv: 1909.13846, 2019
[131]	Wang Zi, Albarghouthi A, Prakriya G, et al. Interval universal approximation for neural networks[J]. Proceedings of the ACM on Programming Languages, 2022, 6(POPL): 14:1−14:29
[132]	Singh G, Gehr T, Mirman M, et al. Fast and effective robustness certification[C] //Proc of the 32nd Int Conf on Neural Information Processing Systems. Cambridge, MA: MIT Press, 2018: 10825−10836
[133]	Singh G, Gehr T, Püschel M, et al. Boosting robustness certification of neural networks[C/OL] //Proc of the Int Conf on Learning Representations. 2018 [2022-12-20].https://openreview.net/pdf?id= HJgeEh09KQ
[134]	Jordan M, Hayase J, Dimakis A G, et al. Zonotope domains for Lagrangian neural network verification[J]. arXiv preprint, arXiv: 2210.08069, 2022
[135]	Singh G, Gehr T, Püschel M, et al. An abstract domain for certifying neural networks[J]. Proceedings of the ACM on Programming Languages, 2019, 3(POPL): 41:1−41:30
[136]	Tran H D, Bak S, Xiang Weiming, et al. Verification of deep convolutional neural networks using imagestars[C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2020: 18−42
[137]	Goubault E, Palumby S, Putot S, et al. Static analysis of ReLU neural networks with tropical polyhedra[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2021: 166−190
[138]	Müller C, Serre F, Singh G, et al. Scaling polyhedral neural network verification on GPUS[J]. Proceedings of Machine Learning and Systems, 2021, 3: 733−746
[139]	Salman H, Yang G, Zhang Huan, et al. A convex relaxation barrier to tight robustness verification of neural networks[C] //Proc of the 33rd Int Conf on Neural Information Processing Systems. Cambrideg, MA: MIT Press, 2019: 9835−9846
[140]	Singh G, Ganvir R, Püschel M, et al. Beyond the single neuron convex barrier for neural network certification[C] //Proc of the Advances in Neural Information Processing Systems. Cambrideg, MA: MIT Press, 2019, 15098−15109
[141]	Clarisó R, Cortadella J. The octahedron abstract domain[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2004: 312−327
[142]	Tjandraatmadja C, Anderson R, Huchette J, et al. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification[C] //Proc of the Advances in Neural Information Processing Systems. Cambridge, MA: MIT Press, 2020, 33: 21675−21686
[143]	De Palma A, Behl H S, Bunel R, et al. Scaling the convex barrier with active sets[C/OL] //Proc of the ICLR Conf. 2021. [2022-12-20].https://arxiv.org/pdf/2101.05844v1.pdf
[144]	Müller M N, Makarchuk G, Singh G, et al. PRIMA: General and precise neural network certification via scalable convex hull approximations[J]. Proceedings of the ACM on Programming Languages, 2022, 6(POPL): 43:1−43:33
[145]	Li Jianlin, Liu Jiangchao, Yang Pengfei, et al. Analyzing deep neural networks with symbolic propagation: Towards higher precision and faster verification[C] //Proc of the Int Static Analysis Symp. Berlin: Springer, 2019: 296−319
[146]	Yang Pengfei, Li Jianlin, Liu Jiangchao, et al. Enhancing robustness verification for deep neural networks via symbolic propagation[J]. Formal Aspects of Computing, 2021, 33(3): 407−435 doi: 10.1007/s00165-021-00548-1
[147]	Elboher Y Y, Gottschlich J, Katz G. An abstraction-based framework for neural network verification[C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2020: 43−65
[148]	Weng Lily, Zhang Huan, Chen Hongge, et al. Towards fast computation of certified robustness for relu networks[C/OL]//Proc of the Int Conf on Machine Learning, 2018 [2022-12-20]. https://arxiv.org/abs/1804.09699
[149]	Zhang Huan, Weng Tsuiwei, Chen Pinyu, et al. Efficient neural network robustness certification with general activation functions[C/OL]//Proc of Advances in Neural Information Processing Systems. Cambridge, MA: MIT Press, 2018 [2022-12-20].https://arxiv.org/abs/1811.00866
[150]	Bastani O, Ioannou Y, Lampropoulos L, et al. Measuring neural net robustness with constraints[C/OL] //Proc of Advances in Neural Information Processing Systems, 2016 [2022-12-20].https://arxiv.org/abs/1605.07262
[151]	Anderson G, Pailoor S, Dillig I, et al. Optimization and abstraction: A synergistic approach for analyzing neural network robustness[C] //Proc of the 40th ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2019: 731−744
[152]	Bunel R R, Turkaslan I, Torr P, et al. A unified view of piecewise linear neural network verification [C/OL] //Proc of Advances in Neural Information Processing Systems, 2018 [2022-12-20]. https://arxiv.org/abs/1711.00455
[153]	Bunel R, Lu J, Turkaslan I, et al. Branch and bound for piecewise linear neural network verification[J]. Journal of Machine Learning Research, 2020, 21(42): 1−39
[154]	Ehlers R. Formal verification of piecewise linear feedforward neural networks [C] //Proc of the Int Symp on Automated Technology for Verification and Analysis. Berlin: Springer, 2017: 269–286
[155]	Katz G, Huang D A, Ibeling D, et al. The Marabou framework for verification and analysis of deep neural networks [C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2019: 443–452
[156]	Katz G, Barrett C, Dill D L, et al. Reluplex: An efficient SMT solver for verifying deep neural networks [C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2017: 97–117
[157]	Wang Shiqi. Efficient neural network verification using branch and bound[D]. Columbia: Columbia University, 2022
[158]	Zhang Hongce, Shinn M, Gupta A, et al. Verification of recurrent neural networks for cognitive tasks via reachability analysis[C/OL] //Proc of the 24th European Conf on Artificial Intelligence, 2020 [2022-12-20].https://ecai2020.eu/papers/1492_paper.pdf
[159]	Akintunde M E, Kevorchian A, Lomuscio A, et al. Verification of RNN-based neural agent-environment systems[C] //Proc of the AAAI Conf on Artificial Intelligence. Mento Park, CA: AAAI, 2019: 6006−6013.
[160]	Jacoby Y, Barrett C, Katz G. Verifying recurrent neural networks using invariant inference[C] //Proc of the Int Symp on Automated Technology for Verification and Analysis. Berlin: Springer, 2020: 57−74
[161]	Ko C Y, Lyu Zhaoyang, Weng L, et al. POPQORN: Quantifying robustness of recurrent neural networks[C] //Proc of the Int Conf on Machine Learning. 2019: 3468−3477.
[162]	Ryou W, Chen Jiayu, Balunovic M, et al. Scalable polyhedral verification of recurrent neural networks[C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2021: 225−248
[163]	Weiss G, Goldberg Y, Yahav E. Extracting automata from recurrent neural networks using queries and counterexamples[C] //Proc of the Int Conf on Machine Learning. New York: ACM, 2018: 5247−5256
[164]	Khmelnitsky I, Neider D, Roy R, et al. Property-directed verification and robustness certification of recurrent neural networks[C] //Proc of the Int Symp on Automated Technology for Verification and Analysis. Berlin: Springer, 2021: 364−380
[165]	Mirman M, Gehr T, Vechev M. Differentiable abstract interpretation for provably robust neural networks[C] //Proc of the Int Conf on Machine Learning. New York: ACM, 2018: 3578−3586
[166]	Gowal S, Dvijotham K, Stanforth R, et al. On the effectiveness of interval bound propagation for training verifiably robust models[J]. arXiv preprint, arXiv: 1810.12715, 2018
[167]	Fischer M, Balunovic M, Drachsler-Cohen D, et al. Dl2: Training and querying neural networks with logic[C] //Proc of the Int Conf on Machine Learning. New York: ACM, 2019: 1931−1941
[168]	Zhang Yuhao, Albarghouthi A, D ’Antoni L. Robustness to programmable string transformations via augmented abstract training[C] //Proc of the Int Conf on Machine Learning. New York: ACM, 2020: 11023−11032
[169]	Zhang Yuhao, Albarghouthi A, D’Antoni L. Certified robustness to programmable transformations in LSTMs[J]. arXiv preprint, arXiv: 2102.07818, 2021
[170]	Jia Robin, Raghunathan A, Göksel K, et al. Certified robustness to adversarial word substitutions[J]. arXiv preprint, arXiv: 1909.00986, 2019
[171]	Xu Kaidi, Shi Zhouxing, Zhang Huan, et al. Automatic perturbation analysis for scalable certified robustness and beyond[J]. Advances in Neural Information Processing Systems, 2020: 1129−1141
[172]	Huang P S, Stanforth R, Welbl J, et al. Achieving verified robustness to symbol substitutions via interval bound propagation[J]. arXiv preprint, arXiv: 1909.01492, 2019
[173]	Zhang Yuhao, Ren Luyao, Chen Liqian, et al. Detecting numerical bugs in neural network architectures[C] //Proc of the 28th ACM Joint Meeting on European Software Engineering Conf and Symp on the Foundations of Software Engineering. New York: ACM, 2020: 826−837
[174]	Pérez V, Klemen M, López-García P, et al. Cost analysis of smart contracts via parametric resource analysis[C] //Proc of Int Static Analysis Symp. Berlin: Springer, 2020: 7−31
[175]	Grech N, Kong M, Jurisevic A, et al. Madmax: Surviving out-of-gas conditions in ethereum smart contracts[J]. Proceedings of the ACM on Programming Languages, 2018, 2(OOPSLA): 116:1−116:27
[176]	Kalra S, Goel S, Dhawan M, et al. Zeus: Analyzing safety of smart contracts[C] //Proc of NDSS 2018. San Diego, CA: University of California, 2018: 1−12
[177]	Giacobazzi R, Mastroeni I. Abstract non-interference: Parameterizing non-interference by abstract interpretation[J]. ACM SIGPLAN Notices, 2004, 39(1): 186−197 doi: 10.1145/982962.964017
[178]	Giacobazzi R, Mastroeni I. Abstract non-interference: A unifying framework for weakening information-flow[J]. ACM Transactions on Privacy and Security, 2018, 21(2): 1−31
[179]	Mastroeni I, Pasqua M. Statically analyzing information flows: An abstract interpretation-based hyperanalysis for non-interference[C] //Proc of the 34th ACM/SIGAPP Symp on Applied Computing. New York: ACM, 2019: 2215−2223
[180]	Köpf B, Mauborgne L, Ochoa M. Automatic quantification of cache side-channels[C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2012: 564−580
[181]	Doychev G, Köpf B, Mauborgne L, et al. Cacheaudit: A tool for the static analysis of cache side channels[J]. ACM Transactions on information and system security, 2015, 18(1): 1−32
[182]	Barthe G, Köpf B, Mauborgne L, et al. Leakage resilience against concurrent cache attacks[C] //Proc of the Int Conf on Principles of Security and Trust. Berlin: Springer, 2014: 140−158
[183]	Doychev G, Köpf B. Rigorous analysis of software countermeasures against cache attacks[C] //Proc of the 38th ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2017: 406−421
[184]	Wang Shuai, Bao Yuyan, Liu Xiao, et al. Identifying cache-based side channels through secret-augmented abstract interpretation[C] //Proc of the 28th USENIX Security Symp (USENIX Security’19). Berkeley, CA: USENIX Associatio, 2019: 657−674
[185]	Touzeau V, Maïza C, Monniaux D, et al. Ascertaining uncertainty for efficient exact cache analysis[C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2017: 22−40
[186]	Wu Meng, Guo Shengjian, Schaumont P, et al. Eliminating timing side-channel leaks using program repair[C] //Proc of the 27th ACM SIGSOFT Int Symp on Software Testing and Analysis. New York: ACM, 2018: 15−26
[187]	Blazy S, Pichardie D, Trieu A. Verifying constant-time implementations by abstract interpretation[J]. Journal of Computer Security, 2019, 27(1): 137−163 doi: 10.3233/JCS-181136
[188]	Wu Meng, Wang Chao. Abstract interpretation under speculative execution[C] //Proc of the 40th ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2019: 802−815
[189]	Fang Zhiyong, Darais D, Near J P, et al. Zero knowledge static program analysis[C] //Proc of the 2021 ACM SIGSAC Conf on Computer and Communications Security. New York: ACM, 2021: 2951−2967
[190]	Yu Nengkun, Palsberg J. Quantum abstract interpretation[C] //Proc of the 42nd ACM SIGPLAN Int Conf on Programming Language Design and Implementation. New York: ACM, 2021: 542−558

施引文献(13)

期刊类型引用(2)

1.	祁磊，任子豪，刘俊汐，耿新. 虚实结合的行人重识别方法. 计算机研究与发展. 2025(02): 418-431 . 本站查看
2.	程思雨，陈莹. 伪标签细化引导的相机感知无监督行人重识别方法. 光电工程. 2023(12): 62-76 . 百度学术