基于携带证明代码的IP核安全性验证方法

　　摘要：针对集成电路在RTL代码级设计阶段由于使用第三方IP软核引入的安全性问题，现有的功能测试方法较难实现全覆盖检测无法保障电路安全性。本文在已有基于携带证明代码思想的基础上改进提出一种安全性验证方法。该方法结合形式化验证平台coq，运用形式化逻辑描述电路代码和安全性假设，构造证明过程并采用系统的证明检查器验证证明过程。通过在DES电路代码的实验，说明了该验证方法能有效检测出电路中后门路径类型的硬件木马。相比较于测试类方法覆盖率不能达到100%而无法确定电路是非安全性，本文提出的方法可以确定电路是安全或非安全，能够保证电路代码级的安全可信性。

　　关键词：第三方IP核;硬件木马;携带证明的代码;形式化验证

　　随着SoC设计技术的发展，为缩短开发周期，可复用的IP核在SoC设计中被广泛应用。大量第三方IP软核的使用，使得硬件木马攻击者有可乘之机，导致电路有泄露信息、功能瘫痪、丧失自主控制能力等威胁[1-3]，因此需要强有力的检测手段确保第三方IP软核的可信性。

　　目前，针对IP软核的检测方法，主要有基于测试[4-6]和形式化验证方法[7-8]。基于测试的方法只有测试到电路设计有不符合需求之处时才能说明电路是不可靠的，是一种证伪的思想，由于测试向量并不能遍历所以可能输入向量，而当没有测试到不符合项时不能确定电路是绝对安全可靠的，因此这种证伪的方法具有一定局限性。形式化验证方法有3种类型：模型验证、等价验证和属性验证。模型验证当电路规模较大时存在空间爆炸问题，不适合用于大规模电路[9-10]。

　　等价验证是指电路设计每个层次的功能针对原有功能目标都需要去进行验证，如验证RTL级和综合后电路之间的相等性[11]。属性验证用于第三方IP核的信号安全性验证，通常结合IP核特定属性、测试覆盖率或门级网表，来验证IP核是否含木马电路[12]。本文在属性验证时引入了携带证明代码思想同时作出了改进，并在形式化验证平台上进行安全性验证。

　　1验证方法

　　1.1携带证明代码原理

　　基于携带证明代码的思想进行安全性验证，主要分成两阶段：第一阶段是IP提供者与IP使用者关于IP核属性达成一致观点，提供者不仅提供IP核代码，同时提供IP核满足安全属性的证明过程[13-14]。这些属性和证明过程需要与IP核独立开描述，采用形式化表示提供给IP使用者。第二阶段是IP使用者在使用IP核时，必须先验证IP核代码是否发生篡改，只有通过形式化证明验证的IP核才被认为是安全可靠的。由于电路的数据安全属性一旦被形式化证明了，就不可能会插入硬件木马使电路属性不改变而且证明验证能够通过。

　　因此，本文提出的方法能够给IP软核使用者提供一种简单有效的机制进行安全性验证，避免IP设计阶段引入的安全威胁。根据携带证明代码的原理进行IP软核的安全性验证时，需要采用形式化描述方法表示属性和证明过程，即形式化验证技术。形式化验证技术是指在特定的形式系统(通常是数理逻辑系统)中对程序及其执行环境构造形式模型，并在形式模型上对代码的各种特性进行逻辑推理和证明[15]。相比于其他的验证技术，形式化验证技术优势在于它是一种保证结果完备性的技术，也就是说如果能够证明电路代码满足特定的属性，那么相应的集成电路就一定满足这个性质，是一个证真的过程。

　　1.2形式化验证流程

　　携带证明代码思想进行IP软核安全性验证时需要IP软核提供者和使用者共同合作，其中主要是IP软核提供者要提供安全性属性的证明过程，由于SoC设计过程中常常会使用多个厂家提供的IP核，我们不可能要求每个IP提供者都提供属性证明过程，而且这些证明过程都使用同样的形式化描述语言。由于安全属性的定义是通过逻辑功能定义的，整个证明过程构造可以通过逻辑推理来得到。

