張 俊

1.中國(guó)科學(xué)院 上海微系統(tǒng)與信息技術(shù)研究所，上海200050

2.上?？萍即髮W(xué) 信息科學(xué)與技術(shù)學(xué)院，上海201210

3.中國(guó)科學(xué)院大學(xué)，北京100049

+通信作者E-mail:zhangjun@shanghaitech.edu.cn

現(xiàn)代社會(huì)生活中，密碼算法已經(jīng)廣泛應(yīng)用于嵌入式計(jì)算設(shè)備，以構(gòu)成其安全機(jī)制的支柱，嵌入式設(shè)備中硬件和軟件系統(tǒng)的安全性分析變得越來(lái)越重要。一般來(lái)說(shuō)，安全性是建立在攻擊者只能訪(fǎng)問(wèn)輸入輸出，但是不能訪(fǎng)問(wèn)到中間計(jì)算結(jié)果的基礎(chǔ)上。不幸的是，攻擊者可以通過(guò)分析側(cè)信道物理泄露信息，通過(guò)統(tǒng)計(jì)分析的方法來(lái)獲得相關(guān)中間計(jì)算結(jié)果，從而推算出加密密鑰。這些所謂的側(cè)信道攻擊利用密鑰和計(jì)算設(shè)備的非功能屬性，如執(zhí)行時(shí)間[1]、功耗[2]、電磁輻射[3]等的統(tǒng)計(jì)依賴(lài)性，其中，差分功耗分析（differential power analysis，DPA）是一種極受歡迎且有效的攻擊手段[4]。

到目前為止，已經(jīng)有很多對(duì)策可以阻止側(cè)信道攻擊。針對(duì)功耗側(cè)信道攻擊，掩碼技術(shù)仍然是使用最為廣泛的一種技術(shù)，可以通過(guò)隨機(jī)化的方式打破密鑰和側(cè)信道泄露信息之間的統(tǒng)計(jì)依賴(lài)性。例如，對(duì)于一個(gè)敏感的密鑰變量k，使用布爾掩蓋，利用一個(gè)隨機(jī)變量r和異或操作⊕可以獲得一個(gè)掩蓋變量km=k⊕r，并且通過(guò)異或操作的可逆性可以利用相同的隨機(jī)變量r恢復(fù)出密鑰變量km⊕r=k。其他的隨機(jī)化掩碼對(duì)策有加法掩蓋km=k+rmodn，乘法掩蓋km=k*rmodn。雖然已經(jīng)有了各種掩碼的實(shí)現(xiàn)方式，如用于AES（advanced encryption standard）或其非線(xiàn)性組件（S-box）[5-7]，但是檢查它們是否正確總是很困難且容易出錯(cuò)。因此，形式化驗(yàn)證這些掩碼對(duì)策的正確性是十分重要的。

在這之前，主要有兩種類(lèi)型的掩碼對(duì)策驗(yàn)證方法：一種是基于類(lèi)型推導(dǎo)[8-9]的；另一種是基于模型計(jì)數(shù)[10-11]的?；陬?lèi)型推導(dǎo)的方法快速而健全，它們可以快速證明計(jì)算是無(wú)側(cè)信道信息泄漏的。例如，當(dāng)需要驗(yàn)證的計(jì)算在句法上是獨(dú)立于密鑰的或已被從未使用的隨機(jī)變量掩蓋?？墒蔷浞?lèi)型推導(dǎo)并不完整，因?yàn)橛行┯?jì)算的句法類(lèi)型推導(dǎo)結(jié)果是分布類(lèi)型未知的。相比之下，基于模型計(jì)數(shù)的方法是完整的，它們檢查計(jì)算結(jié)果在統(tǒng)計(jì)上是否獨(dú)立于密鑰[5]。但是，由于模型計(jì)數(shù)的固有復(fù)雜性，它們?cè)趯?shí)踐中可能運(yùn)行起來(lái)非常慢。在準(zhǔn)確性和可擴(kuò)展性方面，上述差距在最近的方法中尚未得到解決。

過(guò)去幾年，很多掩碼策略[5,7,12-13]發(fā)表出來(lái)，盡管它們?cè)诠裟Ｐ汀⒀诖a模式、加密算法上有所不同，但是共同的問(wèn)題是缺少一個(gè)高效的工具可以形式化地驗(yàn)證這些策略的正確性[14]，本文的工作旨在解決這個(gè)問(wèn)題。盡管有一些驗(yàn)證工具也實(shí)現(xiàn)了相關(guān)功能[8,10-11,15-16]，但是它們要么是運(yùn)行速度快卻不準(zhǔn)確（例如以類(lèi)型推導(dǎo)技術(shù)為基礎(chǔ)的方法），要么是準(zhǔn)確但是運(yùn)行速度慢（例如以模型計(jì)數(shù)為基礎(chǔ)的方法）。例如，Bayrak等[8]提出了一種泄露檢測(cè)方法去判斷計(jì)算結(jié)果是否在邏輯上獨(dú)立于密鑰和隨機(jī)變量，運(yùn)行很快但不準(zhǔn)確，并且很多存在泄露的節(jié)點(diǎn)被錯(cuò)誤地證明了[10-11]。相比之下，Eldib 等[10-11]提出的基于模型計(jì)數(shù)的方法是準(zhǔn)確的，但此方法需要構(gòu)建的邏輯公式與隨機(jī)變量成指數(shù)關(guān)系，顯著地降低了可擴(kuò)展性。本文的語(yǔ)義類(lèi)型推導(dǎo)系統(tǒng)受到最近一些工作[15-16]的啟發(fā)，它們利用了一些可逆操作的獨(dú)特性質(zhì)，然而，這些現(xiàn)有技術(shù)與本文的方法有著顯著的不同點(diǎn)，因?yàn)樗鼈兊念?lèi)型推導(dǎo)規(guī)則是基于句法結(jié)構(gòu)的，而本文的類(lèi)型推導(dǎo)方法是基于語(yǔ)義的，并且可以通過(guò)SMT（satisfiability modulo theories）求解器去細(xì)化未知的推斷類(lèi)型。

