藉由迴圈相依性與限制式牴觸分析進行大範圍安全性質檢查

Scalable Security Property Checking by Loop Dependence and Constraint Contradiction Analysis

翁文健(Wen-Chien Weng)

指導教授 ： 黃世昆

國立交通大學/資訊學院/資訊科學與工程研究所/碩士(2009年)

https://doi.org/10.6842/NCTU.2009.00646

摘要

安全性質檢查用來確認程式中是否存在違反安全性質且可被利用進行惡意攻擊之程式碼。對於邊界值測資以及動態程式分析很難進行此類檢查。故此Execution Generate Executions即EXE提出了universal check的概念，可以輕易地於動態程式分析中進行安全性質檢查，涵蓋範圍遍及所有可執行路徑。然而進行大範圍universal check是有困難的，因為執行路徑中if-statement的數量會呈指數成長。可是大部分的安全性質檢查是多餘的，原因如下：(1) 在迴圈之中或之後的安全性質檢查可能與迴圈執行結果無關。(2) 有其他的條件式保護造成多餘的安全性質檢查。本篇論文提出偵測此類多餘以及不必要的安全性質檢查。我們使用(1)迴圈相依性測試檢測迴圈與安全性質檢查的相關性。(2)條件式牴觸分析判斷安全性質檢查是否已被其他條件式限制保護。

關鍵字

安全性質檢查 ； 全範圍檢查

並列摘要

Security property check is to verify if a program violates security rules and can be exploited to execute arbitrary code. This type of check is hard to be performed by testing with corner cases and dynamic program analysis. Thus Execution Generate Executions, or EXE for short, proposes the idea of universal check which is easy for dynamic program analysis and could cover all execution paths. Unfortunately, universal check is not scalable. The number of the if-statement of the execution path can be exponentially exploded, and most of the property checks are redundant, due to two reasons: (1) Property checks within or after a loop statement and the checks may not dependent on the loop. (2) The check is already protected by other constraints. This paper proposes methods to detect those redundant or unnecessary checks. We use (1) loop dependence analysis to check the dependency relationship between loop and property check, and the necessity of this check, and (2) constraint contradiction analysis to evaluate if the property check is already bounded by other constraints.

並列關鍵字

security property check ； concolic testing ； universal check

參考文獻

[14] Neelam Gupta, Aditya P. Mathur and Mary Lou Soffa, "Generating test data for branch coverage," in Proceedings of the International Conference on Automated Software Engineering, pp. 219, 2000.

[4] Bernard Elspas, Karl N. Levitt, Richard J. Waldinger and Abraham Waksman, "An assessment of echniques for proving program correctness," ACM Computing Surveys (CSUR), vol. 4, pp. 97-147, 1972.

[5] Chittor V. Ramamoorthy and Siu-Bun Ho, "Testing large software with automated software evaluation systems," In Proceedings of the International Conference on Reliable Software Table of Contents, pp. 382-394, 1975.

[7] William E. Howden, "Methodology for the generation of program test data," IEEE Transactions on Computers, vol. 100, pp. 554-560, 1975.

[8] James C. King, "Symbolic execution and program testing," Communications of the ACM, vol. 19, pp. 385-394, 1976.