0 引言

    有限域運算在代數(shù)編碼、數(shù)據(jù)加密和數(shù)字信息處理等領(lǐng)域有著廣泛的應(yīng)用，其運算速度是加密算法運算速度的基礎(chǔ)^[1]；如今僅依靠軟件實現(xiàn)有限域乘法運算已經(jīng)難以滿足人們對加密解密算法運算速度的需求，而已通過改用專門的硬件來滿足市場對有限域乘法運算速率的要求。但是，有限域乘法的硬件實現(xiàn)結(jié)構(gòu)復(fù)雜，容易出現(xiàn)潛在的設(shè)計缺陷而導(dǎo)致運算錯誤，甚至?xí)?dǎo)致加密系統(tǒng)密鑰泄漏，從而給系統(tǒng)的信息安全帶來巨大威脅^[2]。因此，對有限域乘法器的設(shè)計進行可靠性驗證是十分必要的。

    眾所周知，常用的模擬和仿真驗證方法雖易于實現(xiàn)，但驗證過程中存在測試空間不完備的問題，難以排除所有的錯誤。而形式化方法則是使用形式語言分別對系統(tǒng)設(shè)計要求的功能和實現(xiàn)進行形式化描述，再通過基于相同形式語言的證明工具依據(jù)數(shù)學(xué)理論來驗證系統(tǒng)的正確性，它能保證所驗證性質(zhì)的完備性。目前形式化方法主要有等價性驗證、模型檢驗、定理證明和計算機代數(shù)。等價性驗證和模型檢驗方法由于存在狀態(tài)空間爆炸問題，導(dǎo)致驗證的系統(tǒng)規(guī)模有限^[3-4]；計算機代數(shù)方法主要應(yīng)用于數(shù)學(xué)證明，缺乏精確的邏輯概念，難以保障推導(dǎo)過程的可靠性^[5-7]；定理證明方法則需要對待驗證的系統(tǒng)實現(xiàn)和系統(tǒng)規(guī)范進行形式化建模，并在定理證明器中完成系統(tǒng)實現(xiàn)蘊含系統(tǒng)規(guī)范的證明，此法可有效地避免人為推演而造成的證明可靠性問題，更加有利于在驗證過程中快速找出驗證目標(biāo)細(xì)微的缺陷和不足。

    因此，本文選用基于高階邏輯的定理證明器HOL4系統(tǒng)作為驗證平臺，通過層次化方法和基于周期的方法對有限域乘法器形式化建模，并采用定理證明方法完成其可靠性的驗證工作。

1 有限域及域運算

1.1 有限域(finite field)

    有限域是由一個有限元素的集合和兩個二元運算所組成，記為GF(p)^[8]。有限域中的任意元素可以通過不同的基底來表示，本文以應(yīng)用最廣、研究最多的多項式基有限域乘法器設(shè)計作為研究對象。

    常見的有限域算術(shù)運算有加法、乘法、除法以及模逆運算等，本文工作僅涉及到加法和乘法，所以對其他有限域算術(shù)運算不做詳細(xì)說明。

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

    有限域加法是通過標(biāo)準(zhǔn)的多項式加法運算來實現(xiàn)的，表達(dá)式如下：

1.3 有限域GF(2m)乘法

    有限域乘法運算是加密算法和代數(shù)編碼的核心運算，基于多項式基的有限域乘法運算的通用表達(dá)式為：

    由式(2)可知，基于多項式基有限域乘法運算分為兩個運行步驟：多項式乘法和多項式取模。傳統(tǒng)的有限域乘法依序執(zhí)行多項式乘法和多項式取模運算，中間結(jié)果位數(shù)長，硬件實現(xiàn)資源消耗大，運算效率低。而基于最低位優(yōu)先(LSB-First)的有限域乘法算法從乘數(shù)B的最低位開始通過交叉執(zhí)行多項式乘法和多項式取模運算，可減少中間結(jié)果位長，縮短關(guān)鍵路徑，有效地降低乘法運算的空間復(fù)雜度和時間復(fù)雜度^[9]。

    所以，通過對式(2)進行一系列的變化可以得到基于最低位優(yōu)先的有限域乘法的表達(dá)式，如式(3)、式(4)所示。

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

    如前所述，基于定理證明方法對有限域乘法器進行形式化驗證，首先需要完成有限域乘法器的形式化模型，建模工作主要分為兩個部分：(1)依據(jù)算法特性抽取驗證的關(guān)鍵性質(zhì)，即系統(tǒng)的規(guī)范，并基于高階邏輯完成相關(guān)性質(zhì)的描述；(2)分析目標(biāo)系統(tǒng)的實現(xiàn)電路，構(gòu)建描述系統(tǒng)實現(xiàn)的高階邏輯表達(dá)式，即完成系統(tǒng)實現(xiàn)的形式化建模。