為解決現(xiàn)有技術(shù)要么快但不準(zhǔn)確或準(zhǔn)確但是運(yùn)行慢的問(wèn)題，本文提出了一種新的驗(yàn)證掩碼對(duì)策的方法SCVerify。圖1 描繪了整個(gè)流程，其中輸入包括程序和標(biāo)記為明文、密文、隨機(jī)變量的集合。首先將程序轉(zhuǎn)換為中間表示：數(shù)據(jù)依賴(lài)圖（data dependency graph，DDG）。然后，按照拓?fù)渑判虮闅vDDG 并利用類(lèi)型推導(dǎo)方法以推斷每個(gè)中間計(jì)算結(jié)果的分布類(lèi)型；接下來(lái)，根據(jù)分布類(lèi)型檢查所有中間計(jì)算結(jié)果是否已經(jīng)被完美掩蓋，如果其中任意一個(gè)無(wú)法以這種方式解決，調(diào)用基于SMT 求解器的模型計(jì)數(shù)程序，該程序利用可滿(mǎn)足性（SAT）或模型計(jì)數(shù)（SAT#）求解來(lái)驗(yàn)證中間計(jì)算結(jié)果的分布類(lèi)型，再將計(jì)算結(jié)果反饋回類(lèi)型推導(dǎo)系統(tǒng)；最后，基于提煉的類(lèi)型推導(dǎo)規(guī)則，繼續(xù)分析其他中間計(jì)算結(jié)果。

Fig.1 Overview of SCVerify圖1 SCVerify 流程圖

SCVerify 可以被視為類(lèi)型推導(dǎo)方法和模型計(jì)數(shù)方法的集成。其中，類(lèi)型推導(dǎo)受到相關(guān)工作[15-16]的啟發(fā)，它們旨在推導(dǎo)中間計(jì)算結(jié)果的分布類(lèi)型。但是，有一個(gè)至關(guān)重要的區(qū)別：它們的推導(dǎo)規(guī)則是基于句法的且僅僅依賴(lài)于程序的結(jié)構(gòu)信息。本文的推導(dǎo)規(guī)則是基于語(yǔ)義的，并且借助于SMT 求解器可以逐步提高準(zhǔn)確性。從高層次說(shuō)，本文的語(yǔ)義類(lèi)型推導(dǎo)規(guī)則包含它們的句法類(lèi)型推導(dǎo)規(guī)則。因此，綜合類(lèi)型推導(dǎo)方法可以快速獲得驗(yàn)證結(jié)果的優(yōu)點(diǎn)以及利用SMT 求解器來(lái)解決未驗(yàn)證的計(jì)算結(jié)果，本文的方法既準(zhǔn)確又具備可擴(kuò)展性。

1 基礎(chǔ)知識(shí)

1.1 側(cè)信道攻擊

假設(shè)需要驗(yàn)證的程序?qū)崿F(xiàn)了一個(gè)加密函數(shù)c←enc(p,k)，其中p表示明文，k表示密鑰，c表示密文，enc是加密函數(shù)。其中p、k、c都是有限長(zhǎng)度的位向量，函數(shù)enc(p,k)的實(shí)現(xiàn)由以下計(jì)算序列組成：I1(p,k),I2(p,k),…,In(p,k)。It(p,k)是每一個(gè)中間計(jì)算結(jié)果，r是添加到加密函數(shù)enc(p,k)的實(shí)現(xiàn)中用來(lái)掩蓋密鑰k的一個(gè)隨機(jī)變量。在這里，r是一個(gè)均勻分布在域{0,1}s中的s位隨機(jī)數(shù)，使用隨機(jī)數(shù)r掩蓋密鑰k的目的是使所有中間計(jì)算結(jié)果在統(tǒng)計(jì)上與密鑰無(wú)關(guān)。當(dāng)加密函數(shù)enc(p,k)在布爾域中關(guān)于密鑰k是線(xiàn)性相關(guān)的，可以利用enc(p,k⊕r)=enc(p,k)⊕enc(p,r)的事實(shí)，首先使用隨機(jī)變量r與密鑰k進(jìn)行異或操作，然后解碼時(shí)利用enc(p,k⊕r)⊕enc(p,r)=enc(p,k)⊕enc(p,r)⊕enc(p,r)=enc(p,k)。在這種情況下，加密函數(shù)enc(p,k)無(wú)需做出改變。然而，當(dāng)加密函數(shù)enc(p,k)是非線(xiàn)性函數(shù)時(shí)，掩碼和解碼的工作就會(huì)變得更加復(fù)雜，因?yàn)樗鼈兘?jīng)常需要對(duì)加密函數(shù)enc(p,k)重新進(jìn)行一次設(shè)計(jì)，手動(dòng)設(shè)計(jì)這樣的掩碼對(duì)策工作量大且容易出錯(cuò)，因而需要一個(gè)高效的自動(dòng)化工具去評(píng)估掩碼對(duì)策到底有多安全。

