0 引言

    有限域运算在代数编码、数据加密和数字信息处理等领域有着广泛的应用，其运算速度是加密算法运算速度的基础^[1]；如今仅依靠软件实现有限域乘法运算已经难以满足人们对加密解密算法运算速度的需求，而已通过改用专门的硬件来满足市场对有限域乘法运算速率的要求。但是，有限域乘法的硬件实现结构复杂，容易出现潜在的设计缺陷而导致运算错误，甚至会导致加密系统密钥泄漏，从而给系统的信息安全带来巨大威胁^[2]。因此，对有限域乘法器的设计进行可靠性验证是十分必要的。

    众所周知，常用的模拟和仿真验证方法虽易于实现，但验证过程中存在测试空间不完备的问题，难以排除所有的错误。而形式化方法则是使用形式语言分别对系统设计要求的功能和实现进行形式化描述，再通过基于相同形式语言的证明工具依据数学理论来验证系统的正确性，它能保证所验证性质的完备性。目前形式化方法主要有等价性验证、模型检验、定理证明和计算机代数。等价性验证和模型检验方法由于存在状态空间爆炸问题，导致验证的系统规模有限^[3-4]；计算机代数方法主要应用于数学证明，缺乏精确的逻辑概念，难以保障推导过程的可靠性^[5-7]；定理证明方法则需要对待验证的系统实现和系统规范进行形式化建模，并在定理证明器中完成系统实现蕴含系统规范的证明，此法可有效地避免人为推演而造成的证明可靠性问题，更加有利于在验证过程中快速找出验证目标细微的缺陷和不足。

    因此，本文选用基于高阶逻辑的定理证明器HOL4系统作为验证平台，通过层次化方法和基于周期的方法对有限域乘法器形式化建模，并采用定理证明方法完成其可靠性的验证工作。

1 有限域及域运算

1.1 有限域(finite field)

    有限域是由一个有限元素的集合和两个二元运算所组成，记为GF(p)^[8]。有限域中的任意元素可以通过不同的基底来表示，本文以应用最广、研究最多的多项式基有限域乘法器设计作为研究对象。

    常见的有限域算术运算有加法、乘法、除法以及模逆运算等，本文工作仅涉及到加法和乘法，所以对其他有限域算术运算不做详细说明。

1.2 有限域GF(2^m)加法

    有限域加法是通过标准的多项式加法运算来实现的，表达式如下：

1.3 有限域GF(2m)乘法

    有限域乘法运算是加密算法和代数编码的核心运算，基于多项式基的有限域乘法运算的通用表达式为：

    由式(2)可知，基于多项式基有限域乘法运算分为两个运行步骤：多项式乘法和多项式取模。传统的有限域乘法依序执行多项式乘法和多项式取模运算，中间结果位数长，硬件实现资源消耗大，运算效率低。而基于最低位优先(LSB-First)的有限域乘法算法从乘数B的最低位开始通过交叉执行多项式乘法和多项式取模运算，可减少中间结果位长，缩短关键路径，有效地降低乘法运算的空间复杂度和时间复杂度^[9]。

    所以，通过对式(2)进行一系列的变化可以得到基于最低位优先的有限域乘法的表达式，如式(3)、式(4)所示。

2 有限域乘法器的形式化建模

    如前所述，基于定理证明方法对有限域乘法器进行形式化验证，首先需要完成有限域乘法器的形式化模型，建模工作主要分为两个部分：(1)依据算法特性抽取验证的关键性质，即系统的规范，并基于高阶逻辑完成相关性质的描述；(2)分析目标系统的实现电路，构建描述系统实现的高阶逻辑表达式，即完成系统实现的形式化建模。

2.1 有限域乘法器规范的形式化建模

    规范是叙述系统所需要具备的功能和性质。依据上述最低位优先算法，有限域乘法器的功能可描述为：乘法器对输入的乘数InA、InB以及首一不可约多项式P(x)进行相应的多项式乘法和多项式取模运算，得到有限域乘法运算的最终结果C(x)。通过功能分析，可得到有限域乘法的两个基本性质。

    性质1：针对最低位优先算法中的式(3)，当周期i=0时，则对A(x)ⁱ进行初始化置数操作，初始值为输入的乘数InA，否则，A(x)ⁱ的取值等于上一迭代周期结果A(x)^i-1左移一位后再对P(x)进行多项式取模，表述如下：

    性质2：针对最低位优先算法中的式(4)，当周期i=0时，则对部分积累加结果C(x)ⁱ进行初始置数操作，初始值为0；否则，式(3)中上一迭代周期得到的A(x)^i-1和乘数InB的对应位b_i的乘法运算结果，最后再和上一周期部分积结果C(x)进行累加得到当前周期的部分积累加值C(x)ⁱ，即：

    由上文可知，对于有限域GF(2^m)，在最低位优先算法中需要通过m次循环操作才能获得有限域乘法运算的最终结果，即C(x)=C(x)^m。所以基于最低位优先的4位有限域乘法规范的形式化描述是上述2个基本性质的合取，经过4次迭代运算得到最终结果，即：