　　在验证证明过程时，若有子定理与电路设定不符，表示IP软核中有木马电路;否则定理证明过程通过，IP核满足安全属性，因此我们在已有基于携带证明代码思想的基础上改进提出一种安全性验证方法，所有验证工作都由IP使用者执行。

　　分为两阶段，第一阶段是确定安全属性和证明过程，即根据需求确定IP核应满足的属性并构造属性证明的过程;第二阶段是检查证明过程的正确性，即根据证明过程对属性进行推导，若证明检查过程成立则IP核满足属性，若证明不通过表示IP核不满足安全属性，存在木马电路。由于大规模电路的推导过程复杂，人工推导容易出错，所以第二阶段借助已有形式化验证工具完成。我们采用计算机辅助定理证明工具coq(CoqDevelopmentTeam)作为开发平台[16]。选用coq平台的语言Gallina作为形式化描述语言表示电路、属性和证明过程，证明的逻辑基础选用归纳构造演算作为验证框架的元逻辑。

　　coq系统主要由证明开发系统和证明检查器构成。证明开发系统中我们可以用Gallina语言设置相对应的安全属性规范，而且可以使用证明策略构造证明过程。证明检查器主要用来验证被形式化表示的安全性规范即定理，能否通过证明过程文件来完成证明。

　　在证明过程中，coq采用反向推导的方法构造证明，即当将某个策略应用到目标程序上时，系统会根据策略产生相对应的子目标，每一个子目标都使用数字进行标识，通过对各个子目标的证明来完成整个程序的证明过程。在将Coq内安全策略应用到一个给定目标时，系统会对应用该策略需要符合的前提条件进行比对，如果比对结果是不符合，那么则该策略就会应用失败。两者协调可以非常有效地证明从电路代码中抽取的定理的正确性。

　　2实例验证

　　为了证明本文中提出的检测方法能够验证电路中的木马，我们采用DES电路的Verilog代码作为验证对象。DES作为国际通用的加密算法，对信号的保密性区分要求较高，将DES算法的Verilog代码描述作为待验证安全属性的IP核具有很高的代表性。接下来，我们将说明如何运用coq形式化逻辑表示DES电路和电路属性[17]，在coq开发系统中描述待证明的属性并构造证明过程，最后运用证明检查器分析证明过程得出结论。

　　2.1逻辑描述的相关定义

　　根据前述验证方法的描述可知，本文提出的验证方法是在coq验证平台上完成，由于该验证平台无法对Verilog代码进行识别，需要将DES算法等价转化为coq开发平台能够识别的Gallina语言描述，同时待验证属性和证明过程都需要用Gallina语言描述。将Verilog代码转化为coq系统描述需要研究的定义的内容包括：描述电路的形式化模型和代码转化规则。描述电路的形式化模型主要定义了：信号的定义、信号的运算规则、电路表达式类型的描述。

　　2.2安全性设定

　　验证DES算法电路的安全属性时，主要是验证电路中没有信息泄露路径，即需要保密的信息如明文和密钥，经过加密电路后，在输出的密文中不含有保密信息。因此假定：对信号添加密级属性，信号的密级有secure、non_secure两种，同时对信号添加密级。Inductivesecurity:=secure|non_secure.Definitionbus:=nat->(bus_label*security).需要保密的信息，即明文和密钥是秘密的信号。在电路运算时电路信号的密级属性会发生变化，变化可能秘密信号变成非密信号、密级不发生改变或者非密信号变成秘密信号，对应了降密，维持或者升密3种运算。在加密电路中，我们认为移位变换是一种降密运算，其他电路运算都是维持密级不变的运算。

　　2.3验证

