0 引言

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

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

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

1 有限域及域運(yùn)算

1.1 有限域(finite field)

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

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

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

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

1.3 有限域GF(2m)乘法

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2.2.2 有限域乘法器的電路時(shí)序分析

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3 有限域乘法器的形式化驗(yàn)證

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

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

4 結(jié)論

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

參考文獻(xiàn)

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