針對(duì)每條運(yùn)算指令的功耗泄露模型建模，漢明權(quán)重（Hamming weight，HW）是最通用和基礎(chǔ)的模型，它被廣泛應(yīng)用于差分功耗分析。在這個(gè)模型中，嵌入式計(jì)算設(shè)備中執(zhí)行一條指令的功耗在統(tǒng)計(jì)上依賴(lài)于這條指令操作數(shù)的漢明權(quán)重，一個(gè)位向量的漢明權(quán)重就是邏輯設(shè)置為1 的位數(shù)。同時(shí)，當(dāng)知道程序中每個(gè)變量確切的寄存器地址的情況下，也可以插入更精確的功耗模型，如漢明距離（Hamming distance，HD）。漢明距離模型依賴(lài)于通過(guò)隨機(jī)變量改寫(xiě)寄存器中的當(dāng)前值和先前值中發(fā)生改變的位數(shù)數(shù)量。

在本文中，考慮的攻擊模型如下：假設(shè)攻擊者知道明文和密文的對(duì)應(yīng)關(guān)系(p,c)，其中c←enc(p,k)。對(duì)于每對(duì)明文密文關(guān)系對(duì)(p,c)，攻擊者通過(guò)觀察側(cè)信道泄露信息可以知道最多d個(gè)中間計(jì)算結(jié)果I1(p,k,r),I2(p,k,r),…,Id(p,k,r)的聯(lián)合概率分布。然而，攻擊者不會(huì)知道隨機(jī)變量r，因?yàn)閞是通過(guò)真實(shí)的隨機(jī)變量生成器生成的。攻擊者的目標(biāo)是計(jì)算密鑰k。

1.2 概率性布爾程序

按照文獻(xiàn)[5,10-11]中的相關(guān)定義，假設(shè)程序Pro實(shí)現(xiàn)加密函數(shù)enc，如Pro:c←enc(p,k)。在程序Pro中，隨機(jī)變量r在掩蓋密鑰k的同時(shí)需要保持程序Pro 輸入輸出的不變性。在程序Pro 中，因?yàn)檠h(huán)，函數(shù)調(diào)用和程序分支可以通過(guò)自動(dòng)重寫(xiě)去除[10-11]，整數(shù)變量可以轉(zhuǎn)換為位變量，出于驗(yàn)證考慮，假設(shè)Pro 是一個(gè)概率性布爾程序并且其中每條指令都有一個(gè)唯一的運(yùn)算符，最多有兩個(gè)操作數(shù)。

設(shè)K為密鑰集合，R為隨機(jī)變量集合，P為明文變量集合，C為存儲(chǔ)中間計(jì)算結(jié)果的集合，因此變量集是V=K?R?P?C。此外，該程序使用運(yùn)算符集合op包括取反（?）、取并（∧）、取或（∨）、取異或（⊕），即op={?,∧,∨,⊕}。程序Pro 由一組中間計(jì)算結(jié)果表示：c1←I1(p,k,r),c2←I2(p,k,r),ci←Ii(p,k,r),…,cn←In(p,k,r),1 ≤i≤n。其中，r是一個(gè)均勻分布在域{0,1}s中的s位隨機(jī)數(shù)；在程序Pro 中使用它們的唯一目的是確保c1,c2,…,cn在統(tǒng)計(jì)上是獨(dú)立于密鑰k分布的。

定義1（數(shù)據(jù)依賴(lài)圖（DDG））對(duì)于程序Pro，定義數(shù)據(jù)依賴(lài)圖為Gpro=(N,E,λ)，其中N是節(jié)點(diǎn)集，E是邊集，λ是標(biāo)記函數(shù)。

（1）N=L?Lv，L是程序Pro 中的指令集，Lv是程序中的葉子節(jié)點(diǎn)結(jié)合：lv∈Lv對(duì)應(yīng)一個(gè)變量或常量v∈P?K?R?{0,1}，即程序Pro 中任意一個(gè)節(jié)點(diǎn)都可以用輸入的明文、密文、隨機(jī)變量、常量和相關(guān)的運(yùn)算符表示。

（2）E=N×N，包含邊(l,l′)，當(dāng)l:c=x?y，x和y由l′定義；當(dāng)l:c=?x，x由l′定義。

