Responsive image
博碩士論文 etd-0820109-230125 詳細資訊
Title page for etd-0820109-230125
論文名稱
Title
模型檢驗用於偵測網頁應用程式安全弱點之研究
Verifying Web Application Vulnerabilities by Model Checking
系所名稱
Department
畢業學年期
Year, semester
語文別
Language
學位類別
Degree
頁數
Number of pages
77
研究生
Author
指導教授
Advisor
召集委員
Convenor
口試委員
Advisory Committee
口試日期
Date of Exam
2009-07-20
繳交日期
Date of Submission
2009-08-20
關鍵字
Keywords
可滿足性模理論、模型檢驗、網頁應用程式安全弱點
Model Checking, SMT, Satisfiability Modulo Theories, Web application vulnerability
統計
Statistics
本論文已被瀏覽 5827 次,被下載 6
The thesis/dissertation has been browsed 5827 times, has been downloaded 6 times.
中文摘要
由於網際網路科技的不斷進步,愈來愈多民眾願意透過互動性高、多元化的網頁應用程式(web application)來進行商業、知識分享以及社交活動。然而,隨著網頁程式逐漸深入社會結構,駭客便開始利用網頁程式的邏輯缺陷,來對無辜使用者以及後端資料庫進行攻擊,因而造成資訊安全上的嚴重威脅。
有鑑於此,本研究提出一套基於模型檢驗(Model Checking)的偵測機制來進行安全漏洞的檢測。我們將安全弱點的存在問題轉化為一種可滿足性模理論 (Satisfiability Modulo Theories, SMT)問題,並利用SMT解題器(solver)來分析惡意資料在網頁程式中的所有流向,以找出可能的安全弱點。根據本研究實驗結果顯示,我們所提出的方法能有效地檢測出SQL injection與XSS安全漏洞,並證明其為一種可行的網頁應用程式安全弱點偵測方法。
Abstract
Due to the continued development of Internet technology, more and more people are willing to take advantage of high-interaction and diverse web applications to deal with commercial, knowledge-sharing, and social activities. However, while web applications deeply affect our society by degrees, hackers start exploiting web application vulnerabilities to attack innocent end user and back-end database, and therefore pose significant threat in information security.
According to this situation, this paper proposes a detection mechanism based on Model Checking to detect web application vulnerabilities. We reduce the problem whether the vulnerabilities exist or not to a kind of SMT (Satisfiability Modulo Theories) problem, and analyze all of the traces of tainted data flow in web applications to find possible vulnerabilities by SMT solver. The experimental results show that the method we proposed can identify SQL injection and XSS vulnerabilities effectively, and prove our method is a feasible way to find web application vulnerabilities.
目次 Table of Contents
1. 緒論 1
1.1 研究背景 1
1.2 研究動機與目標 2
1.3 論文架構 4
2. 文獻探討 5
2.1 網頁應用程式安全弱點 5
2.1.1 XSS (Cross Site Scripting) 5
2.1.2 SQL Injection 7
2.2 安全弱點檢測機制 9
2.2.1 伺服器端檢測技術 9
2.2.2 客戶端檢測技術 15
2.3 模型檢驗(Model Checking) 18
2.3.1 模型檢驗的概念 18
2.3.2 時序邏輯(Temporal Logic) 19
2.3.3 模型檢驗之演進 22
2.3.4 模型檢驗之實例 23
2.4 可滿足性模理論(Satisfiability Modulo Theories, SMT) 27
3. 研究方法與架構 30
3.1 前處理階段(The Preprocessing Phase) 31
3.1.1 轉譯前的準備 31
3.1.2 程式碼展開 32
3.1.3 變數更名(Variable Renaming) 33
3.1.4 Side Effects 34
3.1.5 特殊函式與情況 37
3.1.6 消除goto指令 40
3.2 程式插裝階段(The Instrument Phase) 41
3.2.1 插入與定義監控變數 42
3.2.2 調整監控變數之值 44
3.2.3 插入assertion 44
3.3 編碼階段(The Encoding Phase) 45
3.3.1 基礎資料型態的塑模 46
3.3.2 物件的塑模 46
3.3.3 陣列的塑模 48
3.3.4 Assertion的塑模 49
3.3.5 分支陳述式的塑模 50
3.4 使用SMT解題器進行偵測 51
4. 實驗結果與討論 54
4.1 實驗假設與限制 54
4.2 實驗樣本 55
4.3 實驗流程 55
4.4 實驗結果與分析 57
4.5 討論與比較 58
4.5.1 與黑箱測試法的比較 58
4.5.2 與其他靜態污染分析的比較 59
4.5.3 與動靜態分析結合法的比較 61
5. 結論與未來研究方向 62
5.1 結論 62
5.2 未來研究方向 63
參考文獻 64
參考文獻 References
1.Armando, A., J. Mantovani, and L. Platania, Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers, in 13th International SPIN Workshop on Model Checking of Software. 2006, Springer: Vienna, Austria. p. 146-162.
2.Barrett, C. and S. Berezin, CVC Lite: A new implementation of the cooperating validity checker, in Proceedings of the 16 th International Conference on Computer Aided Verification. 2004, Springer. p. 515–518.
3.Barrett, C. and C. Tinelli, CVC3, in Proceedings of the 19th International Conference on Computer Aided Verification (CAV '07), W. Damm and H. Hermanns, Editors. 2007, Springer: Berlin, Germany. p. 298-302.
4.Biere, A., et al., Bounded model checking. Advances in computers, 2003. 58: p. 118-149.
5.Biere, A., et al., Symbolic Model Checking without BDDs, in Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS '99). 1999, Springer. p. 193-207.
6.Bryant, R.E., Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, 1986. 35(8): p. 677-691.
7.Burch, J.R., et al., Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1994. 13(4): p. 401-424.
8.Burch, J.R., et al., Symbolic model checking: 1020 states and beyond. Information and Computation, 1992. 98(2): p. 142-170.
9.Christensen, A.S., A. M‥oller, and M.I. Schwartzbach, Precise analysis of string expressions, in In Proceedings of the 10th International Static Analysis Symposium, SAS’03. 2003, Springer-Verlag. p. 1-18.
10.Clarke, E. and D. Kroening, ANSI-C bounded model checker user manual. 2006, School of Computer Science, Carnegie Mellon University.
11.Clarke, E., D. Kroening, and K. Yorav, Behavioral Consistency of C and Verilog Programs using Bounded Model Checking. 2003, Technical Report CMU-CS-03-126, Carnegie Mellon University, School of Computer Science.
12.Clarke, E., D. Kroening, and K. Yorav, Behavioral consistency of C and verilog programs using bounded model checking, in Proceedings of the 40th annual Design Automation Conference. 2003, ACM: Anaheim, CA, USA. p. 368-371.
13.Clarke, E.M., E.A. Emerson, and A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 1986. 8(2): p. 244-263.
14.Clarke, E.M., O. Grumberg, and D.E. Long, Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 1994. 16(5): p. 1512-1542.
15.Clarke, E.M., O. Grumberg, and D. Peled, Model Checking. 2001, Cambridge: MIT Press. p. 35-49.
16.Cook, S., A Web Developer’s Guide to Cross-Site Scripting. 2003, Technical report, SANS Institute.
17.Ganai, M.K., et al. Towards Precise and Scalable Verification of Embedded Software. in 2008 Design and Verification Conference (DVCon). 2008. San Jose, CA.
18.Gould, C., Z. Su, and P. Devanbu, Static checking of dynamically generated queries in database applications, in Proceedings of the 26th International Conference on Software Engineering (ICSE '04). 2004. p. 645–654.
19.Halfond, W.G.J. and A. Orso, AMNESIA: analysis and monitoring for NEutralizing SQL-injection attacks, in Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering. 2005, ACM: Long Beach, CA, USA. p. 174-183.
20.Halfond, W.G.J. and A. Orso, Combining static analysis and runtime monitoring to counter SQL-injection attacks, in Proceedings of the third international workshop on Dynamic analysis. 2005, ACM: St. Louis, Missouri. p. 1-7.
21.Huang, Y.-W., et al., Securing web application code by static analysis and runtime protection, in Proceedings of the 13th international conference on World Wide Web (WWW 2004). 2004, ACM: New York, NY, USA. p. 40-52.
22.Huang, Y.-W., et al., Verifying Web Applications Using Bounded Model Checking, in Proceedings of the 2004 International Conference on Dependable Systems and Networks. 2004, IEEE Computer Society: Florence, Italy. p. 199–208.
23.Jovanovic, N., C. Kruegel, and E. Kirda, Pixy: A Static Analysis Tool for Detecting Web Application Vulnerabilities (Short Paper), in Proceedings of the 2006 IEEE Symposium on Security and Privacy. 2006, IEEE Computer Society: Oakland, CA. p. 258-263.
24.Jovanovic, N., C. Kruegel, and E. Kirda. Precise alias analysis for syntactic detection of web application vulnerabilities. in ACM SIGPLAN Workshop on Programming Languages and Analysis for Security. 2006. Ottowa, Canada.
25.Kirda, E., et al., Noxes: a client-side solution for mitigating cross-site scripting attacks, in Proceedings of the 2006 ACM symposium on Applied computing. 2006, ACM: Dijon, France. p. 330-337.
26.Lee, D.T., et al., Non-Detrimental Web Application Security Scanning, in Proceedings of the 15th International Symposium on Software Reliability Engineering (ISSRE '04). 2004, IEEE Computer Society: France. p. 219-230.
27.Lee, D.T., et al., A testing framework for Web application security assessment. Computer Networks, 2005. 48(5): p. 739-761.
28.Livshits, V.B. and M.S. Lam, Finding security vulnerabilities in java applications with static analysis, in Proceedings of the 14th conference on USENIX Security Symposium. 2005, USENIX Association: Baltimore, MD. p. 271–286.
29.Martin, M. and M.S. Lam, Automatic generation of XSS and SQL injection attacks with goal-directed model checking, in Proceedings of the 17th conference on Security symposium. 2008, USENIX Association: San Jose, CA. p. 31-43.
30.Martin, M., B. Livshits, and M.S. Lam, SecuriFly: Runtime vulnerability protection for Web applications. 2006, Technical report, Stanford University.
31.OWASP. Cross-site Scripting (XSS). July 4, 2009 [cited 2009 July 7]; Available from: http://www.owasp.org/index.php/Cross-site_Scripting_(XSS).
32.OWASP, The ten most critical Web application security vulnerabilities. 2007, OWASP Foundation.
33.Palshikar, G.K. An introduction to model checking. Dec. 2, 2004 [cited 2009 July 7]; Available from: http://www.embedded.com/columns/technicalinsights/17603352?_requestid=157933.
34.Scott, D. and R. Sharp, Abstracting application-level web security, in Proceedings of the 11th international conference on World Wide Web. 2002, ACM: Honolulu, Hawaii, USA. p. 396–407.
35.Scott, D. and R. Sharp, Developing Secure Web Applications. IEEE Internet Computing, 2002. 6(6): p. 38-45.
36.Sistla, A.P. and E.M. Clarke, The complexity of propositional linear temporal logics. Journal of the ACM, 1985. 32(3): p. 733-749.
37.SourceForge.net. Available from: http://sourceforge.net/.
38.Visser, W., et al., Model checking programs. Automated Software Engineering, 2003. 10(2): p. 203-232.
39.Vogt, P., et al. Cross site scripting prevention with dynamic data tainting and static analysis. in Proceeding of the Network and Distributed System Security Symposium (NDSS). 2007. San Diego, CA.
40.Walter, D., S. Little, and C. Myers, Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver, in Automated Technology for Verification and Analysis 5th International Symposium (ATVA). 2007, Springer: Tokyo, Japan. p. 66-81.
41.Wassermann, G. and Z. Su, Static detection of cross-site scripting vulnerabilities, in Proceedings of the 30th international conference on Software engineering. 2008, ACM: Leipzig, Germany. p. 171-180.
42.Whaley, J. and M.S. Lam, Cloning-based context-sensitive pointer alias analysis using binary decision diagrams, in Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation. 2004, ACM: Washington DC, USA. p. 131-144.
43.Wikipedia. Computation tree logic. June 29, 2009 [cited 2009 July 7]; Available from: http://en.wikipedia.org/wiki/Computational_tree_logic.
44.Wikipedia. Linear temporal logic. June 12, 2009 [cited 2009 July 7]; Available from: http://en.wikipedia.org/wiki/Linear_temporal_logic.
45.Wikipedia. Satisfiability Modulo Theories. June 17, 2009 [cited 2009 July 7]; Available from: http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories.
46.Xu, L., SMT-Based Bounded Model Checking for Real-Time Systems (Short Paper), in Proceedings of the 2008 The Eighth International Conference on Quality Software. 2008, IEEE Computer Society. p. 120-125.
47.李德財、黃耀文。2005。Web應用軟體安全之研究。中央研究院學術諮詢總會通訊。第十三卷,第二期,101-105頁。
電子全文 Fulltext
本電子全文僅授權使用者為學術研究之目的,進行個人非營利性質之檢索、閱讀、列印。請遵守中華民國著作權法之相關規定,切勿任意重製、散佈、改作、轉貼、播送,以免觸法。
論文使用權限 Thesis access permission:校內一年後公開,校外永不公開 campus withheld
開放時間 Available:
校內 Campus: 已公開 available
校外 Off-campus:永不公開 not available

您的 IP(校外) 位址是 44.212.50.220
論文開放下載的時間是 校外不公開

Your IP address is 44.212.50.220
This thesis will be available to you on Indicate off-campus access is not available.

紙本論文 Printed copies
紙本論文的公開資訊在102學年度以後相對較為完整。如果需要查詢101學年度以前的紙本論文公開資訊,請聯繫圖資處紙本論文服務櫃台。如有不便之處敬請見諒。
開放時間 available 已公開 available

QR Code