[發(fā)明專利]一種基于圖同構(gòu)的程序高階功耗側(cè)信道安全性的證明方法

在審

• 申請?zhí)枺?/td>: 202010913876.0
• 申請日: 2020-09-03
• 公開（公告）號: CN112364392A
• 公開（公告）日: 2021-02-12
• 發(fā)明（設(shè)計）人: 宋富;高鵬飛;謝弘毅
• 申請（專利權(quán)）人: 上?？萍即髮W(xué)
• 主分類號: G06F21/75
• 分類號: G06F21/75;G06F21/60
• 代理公司: 上海申匯專利代理有限公司 31001
• 代理人: 徐俊

本發(fā)明涉及一種基于圖同構(gòu)的程序高階功耗側(cè)信道安全性的證明方法。本發(fā)明提供的方法通過變量類型敏感的圖同構(gòu)判定兩個變量集合的聯(lián)合概率分布是否相同。在本發(fā)明提供的方法中：將變量的計算表達(dá)式轉(zhuǎn)化為抽象語法樹或有向無環(huán)圖等形式；在對表達(dá)式化簡時，為了保證不會影響驗證的結(jié)果，采用代數(shù)中的等價規(guī)則；對于表達(dá)式中的常量，通過子表達(dá)式替換的方法減少常量時，保證可觀察變量集合的聯(lián)合概率分布不變。通過多個實驗，本發(fā)明提出的方法可以有效減少模型計數(shù)求解的次數(shù)，從而提高了驗證效率。

技術(shù)領(lǐng)域

本發(fā)明涉及一種基于圖同構(gòu)的程序高階功耗側(cè)信道安全性的證明方法，可應(yīng)用于隨機(jī)掩碼高階功耗側(cè)信道安全的驗證。

背景技術(shù)

隨著信息技術(shù)的發(fā)展，密碼算法被廣泛應(yīng)用于保護(hù)隱私數(shù)據(jù)的傳輸和處理?，F(xiàn)代密碼學(xué)是建立在計算復(fù)雜性基礎(chǔ)之上的，因此通過暴力枚舉的攻擊很難破解密鑰。但是，Kocher、Quisquater和Mangard等人提出的側(cè)信道攻擊可以利用系統(tǒng)運行時的時間、功耗、電磁輻射等物理信息快速破解密鑰。

隨機(jī)掩碼是一種有效防御功耗側(cè)信道攻擊的策略，因此受到了國內(nèi)外科研院所和企業(yè)的研究和采用。隨機(jī)掩碼采用隨機(jī)數(shù)掩碼來避免物理信息與加密密鑰之間統(tǒng)計依賴關(guān)系。采用n階掩碼的程序理論上應(yīng)該能抵御n階功耗側(cè)信道攻擊。然而，正確實現(xiàn)n階掩碼的密碼算法是一項復(fù)雜又易錯的工作，因此需要自動化的驗證方法來證明程序高階功耗側(cè)信道安全性。

基于類型推導(dǎo)的證明方法和基于模型計數(shù)求解的證明方法相繼提出，用于證明高階功耗側(cè)信道安全性?；陬愋屯茖?dǎo)的證明方法高效，但是存在誤報導(dǎo)致假陽性；基于模型計數(shù)求解的證明方法理論上不存在誤報，但是由于計算代價高而無法高效地對完整程序進(jìn)行驗證。

發(fā)明內(nèi)容

本發(fā)明的目的是：減少模型計數(shù)求解的次數(shù)，有效提高驗證效率。

為了達(dá)到上述目的，本發(fā)明的技術(shù)方案是提供了一種基于圖同構(gòu)的程序高階功耗側(cè)信道安全性的證明方法，其特征在于，包括以下步驟：

步驟1、輸入程序及其變量類型，互不相交的集合T₁和T₂，其中：任何集合 T₁中的可觀察變量集合的聯(lián)合統(tǒng)計分布獨立于密鑰，任何集合T₂中的可觀察變量集合的聯(lián)合統(tǒng)計分布不獨立于密鑰；

步驟2、構(gòu)造輸入程序的中間表示形式，中間表示形式為抽象語法樹或有向無環(huán)圖；

對于任意一個含有d個可觀察變量的集合t，中間表示形式為t個抽象語法樹或有向無環(huán)圖；一個抽象語法樹或有向無環(huán)圖對應(yīng)一個計算表達(dá)式，抽象語法樹或有向無環(huán)圖的中間節(jié)點對應(yīng)計算表達(dá)式的運算符，葉子節(jié)點對應(yīng)計算表達(dá)式的輸入變量；

步驟3、對于任意一個含有d個可觀察變量的集合t，檢查對應(yīng)的t個抽象語法樹或有向無環(huán)圖中是否含有常量，如果有常量，則進(jìn)入步驟4對表達(dá)式進(jìn)行化簡和變換；如果沒有常量，則進(jìn)入步驟6進(jìn)行變量類型敏感的圖同構(gòu)檢查；

步驟4、對t個抽象語法樹或有向無環(huán)圖中的子表達(dá)式等價變換，使得每一個常量c的出現(xiàn)形式變?yōu)閤☉c，其中，x為變量，☉表示加、減、異或中的任意一個運算符，x在t個抽象語法樹或有向無環(huán)圖出現(xiàn)形式只能為x☉c，或x☉c₁且c₁表示與c不同的其他常量；

步驟5、對t個抽象語法樹或有向無環(huán)圖中所有形式為x☉c的子表達(dá)，迭代執(zhí)行以下步驟5.1及5.2減少常量：

步驟5.1、將所有子表達(dá)式x☉c替換為x；

步驟5.2、將所有子表達(dá)式x☉c₁替換為x☉c₂，其中如果☉是異或運算符，則表示異或運算符；如果☉是加或減運算符，則表示減運算符。