【摘要】：形式化驗證是保證硬件系統(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)格等提供的彈性計算資源,滿足不同規(guī)模問題的求解需求,成為一種有效的應(yīng)對手段。但是,開放計算環(huán)境在為用戶提供使用便利的同時,未授權(quán)訪問等問題對用戶的數(shù)據(jù)安全提出了嚴峻挑戰(zhàn)。為解決該問題,本文針對硬件形式化驗證中SAT問題的特點,以提高方法的可用性和效能為出發(fā)點,系統(tǒng)地研究了在開放計算環(huán)境下進行SAT問題求解時,數(shù)據(jù)隱私保護的若干關(guān)鍵問題,并實現(xiàn)了SAT求解在對偶綜合設(shè)計中的應(yīng)用。本文的主要研究內(nèi)容和創(chuàng)新點如下。1.開放計算環(huán)境下基于加噪混淆的SAT求解框架。現(xiàn)有保護SAT問題數(shù)據(jù)隱私的方法包括基于加密和基于數(shù)據(jù)分割兩類。這些算法都依賴于全空間遍歷求解,在效率和實用性方面存在不足。本文通過對SAT問題自身邏輯特點的分析,提出了基于加噪混淆算法的求解方法。該方法通過在原始CNF公式中無縫的混入噪音公式,在隱藏原有的結(jié)構(gòu)信息的同時,保持原有的CNF數(shù)據(jù)形式和解空間,從而復(fù)用已有的SAT求解算法。本文從理論上證明了該算法的正確性并通過仿真實驗證明了該算法的高效性。2.結(jié)構(gòu)感知的混淆策略。識別混淆后CNF公式結(jié)構(gòu)的困難程度,是衡量混淆算法有效性的重要指標。本文研究了硬件設(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.解空間投影等價的混淆算法。尋找特定CNF公式的所有解的算法,稱為可滿足問題遍歷(ALL-Solution-SAT,簡稱為ALLSAT)算法。該算法構(gòu)成了對上述混淆算法的一個潛在威脅:通過求解出全空間的解,并將在所有解中具有相同唯一賦值的變量作為候選噪音變量,進而從混淆后的公式中識別出原始公式。為了解決該問題,本文研究了解空間投影等價的混淆算法,以打破噪音變量必然是相同單一賦值的斷言,以抵御上述基于ALLSAT的攻擊。4.解空間加噪的混淆算法。在研究了上述保護輸入數(shù)據(jù)結(jié)構(gòu)信息的算法后,本文進一步研究了隱藏SAT問題求解結(jié)果的方法。針對輸出信息隱藏,本文提出了解空間上估計的CNF混淆算法。通過在原始公式中混入具有多個解的噪音公式,使得混淆后公式的解空間為原始解空間的上估計,從而實現(xiàn)對原始解的隱藏。由于上估計的CNF混淆算法可能會多次調(diào)用SAT求解,其調(diào)用的概率取決于真實解與噪音解的比率。本文還討論了結(jié)合投影等價和上估計兩種混淆特性,來實現(xiàn)解空間可調(diào)制的混淆算法。5.基于可滿足問題求解的流控機制迭代特征化算法。特征化流控數(shù)據(jù)是自動生成流控感知解碼器的關(guān)鍵,本文研究了基于可滿足問題求解的迭代特征化方法。該算法在每一次迭代中,為每一個尚未被遍歷的解A,利用其對應(yīng)的余因子化簡R以滿足產(chǎn)生Craig插值的要求。而該插值是A的一個充分擴展。該迭代過程是停機的,且其性能比傳統(tǒng)的完全解遍歷算法有巨大的提升。綜上所述,本文針對形式化驗證中的SAT問題,對其數(shù)據(jù)安全和應(yīng)用的若干關(guān)鍵問題進行了深入的研究,提出了具有實用性、低開銷的解決方案,并通過理論分析和大量的仿真實驗驗證了所提出算法的有效性和性能,對于促進SAT計算外包服務(wù)的實用化有一定的理論意義和應(yīng)用價值。
[Abstract]:......
【學(xué)位授予單位】：國防科學(xué)技術(shù)大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2016
【分類號】：TP309

【相似文獻】

相關(guān)期刊論文 前10條

1 谷文祥;朱磊;黃平;殷明浩;;可滿足問題中的模型計數(shù)[J];智能系統(tǒng)學(xué)報;2012年01期

2 伍麗華;陳藹洋;姜云飛;;規(guī)劃問題編碼為約束可滿足問題的研究[J];計算機科學(xué);2006年08期

3 陳榮,孫吉貴,劉瑞勝;約束可滿足問題求解策略的改進和實驗結(jié)果[J];吉林大學(xué)自然科學(xué)學(xué)報;1997年02期

4 殷志祥;崔建中;支凌迎;孫俠;黃曉慧;;可滿足問題的分子信標計算模型(英文)[J];計算機學(xué)報;2008年12期

5 宋建民;弓小影;;一種求解MAX-k-SAT問題的新方法[J];河南科技學(xué)院學(xué)報(自然科學(xué)版);2014年02期

6 楊煜俊,劉清華,萬立,王啟富,陳立平;基于條件約束滿足問題的產(chǎn)品配置研究[J];計算機集成制造系統(tǒng);2004年11期

7 邵明,李光輝,李曉維;求解可滿足問題的調(diào)查傳播算法以及步長的影響規(guī)律[J];計算機學(xué)報;2005年05期

8 陳振宇;徐寶文;周從華;;一種基于消解的變量極小不可滿足子公式的提取方法[J];計算機研究與發(fā)展;2008年S1期

9 趙春艷;鄭志明;;一種基于變量熵求解約束滿足問題的置信傳播算法[J];中國科學(xué):信息科學(xué);2012年09期

10 余根堅;錢小聰;;小世界網(wǎng)絡(luò)拓撲下的多Agent網(wǎng)絡(luò)傳輸有效性和限定性滿足問題研究[J];計算機應(yīng)用研究;2007年02期

相關(guān)會議論文 前1條

1 邵明;李光輝;李曉維;;提取不可滿足問題核[A];第十屆全國容錯計算學(xué)術(shù)會議論文集[C];2003年

相關(guān)博士學(xué)位論文 前2條

1 秦瑩;面向數(shù)據(jù)安全的形式化驗證可滿足問題研究[D];國防科學(xué)技術(shù)大學(xué);2016年

2 邵明;模型檢驗及其布爾可滿足問題的研究[D];中國科學(xué)院研究生院（計算技術(shù)研究所）;2005年

相關(guān)碩士學(xué)位論文 前7條

1 任明康;求解約束滿足問題的自適應(yīng)蟻群算法研究[D];東北大學(xué);2014年

2 周曦?zé)?基于約束性可滿足問題的解決器[D];復(fù)旦大學(xué);2009年

3 張馳豪;一類約束可滿足問題的固定參數(shù)算法[D];上海交通大學(xué);2012年

4 陳建榮;一類隨機限制滿足問題的相變現(xiàn)象及相關(guān)運算復(fù)雜性研究[D];首都師范大學(xué);2009年

5 朱磊;一種新的求解#CSP上界的方法[D];東北師范大學(xué);2012年

6 盧道設(shè);可滿足模理論解決器[D];廣西民族大學(xué);2013年

7 胡曉艷;基于蘊含推理的SAT預(yù)處理器的實現(xiàn)[D];復(fù)旦大學(xué);2009年

，

本文編號：2323531