（3）λ是l∈N到每對(duì)(val,op) 的匹配：當(dāng)l:c=x?y，λ(l)=(c,?) ；當(dāng)l:c=?x，λ(l)=(c,?) ；λ(l)=(c,⊥)對(duì)應(yīng)每個(gè)葉子節(jié)點(diǎn)lv。同時(shí)，定義λ1(l)=c，λ2(l)=?。

圖2 給出了一個(gè)掩碼策略示例，其中K={k1,k2},R={r1,r2},P=?,C={c1,c2,c3,c4}。圖2 的左邊是一個(gè)類(lèi)似C 語(yǔ)言的程序，只是其中⊕表示異或操作，∧表示取并操作，右邊是程序的數(shù)據(jù)依賴(lài)圖，圖中的各個(gè)節(jié)點(diǎn)表示如下：

Fig.2 Example of masking countermeasure圖2 掩碼策略示例

對(duì)于節(jié)點(diǎn)c1，按照數(shù)據(jù)依賴(lài)圖的定義，有λ(c1)=(c1,⊕),λ1(c1)=c1,λ2(c1)=⊕。同時(shí)，對(duì)于任意一個(gè)節(jié)點(diǎn)l∈N，也可以用l.lft表示節(jié)點(diǎn)l的左孩子節(jié)點(diǎn)，用l.rgt表示節(jié)點(diǎn)l的右孩子節(jié)點(diǎn)，則有c1.lft=k1，c1.rgt=r1。

1.3 完美掩蓋

給出加密函數(shù)enc(p,k)一對(duì)明文密鑰對(duì)(p,k)，一個(gè)隨機(jī)變量r，d個(gè)加密函數(shù)的中間計(jì)算結(jié)果I1(p,k,r),I2(p,k,r),…,Id(p,k,r)。假設(shè)r是一個(gè)s位隨機(jī)變量，均勻分布在域M={0,1}s中，則使用Dp,k(M)表示I1,I2,…,Id的聯(lián)合概率分布，只要Dp,k(M)與密鑰信息k之間存在統(tǒng)計(jì)相關(guān)性，就認(rèn)為加密程序Pro 是側(cè)信道攻擊不安全的。

定義2稱(chēng)中間計(jì)算結(jié)果的d-set{c1,c2,…,cd}是：

（1）均勻分布，如果Dp,k(c1,c2,…,cd) 對(duì)于任意p和k是均勻分布的[10]。

（2）獨(dú)立于密鑰分布，如果對(duì)任意(p,k)和(p,k′)，都有Dp,k(c1,c2,…,cd)=Dp,k′(c1,c2,…,cd)[10]。

這兩者之間有一個(gè)區(qū)別：均勻分布總是獨(dú)立于密鑰分布，但是獨(dú)立于密鑰分布不一定是均勻分布。

定義3程序Pro 是order-d完美掩蓋的當(dāng)且僅當(dāng)程序Pro 的每一個(gè)k-set(c1,c2,…,ck)(k≤d)都是獨(dú)立于密鑰分布的。當(dāng)程序Pro 是order-1 完美掩蓋的，簡(jiǎn)稱(chēng)程序Pro 是完美掩蓋的[10]。

2 基于語(yǔ)義的類(lèi)型推導(dǎo)系統(tǒng)

在這一章中，首先介紹類(lèi)型系統(tǒng)，該類(lèi)型系統(tǒng)受到之前工作[15-16]的啟發(fā)；然后定義用于類(lèi)型系統(tǒng)推導(dǎo)的相關(guān)數(shù)據(jù)結(jié)構(gòu)；最后介紹具體的類(lèi)型系統(tǒng)推導(dǎo)規(guī)則。

2.1 類(lèi)型定義

定義T={CST,RUD,SID,NPM,UKD}為中間計(jì)算結(jié)果的分布類(lèi)型集合，其中[c] 表示中間計(jì)算節(jié)點(diǎn)c←I(p,k,r)的分布類(lèi)型。

（1）[c]=CST 表示c是一個(gè)常量，不存在側(cè)信道信息泄露風(fēng)險(xiǎn)；

（2）[c]=RUD 表示c是均勻分布的，不存在側(cè)信道信息泄露風(fēng)險(xiǎn)；

（3）[c]=SID 表示c是獨(dú)立于密鑰分布的，不存在側(cè)信道信息泄露風(fēng)險(xiǎn)；

（4）[c]=NPM 表示c不是完美掩蓋的，存在側(cè)信道信息泄露風(fēng)險(xiǎn)；

（5）[c]=UKD 表示c的分布類(lèi)型是未知的，側(cè)信道信息泄露風(fēng)險(xiǎn)未知。

對(duì)于初始的葉子節(jié)點(diǎn)l∈LV其分布類(lèi)型定義如下：若λ1(l)∈{0,1}，則[l]=CST；若λ1(l)∈P?K，則[l]=UKD；若λ1(l)∈R，則[l]=RUD。

2.2 輔助數(shù)據(jù)結(jié)構(gòu)

在進(jìn)行類(lèi)型系統(tǒng)推導(dǎo)之前，需要定義相關(guān)的數(shù)據(jù)結(jié)構(gòu)，用以支持類(lèi)型系統(tǒng)的推導(dǎo)工作。相關(guān)定義如下：