　　在coq系统中证明电路的安全性，需要将上述安全性假设转化为待证明的定理，即在DES电路中输入desIn，key密级为secure，输出信号desout密级为non_secure，转化为coq系统描述如下：Axiomsecret_key:forall(c:nat)，bus_senkeyc=secure.Axiomsecret_desIn:forall(c:nat)，bus_send⁃esInc=secure.Theoremno_leaking_des:forall(c:nat)，bus_send⁃esoutc=non_secure.由于密钥生成器为保持密级不变的电路模块，所以有K_sub的密级为secure，转化为coq系统描述如下：Axiomsecret_K_sub:forall(c:nat)，bus_senK_subc=secure.确定输入假设和待证明定理后，需要构造证明过程，coq系统采用的推理逻辑是反向的归纳构造演算的逻辑。

　　所以需要从待证明定理开始展开，即desout开始展开，从电路的输出端开始往前推算，直到找到与输入信号相关时可直接进行比对，证明过程完成。在构造证明过程中，可以运用coq系统提供的证明策略描述每一步证明过程，如展开desout用unfolddesout，简化表达式用simpl。形式化验证需要采用coq系统的证明检查器进行验证，验证内容包括转化后的电路的逻辑描述的准确性，待证明定理准确性和证明过程演算。其中证明过程演算中一旦发生与假设定理矛盾就会证明失败，则说明电路代码中有木马电路。

　　3结论

　　SoC设计时第三方IP软核的使用，导致在RTL代码级设计阶段极易被植入硬件木马，为及早从设计源头发现电路中被插入的硬件木马，本文提出了基于携带证明代码思想改进的形式化验证方法。通过在DES电路上验证说明，该方法是对电路进行代码级分析，能有效检测出改变电路中信号路径类型的硬件木马。

　　相比较于测试类证伪的方法，本文提出方法是一种完备的证真的方法，可靠性更高。形式化验证方法在验证软硬件可靠性方面的应用已较为成熟，在验证电路代码级安全性方面的研究是一个较新的研究方向，具体的技术细节如电路转化模型、代码的自动化转化等都需要深入研究，这些技术的成熟必将提高形式化验证的可适用范围和易用性。

　　参考文献：

　　[1]SalmaniH，TehranipoorM.Analyzingcircuitvul⁃nerabilitytohardwareTrojaninsertionatthebehav⁃iorallevel[J].IEEEInternationalSymposiumonDefectandFaultToleranceinVLSIandNanotech⁃nologySystems，2013，79(2):190-195.

　　[2]李杰，肖立伊，赤诚，等.基于SoC系统的IP核评测平台开发[J].微电子学与计算机，2017，34(6):45-48.

　　[3]周昱，于宗光.硬件木马威胁与识别技术综述[J].信息网络安全，2016(1):11-17.

　　[4]ReeceT，RobinsonWH.Detectionofhardwaretrojansinthird-partyintellectualpropertyusinguntrustedmodules[J].IEEETransactionsonComputer-aidedDesignofIntegratedCircuitsandSystems，2016，35(3):357-366.

　　[5]WaksmanA，SuozzoM，SethumadhavanS.FAN⁃CI:identificationofstealthymaliciouslogicusingbooleanfunctionalanalysis[C]//ProceedingsofAC⁃MSigsacConferenceonComputer&Communica⁃tionsSecurity，2013:697-708.

　　[6]闫淑梅，邹明亮.IP软核测试策略及验证方法研究[J].电子设计工程，2013，21(4):98-100.

　　[7]RajendranJ，DhandayuthapanyA，VedulaV，etal.Formalsecurityverificationofthirdpartyintellectualpropertycoresforinformationleakage[C]//Proceedingsof29thInternationalConferenceonVLSIDesign&15thInternationalConferenceonEmbeddedSystems.2016:547-552.

　　相关刊物推荐：《信息网络安全》论文发表官方网站 是公安部主管，公安部第三研究所主办的综合性专业月刊，是公安部公共信息网络安全监察局及其下属各网络安全监察部门对外宣传的窗口。