一種符號執(zhí)行制導(dǎo)的循環(huán)內(nèi)界分析方法
本文選題:循環(huán)邊界分析 切入點:符號執(zhí)行 出處:《電子學(xué)報》2017年11期 論文類型:期刊論文
【摘要】:循環(huán)是計算機中重要的復(fù)雜程序結(jié)構(gòu).很多應(yīng)用場景要求靜態(tài)分析循環(huán)可能達到的最大迭代次數(shù),即循環(huán)邊界(Loop Bound).對應(yīng)技術(shù)在文獻中被稱為循環(huán)邊界分析(Loop Bound Analysis).現(xiàn)有的循環(huán)邊界分析均使用保守方式進行外界分析,即產(chǎn)生略高于循環(huán)邊界的近似值.基于這一現(xiàn)狀,本文提出了一種自動地循環(huán)內(nèi)界分析方法,產(chǎn)生略低于循環(huán)邊界的近似值.當(dāng)用戶綜合利用外界與內(nèi)界分析,能將循環(huán)邊界值約束到一個統(tǒng)計區(qū)間,從而能對分析結(jié)果獲得更為完整的認(rèn)識.本文基于循環(huán)條件制導(dǎo)的符號執(zhí)行(Symbolic Execution)技術(shù)實現(xiàn)了循環(huán)內(nèi)界分析,該技術(shù)的本質(zhì)在于它能夠利用符號執(zhí)行符號化推導(dǎo)程序執(zhí)行約束的特點,準(zhǔn)確求解循環(huán)在程序所有合法輸入條件下的邊界值,并由生成的測試用例來保證該邊界值一定可達(即保證是循環(huán)內(nèi)界).本文對符號執(zhí)行制導(dǎo)技術(shù)進行了優(yōu)化,并在多組已有研究采用的基準(zhǔn)用例集上進行了實例評估,實驗結(jié)果表明,本文的循環(huán)內(nèi)界分析方法具備準(zhǔn)確性和高效性,可以滿足應(yīng)用需求.
[Abstract]:Loop is an important complex program structure in a computer. Many application scenarios require the maximum number of iterations that can be achieved by a static analysis loop. The corresponding technique is called Loop Bound Analysis in the literature. The existing circular boundary analysis uses conservative methods to carry out external analysis, that is, an approximate value slightly higher than the cyclic boundary. In this paper, a method of automatic circular inner bound analysis is proposed, which produces approximate values slightly lower than the cyclic boundary. When the user synthetically utilizes the external and inner boundary analysis, the cyclic boundary value can be restricted to a statistical interval. Therefore, a more complete understanding of the analysis results can be obtained. In this paper, the cyclic internal bound analysis is realized based on the symbolic execution execution technique based on cyclic conditional guidance. The essence of this technique is that it can accurately solve the boundary value of the loop under all the legitimate input conditions of the program by taking advantage of the characteristic of symbolic execution symbolic derivation program execution constraints. The generated test cases are used to ensure that the boundary value can be reached (that is, cyclic inner bound). In this paper, the symbolic execution guidance technology is optimized, and an example is evaluated on the set of reference cases that have been studied. The experimental results show that the proposed method is accurate and efficient, and can meet the needs of application.
【作者單位】: 南京大學(xué)軟件新技術(shù)國家重點實驗室;南京大學(xué)軟件學(xué)院;南瑞集團公司(國網(wǎng)電力科學(xué)研究院);國電南瑞科技股份有限公司;
【基金】:國家自然科學(xué)基金(No.61402222,No.61632015) 國家重點研發(fā)計劃(No.2016YFB1000802) 教育部高等學(xué)校博士學(xué)科點專項科研基金(No.20110091120058) 江蘇省產(chǎn)學(xué)研項目(No.BY2014126-03)
【分類號】:TP311.53
【相似文獻】
相關(guān)期刊論文 前10條
1 林夢香;陳胤立;陳睿;周剛;;基于懶替換的C符號執(zhí)行[J];北京航空航天大學(xué)學(xué)報;2009年06期
2 洪宇;陳光;于見平;韓柯;;處理符號執(zhí)行中數(shù)組元素混淆的一種新方法[J];計算機應(yīng)用;2005年S1期
3 過辰楷;姬秀娟;許靜;;基于分支混淆算法的符號執(zhí)行技術(shù)[J];計算機科學(xué);2012年09期
4 劉杰;曹琰;魏強;彭建山;;符號執(zhí)行中的循環(huán)依賴分析方法[J];計算機工程;2012年22期
5 黃暉;陸余良;夏陽;;基于動態(tài)符號執(zhí)行的二進制程序缺陷發(fā)現(xiàn)系統(tǒng)[J];計算機應(yīng)用研究;2013年09期
6 翁子盛;王寶生;林錦濱;;程序符號執(zhí)行中的數(shù)組分析[J];長江大學(xué)學(xué)報(自然科學(xué)版)理工卷;2010年01期
7 賈春福;王志;劉昕;劉昕海;;路徑模糊:一種有效抵抗符號執(zhí)行的二進制混淆技術(shù)[J];計算機研究與發(fā)展;2011年11期
8 周孔偉,蔡經(jīng)球;符號執(zhí)行—介于程序驗證和程序調(diào)試之間的方法[J];小型微型計算機系統(tǒng);1982年04期
9 高仲儀 ,梁霞;符號執(zhí)行和測試數(shù)據(jù)輔助生成的實驗系統(tǒng)[J];北京航空學(xué)院學(xué)報;1988年04期
10 程紹銀;蔣凡;林錦濱;唐艷武;;基于有限回溯符號執(zhí)行的軟件疑似缺陷的自動驗證[J];清華大學(xué)學(xué)報(自然科學(xué)版);2009年S2期
相關(guān)會議論文 前2條
1 林錦濱;張曉菲;劉暉;;符號執(zhí)行技術(shù)研究[A];全國計算機安全學(xué)術(shù)交流會論文集(第二十四卷)[C];2009年
2 劉峻宇;李強;余祥;何海洋;;基于符號執(zhí)行的指揮信息系統(tǒng)軟件缺陷檢測技術(shù)[A];2014第二屆中國指揮控制大會論文集(上)[C];2014年
相關(guān)博士學(xué)位論文 前8條
1 張羽豐;符號執(zhí)行可擴展性及可行性關(guān)鍵技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2013年
2 李游;統(tǒng)一的軟件測試控制流覆蓋準(zhǔn)則體系及其符號執(zhí)行制導(dǎo)技術(shù)研究[D];南京大學(xué);2016年
3 傅先進;基于符號執(zhí)行的MPI程序分析與驗證技術(shù)研究[D];國防科學(xué)技術(shù)大學(xué);2016年
4 范文慶;分段符號執(zhí)行模型及其環(huán)境交互問題研究[D];北京郵電大學(xué);2010年
5 安靖;動態(tài)符號執(zhí)行關(guān)鍵技術(shù)研究[D];北京郵電大學(xué);2014年
6 曹琰;面向軟件脆弱性分析的并行符號執(zhí)行技術(shù)研究[D];解放軍信息工程大學(xué);2013年
7 陳廳;動態(tài)程序分析技術(shù)在軟件安全領(lǐng)域的研究[D];電子科技大學(xué);2013年
8 邢學(xué)智;基于TTCN-3語言的測試?yán)碚撆c技術(shù)研究[D];中國科學(xué)技術(shù)大學(xué);2010年
相關(guān)碩士學(xué)位論文 前10條
1 李奇軍;基于符號執(zhí)行的代碼靜態(tài)檢測方法研究與實現(xiàn)[D];電子科技大學(xué);2015年
2 柯明敏;動態(tài)符號執(zhí)行在軟件漏洞自動化發(fā)掘領(lǐng)域的應(yīng)用研究[D];電子科技大學(xué);2015年
3 康文濤;符號執(zhí)行工具KLEE約束求解優(yōu)化設(shè)計與實現(xiàn)[D];電子科技大學(xué);2014年
4 吳情彪;基于符號執(zhí)行的軟件污點分析研究[D];武漢郵電科學(xué)研究院;2016年
5 陳冰;符號執(zhí)行技術(shù)研究與改進[D];南京大學(xué);2014年
6 李景曦;基于控制流分析的模糊測試技術(shù)研究[D];北京理工大學(xué);2016年
7 鮑鐵勻;符號執(zhí)行制導(dǎo)技術(shù)及其應(yīng)用研究[D];南京大學(xué);2016年
8 鄧維;形狀分析符號執(zhí)行引擎中的狀態(tài)合并[D];中國科學(xué)技術(shù)大學(xué);2016年
9 袁健;基于符號執(zhí)行的代碼安全檢查技術(shù)研究與實現(xiàn)[D];電子科技大學(xué);2016年
10 羅榮森;基于符號摘要的動態(tài)符號執(zhí)行的研究[D];電子科技大學(xué);2016年
,本文編號:1640371
本文鏈接:http://sikaile.net/kejilunwen/ruanjiangongchenglunwen/1640371.html