定義4函數(shù)supp:N→K?R?P定義每個(gè)節(jié)點(diǎn)在數(shù)據(jù)結(jié)構(gòu)上的支持變量。若λ1(l)∈{0,1}，則supp(l)=?；若λ1(l)=x∈K?R?P，則supp(l)=x；否則supp(l)=supp(l.lft)?supp(l.rgt)。因此，函數(shù)supp返回λ1(l)在結(jié)構(gòu)上面依賴(lài)的變量集合。

定義5unq:N→R和dom:N→R是兩個(gè)函數(shù)，有以下兩點(diǎn)：

（1）對(duì)任意葉子節(jié)點(diǎn)l∈Lv，如果λ1(l)∈R，則unq(l)=dom(l)=λ1(l)，否則unq(l)=dom(l)=?。

（2）對(duì)任意中間節(jié)點(diǎn)l∈L，有unq(l)=(unq(l.lft)?unq(l.rgt))(supp(l.lft)?supp(l.rgt))；如果λ2(l)=⊕，那么dom(l)=(dom(l.lft)?dom(l.rgt))?unq(l)，其他情況下，dom(l)=?。

給出一個(gè)節(jié)點(diǎn)l，其對(duì)應(yīng)表達(dá)式e由集合V中的變量定義，e在語(yǔ)義上依賴(lài)于一個(gè)隨機(jī)變量r∈V，當(dāng)且僅當(dāng)存在兩種不同的變量賦值π1、π2，對(duì)任意x∈V{r}，當(dāng)π1(r)≠π2(r)，π1(x)=π2(x)，表達(dá)式e在π1、π2的賦值下取值結(jié)果不相同。

定義6函數(shù)semd:N→R定義一個(gè)節(jié)點(diǎn)l到在語(yǔ)義上有依賴(lài)關(guān)系的隨機(jī)變量的集合，這些隨機(jī)變量都是表達(dá)式為e的節(jié)點(diǎn)l在語(yǔ)義上依賴(lài)的。因此，有semd(l)?supp(l)，對(duì)任意r∈supp(l)semd(l)，λ1(l) 在語(yǔ)義上獨(dú)立于隨機(jī)變量r。

不像supp(l)，只是從程序中獲取節(jié)點(diǎn)的結(jié)構(gòu)信息，可以直接通過(guò)句法推導(dǎo)得出，semd(l)則需要計(jì)算得出。提供一個(gè)使用SMT 約束求解器的方法去計(jì)算出對(duì)任意中間計(jì)算結(jié)果c←I(p,k,r)，任意隨機(jī)變量r∈R，判斷c在語(yǔ)義上是否獨(dú)立于變量r。特別的，將此方法形式化定義為一個(gè)可滿(mǎn)足問(wèn)題（SAT），對(duì)應(yīng)公式Θs如下：

2.3 類(lèi)型推導(dǎo)規(guī)則

根據(jù)在文獻(xiàn)[15-16]中的證明，對(duì)于任意中間計(jì)算結(jié)果c←I(p,k,r)，很容易得到以下結(jié)論：

（1）如果dom(l)≠?，那么[c]=RUD；

（2）如果隨機(jī)變量r∈R,r?semd(l)，那么[r⊕c]=RUD；

（3）如果[c]=RUD，那么[?c]=RUD；

（4）如果[c]=SID，那么[?c]=SID；

（5）對(duì)任意c′←I′(p,k,r)，如果semd(l)?semd(l′)=?,[c]=[c′]=SID，那么[c?c′]=SID。

下面給出本文基于以上觀察的語(yǔ)義推導(dǎo)規(guī)則（這里沒(méi)有使用NPM）：

當(dāng)有多個(gè)規(guī)則可以應(yīng)用于節(jié)點(diǎn)l∈N時(shí)，首先選擇可以推導(dǎo)出[l]=RUD 的規(guī)則。如果沒(méi)有規(guī)則可以應(yīng)用在節(jié)點(diǎn)l，則[l]=UKD 。當(dāng)上下文定義都清楚時(shí)，可以用[l]和[c]互換表示λ1(l)=c的分布類(lèi)型。當(dāng)前還沒(méi)有使用NPM 在推導(dǎo)規(guī)則中，在第3 章中會(huì)基于SMT 的模型計(jì)數(shù)的方法去處理語(yǔ)法類(lèi)型推導(dǎo)結(jié)果為UKD 的節(jié)點(diǎn)，最后會(huì)明確其分布類(lèi)型為NPM 還是SID，并反饋回類(lèi)型推導(dǎo)系統(tǒng)中。本文的語(yǔ)義類(lèi)型推導(dǎo)規(guī)則包含基于句法的類(lèi)型推導(dǎo)規(guī)則，在驗(yàn)證工具SCVerify 中，實(shí)際上首先會(huì)直接調(diào)用句法類(lèi)型推導(dǎo)規(guī)則，這時(shí)只需要用supp函數(shù)替換語(yǔ)法推導(dǎo)規(guī)則中的semd函數(shù)即可，當(dāng)發(fā)現(xiàn)句法類(lèi)型推導(dǎo)結(jié)果為UKD時(shí)，需要先計(jì)算出semd，然后通過(guò)語(yǔ)法推導(dǎo)規(guī)則重新推導(dǎo)一遍。其實(shí)，本文的語(yǔ)法推導(dǎo)規(guī)則是對(duì)句法推導(dǎo)規(guī)則的補(bǔ)充，只有當(dāng)語(yǔ)法類(lèi)型推導(dǎo)結(jié)果同樣為UKD 的情況下，才會(huì)調(diào)用特別耗時(shí)的基于SMT 的模型計(jì)數(shù)方法。

