文獻(xiàn)標(biāo)識(shí)碼: A
DOI:10.16157/j.issn.0258-7998.171176
中文引用格式: 張杰,,王少超,,關(guān)永. 基于形式化方法的有限域乘法器的建模與驗(yàn)證[J].電子技術(shù)應(yīng)用,2018,,44(1):109-113.
英文引用格式: Zhang Jie,,Wang Shaochao,Guan Yong. Modeling and verification of finite field multiplier using formal method[J]. Application of Electronic Technique,,2018,,44(1):109-113.
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)算速度的需求,而已通過改用專門的硬件來滿足市場對(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)的信息安全帶來巨大威脅[2]。因此,,對(duì)有限域乘法器的設(shè)計(jì)進(jìn)行可靠性驗(yàn)證是十分必要的,。
眾所周知,常用的模擬和仿真驗(yàn)證方法雖易于實(shí)現(xiàn),,但驗(yàn)證過程中存在測試空間不完備的問題,難以排除所有的錯(cuò)誤,。而形式化方法則是使用形式語言分別對(duì)系統(tǒng)設(shè)計(jì)要求的功能和實(shí)現(xiàn)進(jìn)行形式化描述,,再通過基于相同形式語言的證明工具依據(jù)數(shù)學(xué)理論來驗(yàn)證系統(tǒng)的正確性,它能保證所驗(yàn)證性質(zhì)的完備性,。目前形式化方法主要有等價(jià)性驗(yàn)證,、模型檢驗(yàn)、定理證明和計(jì)算機(jī)代數(shù),。等價(jià)性驗(yàn)證和模型檢驗(yàn)方法由于存在狀態(tài)空間爆炸問題,,導(dǎo)致驗(yàn)證的系統(tǒng)規(guī)模有限[3-4];計(jì)算機(jī)代數(shù)方法主要應(yīng)用于數(shù)學(xué)證明,,缺乏精確的邏輯概念,,難以保障推導(dǎo)過程的可靠性[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ī)范的證明,,此法可有效地避免人為推演而造成的證明可靠性問題,更加有利于在驗(yàn)證過程中快速找出驗(yàn)證目標(biāo)細(xì)微的缺陷和不足,。
因此,,本文選用基于高階邏輯的定理證明器HOL4系統(tǒng)作為驗(yàn)證平臺(tái),通過層次化方法和基于周期的方法對(duì)有限域乘法器形式化建模,并采用定理證明方法完成其可靠性的驗(yàn)證工作,。
1 有限域及域運(yùn)算
1.1 有限域(finite field)
有限域是由一個(gè)有限元素的集合和兩個(gè)二元運(yùn)算所組成,,記為GF(p)[8]。有限域中的任意元素可以通過不同的基底來表示,,本文以應(yīng)用最廣,、研究最多的多項(xiàng)式基有限域乘法器設(shè)計(jì)作為研究對(duì)象。
常見的有限域算術(shù)運(yùn)算有加法,、乘法,、除法以及模逆運(yùn)算等,本文工作僅涉及到加法和乘法,,所以對(duì)其他有限域算術(shù)運(yùn)算不做詳細(xì)說明,。
1.2 有限域GF(2m)加法
有限域加法是通過標(biāo)準(zhǔn)的多項(xiàng)式加法運(yùn)算來實(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ù)長,,硬件實(shí)現(xiàn)資源消耗大,運(yùn)算效率低,。而基于最低位優(yōu)先(LSB-First)的有限域乘法算法從乘數(shù)B的最低位開始通過交叉執(zhí)行多項(xiàng)式乘法和多項(xiàng)式取模運(yùn)算,,可減少中間結(jié)果位長,縮短關(guān)鍵路徑,,有效地降低乘法運(yùn)算的空間復(fù)雜度和時(shí)間復(fù)雜度[9],。
所以,通過對(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),。通過功能分析,,可得到有限域乘法的兩個(gè)基本性質(zhì)。
性質(zhì)1:針對(duì)最低位優(yōu)先算法中的式(3),,當(dāng)周期i=0時(shí),,則對(duì)A(x)i進(jìn)行初始化置數(shù)操作,初始值為輸入的乘數(shù)InA,,否則,,A(x)i的取值等于上一迭代周期結(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)i進(jìn)行初始置數(shù)操作,初始值為0,;否則,,式(3)中上一迭代周期得到的A(x)i-1和乘數(shù)InB的對(duì)應(yīng)位bi的乘法運(yùn)算結(jié)果,最后再和上一周期部分積結(jié)果C(x)進(jìn)行累加得到當(dāng)前周期的部分積累加值C(x)i,,即:
由上文可知,,對(duì)于有限域GF(2m),在最低位優(yōu)先算法中需要通過m次循環(huán)操作才能獲得有限域乘法運(yùn)算的最終結(jié)果,,即C(x)=C(x)m,。所以基于最低位優(yōu)先的4位有限域乘法規(guī)范的形式化描述是上述2個(gè)基本性質(zhì)的合取,經(jīng)過4次迭代運(yùn)算得到最終結(jié)果,,即:
其中LSB_Shift_B_SPEC定義乘數(shù)InB從最低位開始的串行輸出值bi,,Input_Module_4為輔助函數(shù),定義數(shù)據(jù)的類型轉(zhuǎn)換,。有限域乘法運(yùn)算的最后結(jié)果即為outC=C(4)。
2.2 有限域乘法器實(shí)現(xiàn)的形式化建模
本文所研究的基于最低位優(yōu)先算法有限域乘法器的電路實(shí)現(xiàn)如圖1所示[10],,該系統(tǒng)通過比特串行的方式經(jīng)過4個(gè)時(shí)鐘周期可完成4位有限域乘法運(yùn)算,。
2.2.1 有限域乘法器電路結(jié)構(gòu)分解
通常,對(duì)于加法器和譯碼器等規(guī)模較小,、結(jié)構(gòu)較為簡單的電路,,可以直接通過邏輯“與”運(yùn)算連接所有門電路完成電路實(shí)現(xiàn)的形式化建模。但是對(duì)于一個(gè)實(shí)現(xiàn)功能更為強(qiáng)大,、規(guī)模更為龐大的電路實(shí)現(xiàn),,由于內(nèi)部器件之間連線更為復(fù)雜,直接通過門電路合取進(jìn)行建模容易由于人為的連接錯(cuò)誤而導(dǎo)致模型錯(cuò)誤,,給驗(yàn)證增加工作量,;同時(shí)直接通過門電路合取構(gòu)建的電路實(shí)現(xiàn)模型無法體現(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)中從最低位開始串行輸出乘數(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)證思路更加簡單明了,,同時(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)的形式化建模
電路的形式化建模過程一般為電路結(jié)構(gòu)模塊分解的逆過程:在基本單元結(jié)構(gòu)完成描述的基礎(chǔ)上,開始自底向上地進(jìn)行建模,,在完成所有對(duì)應(yīng)子模塊驗(yàn)證后,,再通過子模塊的驗(yàn)證結(jié)果完成上一層次模塊的建模和驗(yàn)證,并逐步地,、層次化地完成有限域乘法器的形式化建模,。為了更好地說明有限域乘法器實(shí)現(xiàn)的形式化建模過程,本節(jié)將以有限域乘法器中計(jì)算A(x)模塊的建模和驗(yàn)證為例進(jìn)行說明,。
計(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ā)器和多路選擇模塊組成,其中初始化模塊和多路選擇模塊通過基本門電路組合實(shí)現(xiàn),。
初始化模塊的實(shí)現(xiàn)描述如下:
初始化模塊實(shí)現(xiàn)通過初始化信號(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ǔ)上,,通過子模塊的組合完成計(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é)果。
通過初始化模塊和多路選擇模塊的驗(yàn)證結(jié)果,,完成對(duì)計(jì)算A(x)模塊基本單元的正確性進(jìn)行驗(yàn)證:
又因?yàn)橛?jì)算A(x)模塊由4個(gè)基本單元組合,,故通過基本單元實(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)證
通過對(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)得證,,說明有限域乘法電路實(shí)現(xiàn)可以正確地實(shí)現(xiàn)有限域乘法運(yùn)算并輸出正確的運(yùn)算結(jié)果,。
4 結(jié)論
本文使用定理證明方法對(duì)有限域乘法器進(jìn)行形式化驗(yàn)證,并在形式化建模過程中提出了模塊分解和分層的思想,,依據(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.