2.1 有限域乘法器規(guī)范的形式化建模

    規(guī)范是敘述系統(tǒng)所需要具備的功能和性質(zhì)。依據(jù)上述最低位優(yōu)先算法，有限域乘法器的功能可描述為：乘法器對輸入的乘數(shù)InA、InB以及首一不可約多項式P(x)進行相應(yīng)的多項式乘法和多項式取模運算，得到有限域乘法運算的最終結(jié)果C(x)。通過功能分析，可得到有限域乘法的兩個基本性質(zhì)。

    性質(zhì)1：針對最低位優(yōu)先算法中的式(3)，當(dāng)周期i=0時，則對A(x)ⁱ進行初始化置數(shù)操作，初始值為輸入的乘數(shù)InA，否則，A(x)ⁱ的取值等于上一迭代周期結(jié)果A(x)^i-1左移一位后再對P(x)進行多項式取模，表述如下：

    性質(zhì)2：針對最低位優(yōu)先算法中的式(4)，當(dāng)周期i=0時，則對部分積累加結(jié)果C(x)ⁱ進行初始置數(shù)操作，初始值為0；否則，式(3)中上一迭代周期得到的A(x)^i-1和乘數(shù)InB的對應(yīng)位b_i的乘法運算結(jié)果，最后再和上一周期部分積結(jié)果C(x)進行累加得到當(dāng)前周期的部分積累加值C(x)ⁱ，即：

    由上文可知，對于有限域GF(2^m)，在最低位優(yōu)先算法中需要通過m次循環(huán)操作才能獲得有限域乘法運算的最終結(jié)果，即C(x)=C(x)^m。所以基于最低位優(yōu)先的4位有限域乘法規(guī)范的形式化描述是上述2個基本性質(zhì)的合取，經(jīng)過4次迭代運算得到最終結(jié)果，即：

其中LSB_Shift_B_SPEC定義乘數(shù)InB從最低位開始的串行輸出值b_i，Input_Module_4為輔助函數(shù)，定義數(shù)據(jù)的類型轉(zhuǎn)換。有限域乘法運算的最后結(jié)果即為outC=C⁽⁴⁾。

2.2 有限域乘法器實現(xiàn)的形式化建模

    本文所研究的基于最低位優(yōu)先算法有限域乘法器的電路實現(xiàn)如圖1所示^[10]，該系統(tǒng)通過比特串行的方式經(jīng)過4個時鐘周期可完成4位有限域乘法運算。

