面向數(shù)據(jù)安全的形式化驗證可滿足問題研究.pdf

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

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

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

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

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

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

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