硬件安全门级细粒度形式化验证方法

秦茂源，慕德俊，胡 伟，毛保磊

(西北工业大学 深圳研究院，广东 深圳 518057)

近年来硬件安全问题频频发生，造成的后果日益严重，例如伊朗核电站震网事件，攻击者通过网络激活事先植入的硬件木马使电机转子超负荷运转烧毁．然而，现今硬件设计仍缺乏有效的安全验证方法检测，导致硬件设计中存在潜在的安全漏洞、木马、恶意程序等[1]．现有的安全验证技术主要包含仿真和形式化验证技术，但是仿真技术存在覆盖率难以保证的问题．

形式化验证技术采用严格的数学定义描述电路规范，形式化检查硬件行为特征．现有的形式化验证技术包括模型检验和定理证明．模型检验采用搜索算法验证设计是否满足设计规范，但会因设计规模的增大导致状态空间爆炸．虽然引入符号执行后解决了状态空间爆炸问题，但仍可能导致路径爆炸．而定理证明是采用形式化语言描述程序规范和性质，用演绎的方法交互式地验证程序的规范和性质[2]．PCH(Proof-Carrying Hardware)框架[3-4]首次提出了硬件可携带证明代码的机制描述和验证现场可编程门阵列(Field Programmable Gate Array，FPGA)的比特流文件．PCH-IP(Proof-Carrying Hardware-IP)框架[5-7]在PCH框架上进一步提出了IP核安全性可验证框架．HiFV(Hierarchy-preserving Formal Verification)框架[8]和Enhanced PCH(Enhanced Proof-Carrying Hardware)框架[9]将IP核的验证扩展至片上系统(System on Chip，SoC)的安全性验证．以上方法皆采用形式化语言描述电路的设计规范和安全属性传播规则，通过定理证明的方式验证电路的安全性，但都采用了保守的安全属性传播规则，引入了误报，导致验证结果不精确．

针对现有硬件设计形式化安全验证技术的问题，笔者结合门级信息流跟踪[10]与定理证明的方法，使用形式化语言描述硬件的规范和安全标签传播策略，将硬件设计转化为包含信息流跟踪逻辑的电路语义模型，继而结合霍尔三元组理论构造验证模型安全性的定理；然后使用证明策略验证定理的合理性．

1 门级信息流跟踪概述

门级信息流跟踪是为电路分配表示安全属性的污染标签．考虑受污染的输入对输出的影响，构造可用于追踪信息流动的与、或、非等逻辑门的跟踪逻辑[10]:

其中，a、b和o分别为二输入逻辑与门的输入和输出，at、bt和ot分别为其安全标签．定义逻辑“1”表示受“污染”，逻辑“0”表示“非污染”．假设逻辑与门的输入a被标记为“污染”(at为“1”)，输入b被标记为“非污染”(bt为“0”)，当输入b为“0”时，输出o始终为“0”，输入a对输出没有影响，则ot为“0”．如果输入b为“1”，那么输入a的变化便会导致o发生变化，则ot为“1”，因而可以推导出逻辑与门的追踪逻辑．同理可推导或门、非门的追踪逻辑，如式(2)和式(3)所示．

图1 硬件安全门级细粒度形式化验证方法的流程

2 电路语义模型的生成和验证

硬件安全门级细粒度形式化验证方法包括语义逻辑库的生成、电路语义模型的生成、定理生成和证明生成4个步骤，如图1所示．语义逻辑库定义了用于描述原始电路和跟踪逻辑的语法语句和计算函数；电路语义模型的生成是使用语义逻辑库中的语法语句将硬件设计转化为电路语义模型;定理生成则是使用霍尔三元组理论将电路语义模型转变成待证明的定理;证明生成是使用证明策略和公理开发合理性的证明．

2.1 语义逻辑库的生成

逻辑语义库是对原始电路及其信息流跟踪逻辑的语义描述，其包括原始语义库及追踪语义库．原始语义库定义了描述原始电路的语义语句，该库包括了逻辑值、信号、逻辑值函数、原始表达式、表达式函数、原始赋值表达式、原始赋值函数的定义．而追踪语义库定义了跟踪逻辑的语义语句，该库包括了安全属性、安全标签、安全属性传播函数、追踪表达式、追踪表达式函数、追踪赋值表达式、追踪赋值函数的定义．