Fig.3 Example of type inference圖3 類(lèi)型推導(dǎo)示例

圖3 給出了一個(gè)類(lèi)型推導(dǎo)示例，當(dāng)使用supp進(jìn)行句法類(lèi)型推導(dǎo)時(shí)，結(jié)果為[r1]=[r2]=[c1]=[c2]=[c3]=RUD，[k]=[c4]=[UKD]；當(dāng)使用semd進(jìn)行推導(dǎo)，結(jié)果為[r1]=[r2]=[c1]=[c2]=[c3]=[c4]=RUD，[k]=UKD 。其中節(jié)點(diǎn)c4在句法類(lèi)型推導(dǎo)的情況下分布類(lèi)型為UKD，經(jīng)過(guò)語(yǔ)法類(lèi)型推導(dǎo)分布類(lèi)型未RUD，語(yǔ)法類(lèi)型推導(dǎo)可以很好地補(bǔ)充句法類(lèi)型推導(dǎo)。

3 基于模型計(jì)數(shù)的細(xì)化方法

本章介紹利用基于SMT 求解器的技術(shù)逐步完善類(lèi)型推導(dǎo)系統(tǒng)，添加SMT 求解器后可以讓已有的類(lèi)型推導(dǎo)系統(tǒng)結(jié)果變得更加完整，可以證明一個(gè)待驗(yàn)證的程序?qū)崿F(xiàn)是否存在側(cè)信道信息泄露。

3.1 SMT 方法

對(duì)于一個(gè)中間計(jì)算結(jié)果c←I(p,k,r)，為了驗(yàn)證其是否滿(mǎn)足完美掩蓋（定義3），可以將其約減到一個(gè)可滿(mǎn)足的邏輯公式（Ψ），定義如下：

其中，r是一個(gè)均勻分布在域{0,1}s中的s位隨機(jī)數(shù)，表明公式I(p,k,r)的值為邏輯1 時(shí)隨機(jī)變量r的所有賦值情況的總和。當(dāng)隨機(jī)變量r中的每個(gè)比特在集合{0,1}上是均勻分布的時(shí)候，是公式I(p,k,r)為邏輯1 的概率。因此，公式Ψ是不滿(mǎn)足的當(dāng)且僅當(dāng)中間計(jì)算結(jié)果c是完美掩蓋的。

按照Eldib[10-11]等提出的方法，將Ψ編碼為一個(gè)可以被現(xiàn)有的SMT 求解器解決的無(wú)量詞的一階邏輯公式，如下：

（2）Θb2i：轉(zhuǎn)換布爾結(jié)果的輸出為整數(shù)輸出（為true 轉(zhuǎn)換為1，為false 轉(zhuǎn)換為0），使得賦值的數(shù)量可以被計(jì)數(shù)。

（3）Θ≠：對(duì)于兩個(gè)不同的k和k′，判斷求和結(jié)果是否相同。

例如在圖2 中的節(jié)點(diǎn)c3=r1⊕c2=r1⊕(k2⊕r2)，其中(r1,r2)∈{(0,0),(0,1),(1,0),(1,1)}，由此可以構(gòu)成求解節(jié)點(diǎn)c3是否被完美掩蓋的SMT 公式Ψ，其對(duì)應(yīng)的四部分分別如下：

通過(guò)添加斷言((n=1)∧c)∨((n=0)∧?c)將布爾變量轉(zhuǎn)換為整型值，該斷言可以確保當(dāng)布爾變量c的值為true 時(shí)，整型n=1；當(dāng)布爾變量c的值為false 時(shí)，整型n=0。

盡管SMT 公式的大小和程序Pro 的大小是線(xiàn)性相關(guān)的，但是不同副本的數(shù)量和在計(jì)算中使用的隨機(jī)比特?cái)?shù)成指數(shù)關(guān)系。因此，這個(gè)方法不能適用于大型程序。為了克服這個(gè)問(wèn)題，之前的工作[10-11]提出一種約減方法用來(lái)減小公式大小。其主要思路如下：一個(gè)中間計(jì)算結(jié)果c←I(p,k,r)，對(duì)應(yīng)DDG 中以節(jié)點(diǎn)l為根的子樹(shù)T，尋找一個(gè)在子樹(shù)T中的中間節(jié)點(diǎn)ls，滿(mǎn)足dom(ls)∩unq(l)≠?，這樣的一個(gè)節(jié)點(diǎn)稱(chēng)之為割點(diǎn)。一個(gè)割點(diǎn)是最大的當(dāng)且僅當(dāng)沒(méi)有其他可以從l到ls的割點(diǎn)。如果ls是一個(gè)割點(diǎn)，那么存在一個(gè)隨機(jī)變量r∈dom(ls)∩unq(l)；因?yàn)閞∈dom(ls)，dom(ls)≠?，則[λ1(ls)]=RUD；此外r∈unq(l)，表明當(dāng)在判斷節(jié)點(diǎn)l的分布類(lèi)型時(shí)λ1(ls)可以被看成是一個(gè)新的隨機(jī)變量。因此，可以用一個(gè)來(lái)自dom(ls)∩unq(l)中的隨機(jī)變量替換根節(jié)點(diǎn)為ls的在T中的子樹(shù)，這樣可以有效約減公式大小。

