面向數(shù)據(jù)安全的形式化驗(yàn)證可滿(mǎn)足問(wèn)題研究.pdf

1、形式化驗(yàn)證是保證硬件系統(tǒng)設(shè)計(jì)正確性的一種有效的手段，它基于已建立的形式化規(guī)格，分析系統(tǒng)的相關(guān)特性，以評(píng)判系統(tǒng)是否滿(mǎn)足期望。命題可滿(mǎn)足問(wèn)題求解是其中重要的分析推理引擎。命題可滿(mǎn)足問(wèn)題(簡(jiǎn)稱(chēng)為可滿(mǎn)足問(wèn)題或SAT問(wèn)題)是指，對(duì)于一個(gè)表示為合取范式(CNF)的命題邏輯公式，是否存在對(duì)其所有變量的一個(gè)真值賦值使之成立。隨著硬件系統(tǒng)規(guī)模日益增大，形式化驗(yàn)證過(guò)程中產(chǎn)生的SAT問(wèn)題規(guī)模也急劇增長(zhǎng)。
　　開(kāi)放環(huán)境下的SAT求解服務(wù)，可利用云或網(wǎng)格等

2、提供的彈性計(jì)算資源，滿(mǎn)足不同規(guī)模問(wèn)題的求解需求，成為一種有效的應(yīng)對(duì)手段。但是，開(kāi)放計(jì)算環(huán)境在為用戶(hù)提供使用便利的同時(shí)，未授權(quán)訪問(wèn)等問(wèn)題對(duì)用戶(hù)的數(shù)據(jù)安全提出了嚴(yán)峻挑戰(zhàn)。為解決該問(wèn)題，本文針對(duì)硬件形式化驗(yàn)證中SAT問(wèn)題的特點(diǎn)，以提高方法的可用性和效能為出發(fā)點(diǎn)，系統(tǒng)地研究了在開(kāi)放計(jì)算環(huán)境下進(jìn)行SAT問(wèn)題求解時(shí)，數(shù)據(jù)隱私保護(hù)的若干關(guān)鍵問(wèn)題，并實(shí)現(xiàn)了SAT求解在對(duì)偶綜合設(shè)計(jì)中的應(yīng)用。
　　本文的主要研究?jī)?nèi)容和創(chuàng)新點(diǎn)如下。
　　1.開(kāi)放

3、計(jì)算環(huán)境下基于加噪混淆的SAT求解框架?，F(xiàn)有保護(hù)SAT問(wèn)題數(shù)據(jù)隱私的方法包括基于加密和基于數(shù)據(jù)分割兩類(lèi)。這些算法都依賴(lài)于全空間遍歷求解，在效率和實(shí)用性方面存在不足。本文通過(guò)對(duì)SAT問(wèn)題自身邏輯特點(diǎn)的分析，提出了基于加噪混淆算法的求解方法。該方法通過(guò)在原始CNF公式中無(wú)縫的混入噪音公式，在隱藏原有的結(jié)構(gòu)信息的同時(shí)，保持原有的CNF數(shù)據(jù)形式和解空間，從而復(fù)用已有的SAT求解算法。本文從理論上證明了該算法的正確性并通過(guò)仿真實(shí)驗(yàn)證明了該算法的高

4、效性。
　　2.結(jié)構(gòu)感知的混淆策略。識(shí)別混淆后CNF公式結(jié)構(gòu)的困難程度，是衡量混淆算法有效性的重要指標(biāo)。本文研究了硬件設(shè)計(jì)中CNF公式攜帶的結(jié)構(gòu)信息特征，提出結(jié)構(gòu)感知的加噪策略。該策略將原始公式的結(jié)構(gòu)映射至新的帶噪聲結(jié)構(gòu)，使得該新結(jié)構(gòu)與原始結(jié)構(gòu)不存在明確對(duì)應(yīng)，從而增大第三方恢復(fù)出原始結(jié)構(gòu)的難度。本文從理論上論證了結(jié)構(gòu)感知混淆算法的有效性，并通過(guò)大量的仿真實(shí)驗(yàn)分析驗(yàn)證了策略對(duì)性能的影響。
　　3.解空間投影等價(jià)的混淆算法。尋找

5、特定CNF公式的所有解的算法，稱(chēng)為可滿(mǎn)足問(wèn)題遍歷(ALL-Solution-SAT,簡(jiǎn)稱(chēng)為ALLSAT)算法。該算法構(gòu)成了對(duì)上述混淆算法的一個(gè)潛在威脅：通過(guò)求解出全空間的解，并將在所有解中具有相同唯一賦值的變量作為候選噪音變量，進(jìn)而從混淆后的公式中識(shí)別出原始公式。為了解決該問(wèn)題，本文研究了解空間投影等價(jià)的混淆算法，以打破噪音變量必然是相同單一賦值的斷言，以抵御上述基于ALLSAT的攻擊。
　　4.解空間加噪的混淆算法。在研究了上述

6、保護(hù)輸入數(shù)據(jù)結(jié)構(gòu)信息的算法后，本文進(jìn)一步研究了隱藏SAT問(wèn)題求解結(jié)果的方法。針對(duì)輸出信息隱藏，本文提出了解空間上估計(jì)的CNF混淆算法。通過(guò)在原始公式中混入具有多個(gè)解的噪音公式，使得混淆后公式的解空間為原始解空間的上估計(jì)，從而實(shí)現(xiàn)對(duì)原始解的隱藏。由于上估計(jì)的CNF混淆算法可能會(huì)多次調(diào)用SAT求解，其調(diào)用的概率取決于真實(shí)解與噪音解的比率。本文還討論了結(jié)合投影等價(jià)和上估計(jì)兩種混淆特性，來(lái)實(shí)現(xiàn)解空間可調(diào)制的混淆算法。
　　5.基于可滿(mǎn)足問(wèn)

7、題求解的流控機(jī)制迭代特征化算法。特征化流控?cái)?shù)據(jù)是自動(dòng)生成流控感知解碼器的關(guān)鍵，本文研究了基于可滿(mǎn)足問(wèn)題求解的迭代特征化方法。該算法在每一次迭代中，為每一個(gè)尚未被遍歷的解A，利用其對(duì)應(yīng)的余因子化簡(jiǎn)R以滿(mǎn)足產(chǎn)生Craig插值的要求。而該插值是A的一個(gè)充分?jǐn)U展。該迭代過(guò)程是停機(jī)的，且其性能比傳統(tǒng)的完全解遍歷算法有巨大的提升。
　　綜上所述，本文針對(duì)形式化驗(yàn)證中的SAT問(wèn)題，對(duì)其數(shù)據(jù)安全和應(yīng)用的若干關(guān)鍵問(wèn)題進(jìn)行了深入的研究，提出了具有實(shí)用