2.1.1 原始语义库的生成

在Coq环境下，定义level类型，其构造子“hi”和“lo”表示逻辑“1”和逻辑“0”，如式(4)所示．因为数字电路中信号的逻辑值总是伴随着时钟发生变化，所以构造以自然数t为时间离散单元的一元函数bus表示信号，如式(5)所示．任何声明为bus的信号都可以时间为参数返回该时间节点的逻辑值，例如，信号key被声明为bus(key: bus)，则t时间下的逻辑值可表示为 keyt．逻辑值函数描述了与、或、非等基本逻辑门的逻辑运算规则，例如式(6)是以两个level类型为参数，按照模式匹配返回一个level类型的与逻辑值函数and．其余或门(or)、非门(not)等逻辑值函数也可按照以上方法定义．

在定义函数类型bus及逻辑值函数的基础上，引入原始表达式Exprorig类型，以“树”型结构定义与逻辑构造子、或逻辑构造子、非逻辑构造子和类型转换构造子，分别描述信号之间的与、或、非和类型变换逻辑操作．例如式(7)的类型转换构造子SVorig可将bus类型的信号a以(SVoriga)的方式转换为Exprorig类型的表达式．再如式(8)中的与逻辑构造子ExprAndOrig表示信号a、b的与逻辑操作，先将信号a、b转换为Exprorig类型后，代入到ExprAndOrig中得到式(9)的一个复杂表达式．其计算可通过表达式函数Evalorig以模式匹配的方式将表达式规约为逻辑值函数．例如，将式(9)代入到Evalorig中得到式(10)，而后被规约至式(11)所示的逻辑值函数and．

由于硬件描述语言中赋值行为是一种隐含操作，而Coq并不具备实现这种隐含的操作能力，为此需要定义一种赋值表达式类型以命题逻辑的方式代替表示两个信号之间的赋值行为．定义组合逻辑赋值类型Combine及时序逻辑赋值类型Sequence描述表达式之间的组合逻辑赋值及时序逻辑赋值，如式(12)和式(13)所示．例如Sequence (SVorigo)(ExprAndOrig(SVoriga)(SVorigb))表示了表达式(SVorigo)和表达式(ExprAndOrig(SVoriga)(SVorigb))之间的时序逻辑赋值，将其代入到原始赋值函数update中得到式(14)，继而被规约为式(15)所示的等价命题逻辑．

2.1.2 追踪语义库的生成