3.2 SMT 求解結(jié)果反饋回類(lèi)型推導(dǎo)系統(tǒng)

考慮以下場(chǎng)景：類(lèi)型推導(dǎo)系統(tǒng)推斷出節(jié)點(diǎn)l的分布類(lèi)型[l]=UKD，但是以SMT 求解器推斷出其類(lèi)型為NPM 或者SID。這些結(jié)果可以反饋回類(lèi)型推導(dǎo)系統(tǒng)中，產(chǎn)生以下兩點(diǎn)益處：（1）標(biāo)記更多的節(jié)點(diǎn)為完美掩蓋（RUD 或者SID）；（2）使得更多節(jié)點(diǎn)為NPM，這就意味著無(wú)需調(diào)用復(fù)雜的SMT 求解器去計(jì)算出這些節(jié)點(diǎn)的類(lèi)型。更多的是，如果SMT 求解器得出節(jié)點(diǎn)l是完美掩蓋的，那么[l]=SID，將其反饋代入類(lèi)型推導(dǎo)系統(tǒng)中可以幫助更方便地推導(dǎo)出依賴(lài)于節(jié)點(diǎn)l的其他節(jié)點(diǎn)類(lèi)型。

另一方面，如果SMT 求解器得出節(jié)點(diǎn)l不是完美掩蓋的，則[l]=NPM，并將其反饋回類(lèi)型推導(dǎo)系統(tǒng)，這樣可以推導(dǎo)出其他節(jié)點(diǎn)的類(lèi)型也是NPM。為了實(shí)現(xiàn)上述的情況，增加了與NPM 相關(guān)的類(lèi)型推導(dǎo)規(guī)則，如下所示。

帶有NPM 類(lèi)型的語(yǔ)義推導(dǎo)規(guī)則：

它們是對(duì)前文沒(méi)有使用NPM 類(lèi)型推導(dǎo)規(guī)則的補(bǔ)充，這樣可以使得更多的NPM類(lèi)型的節(jié)點(diǎn)通過(guò)類(lèi)型推導(dǎo)系統(tǒng)推斷出來(lái)，避免調(diào)用耗時(shí)的SMT求解器去計(jì)算。

4 實(shí)驗(yàn)

使用Z3[17]作為底層的SMT 求解器實(shí)現(xiàn)了文章中提出的細(xì)化的模型計(jì)數(shù)方法，并將其與語(yǔ)法類(lèi)型推導(dǎo)系統(tǒng)進(jìn)行整合，形成了一套命名為SCVerify 的驗(yàn)證工具。為了比較實(shí)驗(yàn)結(jié)果，在工具中也實(shí)現(xiàn)了句法類(lèi)型推導(dǎo)方法[16]和以SMT 為基礎(chǔ)的方法[10-11]。在公開(kāi)的可以獲得的加密軟件實(shí)現(xiàn)代碼上進(jìn)行實(shí)驗(yàn)，包括AES 和MAC-Keccak（message authentication code Keccak）中的代碼片段[10-11]。最終實(shí)驗(yàn)結(jié)果表明：

（1）SCVerify 比之前的句法類(lèi)型推導(dǎo)方法[16]更準(zhǔn)確，可以解決在句法類(lèi)型推導(dǎo)中分布類(lèi)型為UKD 的無(wú)法確定的中間節(jié)點(diǎn)。

（2）SCVerify 比以SMT 為基礎(chǔ)的模型計(jì)數(shù)方法在保持相同準(zhǔn)確率的情況下驗(yàn)證大規(guī)模的程序時(shí)運(yùn)行時(shí)間更短，相比于原先的運(yùn)行時(shí)間，可以縮減50%以上。例如，SCVerify 驗(yàn)證名為P12 的程序時(shí)只需花費(fèi)幾秒鐘，然而以SMT 為基礎(chǔ)的方法需要花費(fèi)超過(guò)1 h 的時(shí)間。

Table 1 Test case statistics表1 測(cè)試用例統(tǒng)計(jì)

4.1 測(cè)試用例