其中LSB_Shift_B_SPEC定义乘数InB从最低位开始的串行输出值b_i，Input_Module_4为辅助函数，定义数据的类型转换。有限域乘法运算的最后结果即为outC=C⁽⁴⁾。

2.2 有限域乘法器实现的形式化建模

    本文所研究的基于最低位优先算法有限域乘法器的电路实现如图1所示^[10]，该系统通过比特串行的方式经过4个时钟周期可完成4位有限域乘法运算。

2.2.1 有限域乘法器电路结构分解

    通常，对于加法器和译码器等规模较小、结构较为简单的电路，可以直接通过逻辑“与”运算连接所有门电路完成电路实现的形式化建模。但是对于一个实现功能更为强大、规模更为庞大的电路实现，由于内部器件之间连线更为复杂，直接通过门电路合取进行建模容易由于人为的连接错误而导致模型错误，给验证增加工作量；同时直接通过门电路合取构建的电路实现模型无法体现模块间关系和电路结构特点，难以推导和证明实现电路蕴含目标性质。因此，为了验证前述目标，本文采用自顶向下地对电路实现进行层次化分析和模块化分解，依据实现的功能特性将整体电路划分为若干模块，然后将划分得到的模块进一步分解为若干的子模块，直到不可再分解的基本单元结构。依据该方法分解的电路结构框图如图2所示。

    总体上，有限域乘法器实现电路被分解为移位模块和计算模块两大功能模块。其中，移位模块由若干个结构相同的移位基本单元所组成，用以实现式(4)中从最低位开始串行输出乘数bi，移位基本单元又由D触发器和初始化模块所组成。计算模块可进一步分解为计算A(x)模块和计算C(x)模块，分别对应实现式(3)和式(4)的运算功能。同理，这两个子模块也可由若干结构相同的更小子模块所组成。

    研究发现，有效的电路模块分解有利于后续构建结构层次清晰的实现电路的形式化模型，这可使得验证思路更加简单明了，同时也缩小了验证的规模，降低验证难度。

2.2.2 有限域乘法器的电路时序分析

    由于上述的有限域乘法器为同步时序逻辑电路，其任意时刻的输出信号不仅与当前时刻的输入信号有关，还与电路在输入信号前的状态相关，所以相比于传统的组合逻辑电路验证，其验证难度更大。

    图1中电路实现的存储元件为D触发器，当直接依据触发器特性进行建模时，建模和验证的重心将偏向于时钟信号波形的变化和输入输出状态之间的关系，不利于对有限域乘法器功能的验证。另外，在对电路特性和功能特性进行分析后发现，该电路是由统一的时钟信号控制，只有时钟信号出现触发沿时，电路中各个变量的状态才会发生变化，而在两个相邻时钟信号的触发沿之间，电路状态是不会发生改变的，因而定义相邻触发沿的时间间隔为同步时序逻辑电路的一个运行周期，以周期作为时间抽象的最小粒度，可以有效地构建电路实现基于功能的形式化模型^[11]。因此，本文采用基于周期的方法完成对同步时序逻辑电路的形式化建模。

    D触发器基于周期所实现的功能为：在任意周期内，当置位信号set为T时，触发器进行置位操作，输出信号out为高电平T；当复位信号reset为T时，触发器进行复位操作，输出信号out为低电平F；否则输出信号out等于上一周期的输入信号值inp，则基于上述方法D触发器的形式化描述为：