为便于逻辑电平和安全属性的逻辑计算，将安全属性、安全标签、逻辑值、信号统一定义为式(4)和式(5)．安全属性传播函数描述了追踪逻辑的逻辑结构，如式(16)所示的或门安全属性传播函数org．追踪表达式类型Exprg按照“树形”结构逐个定义与、或、非等追踪逻辑．例如式(17)所示的“或”追踪逻辑构造子ExprOrg，该构造子表示了4个Exprg类型之间的或跟踪逻辑表达式．该表达式的可被追踪表达式函数Evalg规约至“或”安全属性逻辑函数org．而追踪赋值表达式类型同样采用等价命题的方式表示追踪逻辑表达式之间的赋值．例如使用式(18)的追踪组合逻辑赋值表达式Combineg类型构造(SVgot)和(ExprOrg(SVga)(SVgb)(SVgat)(SVgbt)之间赋值，得到式(19)所示追踪组合逻辑表达式．该表达式可通过追踪赋值函数assigng将式(19)规约为式(20)．

2.2 电路语义模型生成

电路语义模型的生成是依据语义逻辑库将电路网表映射为电路语义模型．该模型是由多个简单合取命题组成的蕴含式，表示条件蕴含关系．每个简单合取命题由追踪赋值函数和原始赋值函数组成，通过合取连接词连接表示必须同时成立．例如式(21)表示了一个输入为a、b、c，输出为o1t的电路语义模型．

2.3 定理生成和证明生成

定理生成依据霍尔逻辑三元组理论，将输入和输出的标签定义作为定理的前条件{P}和后条件{Q}，电路语义模型作为程序C，生成该模型的待证明的定理．对于有多位输出的电路，可首先构造多个单位比特输出的电路语义模型．而后定义相应的子定理，以合取符号连接表示多位输出电路语义模型的定理，如式(22)．子定理的证明即是良性定理的证明，借助辅助证明策略开发满足安全策略的证明．如果所有子定理是良性的，那么定理是良性的，反之定理是非良性的．

定理：子定理1∧子定理2∧…∧子定理n．

(22)

3 实验结果及其分析

3.1 实验设计

采用硬件安全门级细粒度形式化验证方法(Fine-granularity Gate level formal Verification method for hardware security，FGV)和具有保守传播策略的硬件验证方法(security verification method based on Conservative Security Property transition rules， CSP)验证JTAG(Joint Test Action Group)调试接口程序和IWLS(International Workshop on Logic & Synthesis)测试基准，通过统计验证结果，分析FGV精确性的原因和量化两种方法所产生的精确度的差异．

3.2 硬件安全门级细粒度形式化验证方法精确性的原因

JTAG调试接口的输入、输出分别由数据(data)、调试(debug)、选通(En)和输出(out)组成．其工作原理是当En为“hi”时，选通data将数据传输到out，反之选通debug将数据传输到out．在明确功能的基础上，分别为输入、输出分配安全标签datat、Ent、debugt、outt，按照不可信的数据不能影响可信信息系统的完整性安全策略(被标记为“hi”的输入不能将该属性传递至outt)，采用FGV和CSP验证JTAG调试接口程序，结果如表1所示．可以得出，当datat或者debugt为“hi”，或两者皆为“hi”时，采用CSP所得到结果outt皆为“hi”， 输出out总是不可信的．而采用FGV验证时， 仅有部分情况会导致输出不可信．例如表1第3行中data 为“lo”、datat为“lo”、En为“hi”、Ent为“lo”、debug为“lo”、debugt为“hi”的输入组合，其验证后输出的安全标签 outt为 “lo” (即输出是安全的)． 分析原因是 FGV 保证了安全标签传播计算与电路实际工作状态相符合，考虑En信号对支路的选择，阻止了不可信信号在未选通的情况下将不可信的安全属性传递到输出，消除了误报，提高了验证精度．

表1 JTAG接口程序验证部分真值表

3.3 FGV和CSP的精度对比

为对比FGV和CSP两种方法的精确度，遵照秘密的信息不能流向输出的机密性原则(即被标记为“hi”的输入不能流向输出)分别验证IWLS测试集中9Symmel、cordic、frg1、decod、c432、Cm163a、count、cht这8组设计的安全性，将验证得出的非良性子定理的数目作为量化验证精度的指标，表2即为两类方法验证精度的对比统计．

表2 FGV和CSP验证IWLS测试集非良性子定理数目

统计结果表明，在相同约束条件下，CSP得出的非良性子定理数目远超出FGV所得出的非良性子定理数目．例如采用CSP验证decod所得出的非良性子定理数目为480个，等同于子定理总数；而采用FGV验证得到的非良性子定理数目为0．从而得知采用CSP验证，其结果必然存在大量误报．再如将9Symmel验证的子定理总数从162个增加到512个，虽然FGV所验证出的非良性子定理数目有所增长，但仍远小于CSP所验证出的非良性子定理数目．此外，CSP验证cht得出的非良性子定理数目仅占子定理总数的8.6%，但仍旧在数目上远高于FGV所验证出的72个非良性子定理．因而可以得出FGV较之CSP有更高的精度．

4 总 结

笔者提出了硬件安全门级细粒度形式化验证方法，可将硬件代码构造为逻辑门层面上的电路语义模型，继而结合霍尔定理生成可用于电路安全性验证的定理和证明．通过对比硬件安全门级细粒度形式化验证方法和保守传播策略的硬件验证方法验证JTAG接口调试程序的结果，得出了硬件安全门级细粒度形式化验证方法精确性的原因．而后选用IWLS测试集进行验证，统计两类方法所验证出的非良性子定理的数目，量化分析精确性的差异．实验表明，硬件安全门级细粒度形式化验证方法能够精确地验证电路的安全属性，有效地提高了验证覆盖率．