表1 展示了測(cè)試用例（P1～P17）的詳細(xì)情況，第一列是測(cè)試用例的名稱(chēng)，第二列是測(cè)試用例的簡(jiǎn)單描述，第三列表明程序中的運(yùn)算指令數(shù)量，第四列表明程序轉(zhuǎn)換為DDG 后中間計(jì)算節(jié)點(diǎn)個(gè)數(shù)，第五列到第七列分別表示程序中總共的密鑰變量數(shù)量、明文變量數(shù)量、隨機(jī)變量數(shù)量，所有的統(tǒng)計(jì)數(shù)據(jù)都是在將程序轉(zhuǎn)換為概率性布爾程序之后的統(tǒng)計(jì)結(jié)果。其中P1～P5 是從文獻(xiàn)[8]中得出的掩碼用例；P6～P7 來(lái)自于文獻(xiàn)[5]；P8～P9 是MAC-Keccak 重新計(jì)算的例子，來(lái)自于文獻(xiàn)[18]；P10～P11 的掩碼例子來(lái)自于MACKeccak 中的Chi 函數(shù)；P12～P17 是幾個(gè)較大的測(cè)試用例，是從提交到NIST 主辦的SHA-3 組委會(huì)的MACKeccak 的示例代碼演化過(guò)來(lái)的。其中P13～P16 用不同的掩碼方式實(shí)現(xiàn)了Chi 函數(shù)；P17 實(shí)現(xiàn)了Pi 函數(shù)的掩碼解碼過(guò)程。

4.2 實(shí)驗(yàn)結(jié)果

本文比較了SCVerify、句法類(lèi)型推導(dǎo)的方法（記為Syn）[16]、以SMT 為基礎(chǔ)的模型計(jì)數(shù)方法（記為SMT）[10-11]的表現(xiàn)性能。表2 是Syn 與SCVerify 的對(duì)比實(shí)驗(yàn)結(jié)果，第1 列表示測(cè)試用例的名稱(chēng)，第2 列是Syn 方法中分布類(lèi)型為UKD 的節(jié)點(diǎn)個(gè)數(shù)，第3 列和第4 列分別表示在Syn 方法中推斷節(jié)點(diǎn)的分布類(lèi)型為UKD 時(shí)，在SCVerify 中將這些分布類(lèi)型未知的節(jié)點(diǎn)明確為NPM 或SID 后，對(duì)應(yīng)類(lèi)型的節(jié)點(diǎn)數(shù)量。表2的實(shí)驗(yàn)結(jié)果說(shuō)明與句法類(lèi)型推導(dǎo)方法相比，本文的方法是更準(zhǔn)確的，可以消除在句法類(lèi)型推導(dǎo)中分布類(lèi)型為UKD 的節(jié)點(diǎn)，明確當(dāng)前測(cè)試用例是否為完美掩蓋。表3 是SMT 與SCVerify 的對(duì)比實(shí)驗(yàn)結(jié)果，第1列表示測(cè)試用例的名稱(chēng)，第2 列和第3 列分布表示以SMT 為基礎(chǔ)的模型計(jì)數(shù)方法和SCVerify 的實(shí)驗(yàn)時(shí)間，第4 列表示以SMT 為基礎(chǔ)的模型計(jì)數(shù)方法和SCVerify 判斷測(cè)試用例是否為完美掩蓋的測(cè)試結(jié)果是否保持一致。從表3 的實(shí)驗(yàn)結(jié)果中可以很明顯地發(fā)現(xiàn)，與SMT 為基礎(chǔ)的模型計(jì)數(shù)方法相比較，本文方法在保證相同準(zhǔn)確性的情況下，在大的測(cè)試用例中，可以縮短超過(guò)一半的時(shí)間。表4 展示了SCVerify 的具體結(jié)果集，第1 列表示測(cè)試用例的名稱(chēng)，第2 列給出測(cè)試用例是否為完美掩蓋的值，第3 列～第6 列分別給出了測(cè)試用例對(duì)應(yīng)的分布類(lèi)型為RUD、SID、CST、NPM 的節(jié)點(diǎn)數(shù)量。SCVerify 可以準(zhǔn)確地判斷出各個(gè)測(cè)試用例是否為完美掩蓋，并且給出具體的中間節(jié)點(diǎn)的分布類(lèi)型統(tǒng)計(jì)結(jié)果。

Table 2 Comparison between Syn and SCVerify表2 Syn 與SCVerify 對(duì)比

Table 3 Comparison between SMT and SCVerify表3 SMT 和SCVerify 對(duì)比

5 結(jié)論

本文提出了一種方法來(lái)證明一段加密軟件代碼的實(shí)現(xiàn)是否存在功耗側(cè)信道信息泄漏。該方法利用語(yǔ)義推導(dǎo)規(guī)則來(lái)推斷程序中每一個(gè)中間計(jì)算結(jié)果的分布類(lèi)型，當(dāng)發(fā)現(xiàn)語(yǔ)義推導(dǎo)規(guī)則不能明確某個(gè)中間結(jié)算結(jié)果的分布類(lèi)型時(shí)，結(jié)合基于SMT 求解器的模型計(jì)數(shù)方法來(lái)逐步完善這些類(lèi)型以提高準(zhǔn)確性。已經(jīng)實(shí)現(xiàn)了文中提出的方法并在相關(guān)密碼學(xué)測(cè)試用例上證明了它的有效性和正確性。實(shí)驗(yàn)結(jié)果表明本文方法在效率和準(zhǔn)確性方面優(yōu)于當(dāng)前最先進(jìn)的驗(yàn)證工具。

Table 4 SCVerify experimental results表4 SCVerify 實(shí)驗(yàn)結(jié)果