2.2.3 有限域乘法器实现的形式化建模

    电路的形式化建模过程一般为电路结构模块分解的逆过程：在基本单元结构完成描述的基础上，开始自底向上地进行建模，在完成所有对应子模块验证后，再通过子模块的验证结果完成上一层次模块的建模和验证，并逐步地、层次化地完成有限域乘法器的形式化建模。为了更好地说明有限域乘法器实现的形式化建模过程，本节将以有限域乘法器中计算A(x)模块的建模和验证为例进行说明。

    计算模块是有限域乘法器中实现乘法运算的核心模块，依据电路功能结构划分，计算模块可以分解为计算A(x)模块和计算C(x)模块，分别对应实现最低位优先算法中式(3)和式(4)的运算操作。

    计算A(x)模块由4个结构相同的计算A(x)模块基本单元所组成，其基本单元实现按位对A(x)进行初始化置数、移位和取模运算操作。该基本单元模块进一步由与门、异或门、初始化模块、D触发器和多路选择模块组成，其中初始化模块和多路选择模块通过基本门电路组合实现。

    初始化模块的实现描述如下：

    初始化模块实现通过初始化信号init控制，依据输入值in生成相应的置位信号set和复位信号reset，其规范表述为：

    多路选择模块由基本门电路的组合实现，依据选择信号sw选择相应的输入作为输出的功能，实现的描述如下：

    在完成相应子模块建模和验证的基础上，通过子模块的组合完成计算A(x)模块基本单元实现的形式化建模，表述如下：

    计算A(x)模块基本单元所实现的功能为：在初始周期，对模块进行初始化操作，输出对应比特位的初始数值；其他任意周期，由模式信号mode控制选择输出有限域加法或者移位取模对应比特位的运算结果。

    通过初始化模块和多路选择模块的验证结果，完成对计算A(x)模块基本单元的正确性进行验证：

    又因为计算A(x)模块由4个基本单元组合，故通过基本单元实现模型逻辑表达式的合取完成计算A(x)模块的形式化建模，结果为：

    同理，使用相同的方法也可完成对移位模块和计算C(x)模块的形式化建模和验证，并验证计算C(x)模块实现电路蕴含有限域乘法规范中的性质2。最后得到的有限域乘法器实现的形式化描述如下：

其中，Shift_Right_4_IMP表示移位模块实现的形式化模型，GF_Product_A_4_IMP表示计算A(x)模块实现的形式化描述，而GF_Product_C_4_IMP为计算C(x)模块实现的形式化描述，Input_Module_4_IMP和Output_Module_4_IMP为辅助函数，定义数据的类型转换。

3 有限域乘法器的形式化验证

    通过对有限域乘法器算法和电路实现的分析，完成对有限域乘法器性质规范和电路实现的形式化建模。为了进一步证明有限域乘法器设计的正确性，仍需在HOL4系统中完成有限域乘法器电路实现蕴含有限域乘法器算法规范的验证，即：

    其在HOL4系统中的形式化描述如图3所示。图4为有限域乘法器在HOL4系统中的验证结果，初始目标得证，说明有限域乘法电路实现可以正确地实现有限域乘法运算并输出正确的运算结果。

4 结论

    本文使用定理证明方法对有限域乘法器进行形式化验证，并在形式化建模过程中提出了模块分解和分层的思想，依据功能结构特点对电路实现进行自顶向下的分解，并自低向高地完成结构建模和逐层验证。另外，依据电路的时序特点，提出了一种基于周期的形式化建模方法，有效映射了算法循环周期与电路时序周期的对应关系，该建模方法也可以应用到其他时序逻辑电路的建模和验证中。

参考文献

[1] LID`L R，NIEDERREITER H.Introduction to finite fields and their applications[M].New York：Cambridge University Press，2012.

[2] BIHAM E，CARMELI Y，SHAMIR A.Bug attacks[J].Journal of Cryptology，2016，29(4)：775-805.

[3] MORIOKA S，KATAYAMA Y，YAMANE T.Towards efficient verification of arithmetic algorithms over Galois fields GF(2m)[C].Proceedings of the 13th International Conference of Computer Aided Verification.Paris，France：Spring，2001：465-477.

[4] MUKHOPADHYAY D，SENGAR G，CHOWDHURY D R.Hierarchical verification of Galois field circuits[J].IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems，2007，26(10)：1893-1898.

[5] LV J，KALLA P，ENESCU F.Efficient Grobner basis reductions for formal verification of Galois field multipliers[C].Proceedings of the Conference on Design，Automation and Test in Europe.Dresden，Germany：2012：899-904.

[6] LV J，KALLA P，ENESCU F.Efficient Grobner basis reductions for formal verification of Galois field arithmetic circuits[J].IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems，2013，32(9)：1409-1420.

[7] OKAMOTO K，HOMMA N，AOKI T.A graph-based approach to designing parallel multipliers over Galois fields based on normal basis representations[C].Proceedings of the 43rd International Symposium on Multiple-Valued Logic，Toyama，Japan：2013：158-163.

[8] PAAR C，PELZL J.Understanding cryptography：a textbook for students and practitioners[M].Berlin：Springer Publishing Company，2010.

[9] SARGUNAM B，ARUL MOZHI S，DHANASEKARAN R.High speed bit-parallel systolic multiplier over GF(2m) for cryptographic application[C].2012 IEEE International Conference on Advanced Communication Control and Computing Technologies.Ramanathapuram，India：IEEE Press，2012：244-247.

[10] ANDRONIC C，CHIPER D F.A unified VLSI architecture for addition and multiplication in GF(2m)[C].Proceedings of 2015 International Symposium on Signals, Circuits and Systems.Iasi，Romania：IEEE Press，2015：1-4.

[11] 周宁.代数化符号模拟验证的应用研究[D].北京：北京交通大学，2015.