- 學位論文
藉由迴圈相依性與限制式牴觸分析進行大範圍安全性質檢查
Scalable Security Property Checking by Loop Dependence and Constraint Contradiction Analysis
摘要
安全性質檢查用來確認程式中是否存在違反安全性質且可被利用進行惡意攻擊之程式碼。對於邊界值測資以及動態程式分析很難進行此類檢查。故此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.