帳號:guest(18.234.55.154)          離開系統
字體大小: 字級放大   字級縮小   預設字形  

詳目顯示

以作者查詢圖書館館藏以作者&題名查詢臺灣博碩士以作者查詢全國書目
作者:翁文健
作者(英文):Weng, Wen-Chien
論文名稱(中文):藉由迴圈相依性與限制式牴觸分析進行大範圍安全性質檢查
論文名稱(英文):Scalable Security Property Checking by Loop Dependence and Constraint Contradiction Analysis
指導教授(中文):黃世昆
指導教授(英文):Huang, Shih-Kun
學位類別:碩士
校院名稱:國立交通大學
系所名稱:資訊科學與工程研究所
學號:9655527
出版年(民國):98
畢業學年度:97
語文別:英文
論文頁數:45
中文關鍵詞:安全性質檢查全範圍檢查
外文關鍵詞:security property checkconcolic testinguniversal check
相關次數:
  • 推薦推薦:0
  • 點閱點閱:645
  • 評分評分:*****
  • 下載下載:4
  • 收藏收藏:0
安全性質檢查用來確認程式中是否存在違反安全性質且可被利用進行惡意攻擊之程式碼。對於邊界值測資以及動態程式分析很難進行此類檢查。故此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.
摘要 i
Abstract ii
致謝 iii
Content iv
List of Figures vi
List of Tables vii
1 Introduction 1
1.1 Problem Descriptions 1
1.2 Motivation 2
1.3 Objective 2
2 Background 3
2.1 Program testing 3
2.2 Symbolic execution 3
2.3 Concolic execution 4
2.4 Static test generation 5
2.5 Dynamic test generation 5
2.6 Security property checking 6
2.7 ALERT 6
3 Related work: Constraint-based Execution Optimization 9
3.1 Constraint Solving Optimization 9
3.1.1 Minimizing Number of Calls to Constraint Solver 9
3.1.2 Minimizing Formulas 10
3.2 Path Optimization 12
3.2.1 Constraint Caching and reusing 12
3.2.2 Path Reduction 14
4 Method 17
4.1 Loop dependence analysis 17
4.2 Constraint contradiction detection 18
4.3 Reverse incremental check algorithm 19
5 Implementation 22
5.1 Data structure 22
5.1.1 Structure 22
5.1.2 Vector 22
5.2 Naming 23
5.3 Taint analysis 24
5.3.1 Tainted by global variable 24
5.3.2 Tainted by function arguments 24
5.3.3 Tainted by return value 25
5.3.4 Tainted by pass by address 26
5.4 Nested loop 27
5.5 Loop constraints elimination 27
6 Evaluations 32
6.1 Sort algorithms compared with CREST 32
6.2 An n*n matrix allocation example 40
7 Conclusion 43
References 44
References
[1] Patrice Godefroid, "Compositional dynamic test generation," in POPL '07: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 47-54, 2007.
[2] Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill and Dawson R. Engler, "EXE: Automatically generating inputs of death," In CCS '06: Proceedings of the 13th ACM Conference on Computer and Communications Security, pp. 322-335, 2006.
[3] Koushik Sen, Darko Marinov and Gul Agha, "CUTE: A concolic unit testing engine for C," In ESEC/FSE-13: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 263-272, 2005.
[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.
[6] K. Krause, M. Goodwin and R. Smith, "Optimal Software Test Planning through Automated Network Analysis," IEEE Symposium on Computer Software Reliability, pp. 18-22, April 1973.
[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.
[9] Patrice Godefroid, Nils Klarlund and Koushik Sen, "DART: Directed automated random testing," In PLDI '05: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 213-223, 2005.
[10] Eric Larson and Todd Austin, "High coverage detection of input-related security faults," In Proceedings of the 12th USENIX Security Symposium (Security '03), August 2003.
[11] Christoph Csallner and Yannis Smaragdakis, "Check'n'crash: Combining static checking and testing," In Proceedings of the 27th International Conference on Software Engineering, pp. 422-431, 2005.
[12] Willem Visser, Corina S. P□s□reanu and Sarfraz Khurshid, "Test input generation with java PathFinder," In Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 97-107, 2004.
[13] Tao Xie, Darko Marinov, Wolfram Schulte and David Notkin, "Symstra: A framework for generating object-oriented unit tests using symbolic execution," In the Tools and Algorithms for the Construction and Analysis of Systems, pp. 365-381, 2005.
[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.
[15] Bogdan Korel, "A dynamic approach of test data generation," IEEE Conference on Software Maintenance, pp. 311--317, November 1990.
[16] Bogdan Korel, "Automated software test data generation," IEEE Transactions of Software Engineering, vol. 16, pp. 870-879, 1990.
[17] Nicholas Nethercote and Julian Seward, "Valgrind: A framework for heavyweight dynamic binary instrumentation," In Proceedings of the 2007 PLDI Conference, pp. 89-100, 2007.
[18] Reed Hastings and Bob Joyce, "Purify: Fast detection of memory leaks and access errors," In Proceedings of the Winter USENIX Conference, http://www.rational.com/supprot/techpapers/fast_detection/, 1992.
[19] Patrice Godefroid, Michael Y. Levin and David A. Molnar, "Automated whitebox fuzz testing," In Proceedings of the Network and Distributed System Security Symposium, http://research.microsoft. com/users/pg/public_psfiles/ndss2008.pdf, 2008.
[20] Yang-Chieh Fan, "Resolving Constraints from COTS/Binary Components for Concolic Random Testing," 2007.
[21] Peter Boonstoppel, Cristian Cadar and Dawson Engler, "RWset: Attacking path explosion in constraint-based test generation," Lecture Notes in Computer Science, vol. 4963, pp. 351, 2008.
 
 
 
 
第一頁 上一頁 下一頁 最後一頁 top
* *