2.2.1 有限域乘法器電路結(jié)構(gòu)分解

    通常，對于加法器和譯碼器等規(guī)模較小、結(jié)構(gòu)較為簡單的電路，可以直接通過邏輯“與”運算連接所有門電路完成電路實現(xiàn)的形式化建模。但是對于一個實現(xiàn)功能更為強大、規(guī)模更為龐大的電路實現(xiàn)，由于內(nèi)部器件之間連線更為復(fù)雜，直接通過門電路合取進行建模容易由于人為的連接錯誤而導(dǎo)致模型錯誤，給驗證增加工作量；同時直接通過門電路合取構(gòu)建的電路實現(xiàn)模型無法體現(xiàn)模塊間關(guān)系和電路結(jié)構(gòu)特點，難以推導(dǎo)和證明實現(xiàn)電路蘊含目標(biāo)性質(zhì)。因此，為了驗證前述目標(biāo)，本文采用自頂向下地對電路實現(xiàn)進行層次化分析和模塊化分解，依據(jù)實現(xiàn)的功能特性將整體電路劃分為若干模塊，然后將劃分得到的模塊進一步分解為若干的子模塊，直到不可再分解的基本單元結(jié)構(gòu)。依據(jù)該方法分解的電路結(jié)構(gòu)框圖如圖2所示。

    總體上，有限域乘法器實現(xiàn)電路被分解為移位模塊和計算模塊兩大功能模塊。其中，移位模塊由若干個結(jié)構(gòu)相同的移位基本單元所組成，用以實現(xiàn)式(4)中從最低位開始串行輸出乘數(shù)bi，移位基本單元又由D觸發(fā)器和初始化模塊所組成。計算模塊可進一步分解為計算A(x)模塊和計算C(x)模塊，分別對應(yīng)實現(xiàn)式(3)和式(4)的運算功能。同理，這兩個子模塊也可由若干結(jié)構(gòu)相同的更小子模塊所組成。

    研究發(fā)現(xiàn)，有效的電路模塊分解有利于后續(xù)構(gòu)建結(jié)構(gòu)層次清晰的實現(xiàn)電路的形式化模型，這可使得驗證思路更加簡單明了，同時也縮小了驗證的規(guī)模，降低驗證難度。

2.2.2 有限域乘法器的電路時序分析

    由于上述的有限域乘法器為同步時序邏輯電路，其任意時刻的輸出信號不僅與當(dāng)前時刻的輸入信號有關(guān)，還與電路在輸入信號前的狀態(tài)相關(guān)，所以相比于傳統(tǒng)的組合邏輯電路驗證，其驗證難度更大。

    圖1中電路實現(xiàn)的存儲元件為D觸發(fā)器，當(dāng)直接依據(jù)觸發(fā)器特性進行建模時，建模和驗證的重心將偏向于時鐘信號波形的變化和輸入輸出狀態(tài)之間的關(guān)系，不利于對有限域乘法器功能的驗證。另外，在對電路特性和功能特性進行分析后發(fā)現(xiàn)，該電路是由統(tǒng)一的時鐘信號控制，只有時鐘信號出現(xiàn)觸發(fā)沿時，電路中各個變量的狀態(tài)才會發(fā)生變化，而在兩個相鄰時鐘信號的觸發(fā)沿之間，電路狀態(tài)是不會發(fā)生改變的，因而定義相鄰觸發(fā)沿的時間間隔為同步時序邏輯電路的一個運行周期，以周期作為時間抽象的最小粒度，可以有效地構(gòu)建電路實現(xiàn)基于功能的形式化模型^[11]。因此，本文采用基于周期的方法完成對同步時序邏輯電路的形式化建模。

    D觸發(fā)器基于周期所實現(xiàn)的功能為：在任意周期內(nèi)，當(dāng)置位信號set為T時，觸發(fā)器進行置位操作，輸出信號out為高電平T；當(dāng)復(fù)位信號reset為T時，觸發(fā)器進行復(fù)位操作，輸出信號out為低電平F；否則輸出信號out等于上一周期的輸入信號值inp，則基于上述方法D觸發(fā)器的形式化描述為：

2.2.3 有限域乘法器實現(xiàn)的形式化建模

    電路的形式化建模過程一般為電路結(jié)構(gòu)模塊分解的逆過程：在基本單元結(jié)構(gòu)完成描述的基礎(chǔ)上，開始自底向上地進行建模，在完成所有對應(yīng)子模塊驗證后，再通過子模塊的驗證結(jié)果完成上一層次模塊的建模和驗證，并逐步地、層次化地完成有限域乘法器的形式化建模。為了更好地說明有限域乘法器實現(xiàn)的形式化建模過程，本節(jié)將以有限域乘法器中計算A(x)模塊的建模和驗證為例進行說明。

    計算模塊是有限域乘法器中實現(xiàn)乘法運算的核心模塊，依據(jù)電路功能結(jié)構(gòu)劃分，計算模塊可以分解為計算A(x)模塊和計算C(x)模塊，分別對應(yīng)實現(xiàn)最低位優(yōu)先算法中式(3)和式(4)的運算操作。

    計算A(x)模塊由4個結(jié)構(gòu)相同的計算A(x)模塊基本單元所組成，其基本單元實現(xiàn)按位對A(x)進行初始化置數(shù)、移位和取模運算操作。該基本單元模塊進一步由與門、異或門、初始化模塊、D觸發(fā)器和多路選擇模塊組成，其中初始化模塊和多路選擇模塊通過基本門電路組合實現(xiàn)。

    初始化模塊的實現(xiàn)描述如下：

    初始化模塊實現(xiàn)通過初始化信號init控制，依據(jù)輸入值in生成相應(yīng)的置位信號set和復(fù)位信號reset，其規(guī)范表述為：

    多路選擇模塊由基本門電路的組合實現(xiàn)，依據(jù)選擇信號sw選擇相應(yīng)的輸入作為輸出的功能，實現(xiàn)的描述如下：

    在完成相應(yīng)子模塊建模和驗證的基礎(chǔ)上，通過子模塊的組合完成計算A(x)模塊基本單元實現(xiàn)的形式化建模，表述如下：

    計算A(x)模塊基本單元所實現(xiàn)的功能為：在初始周期，對模塊進行初始化操作，輸出對應(yīng)比特位的初始數(shù)值；其他任意周期，由模式信號mode控制選擇輸出有限域加法或者移位取模對應(yīng)比特位的運算結(jié)果。

    通過初始化模塊和多路選擇模塊的驗證結(jié)果，完成對計算A(x)模塊基本單元的正確性進行驗證：

    又因為計算A(x)模塊由4個基本單元組合，故通過基本單元實現(xiàn)模型邏輯表達(dá)式的合取完成計算A(x)模塊的形式化建模，結(jié)果為：

    同理，使用相同的方法也可完成對移位模塊和計算C(x)模塊的形式化建模和驗證，并驗證計算C(x)模塊實現(xiàn)電路蘊含有限域乘法規(guī)范中的性質(zhì)2。最后得到的有限域乘法器實現(xiàn)的形式化描述如下：

其中，Shift_Right_4_IMP表示移位模塊實現(xiàn)的形式化模型，GF_Product_A_4_IMP表示計算A(x)模塊實現(xiàn)的形式化描述，而GF_Product_C_4_IMP為計算C(x)模塊實現(xiàn)的形式化描述，Input_Module_4_IMP和Output_Module_4_IMP為輔助函數(shù)，定義數(shù)據(jù)的類型轉(zhuǎn)換。

3 有限域乘法器的形式化驗證

    通過對有限域乘法器算法和電路實現(xiàn)的分析，完成對有限域乘法器性質(zhì)規(guī)范和電路實現(xiàn)的形式化建模。為了進一步證明有限域乘法器設(shè)計的正確性，仍需在HOL4系統(tǒng)中完成有限域乘法器電路實現(xiàn)蘊含有限域乘法器算法規(guī)范的驗證，即：

    其在HOL4系統(tǒng)中的形式化描述如圖3所示。圖4為有限域乘法器在HOL4系統(tǒng)中的驗證結(jié)果，初始目標(biāo)得證，說明有限域乘法電路實現(xiàn)可以正確地實現(xiàn)有限域乘法運算并輸出正確的運算結(jié)果。

4 結(jié)論

    本文使用定理證明方法對有限域乘法器進行形式化驗證，并在形式化建模過程中提出了模塊分解和分層的思想，依據(jù)功能結(jié)構(gòu)特點對電路實現(xiàn)進行自頂向下的分解，并自低向高地完成結(jié)構(gòu)建模和逐層驗證。另外，依據(jù)電路的時序特點，提出了一種基于周期的形式化建模方法，有效映射了算法循環(huán)周期與電路時序周期的對應(yīng)關(guān)系，該建模方法也可以應(yīng)用到其他時序邏輯電路的建模和驗證中。

參考文獻

[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，F(xiàn)rance：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] 周寧.代數(shù)化符號模擬驗證的應(yīng)用研究[D].北京：北京交通大學(xué)，2015.