Abstract
摘要:網站應用程式是否設計正確不僅影響作業流程及網頁呈現,甚至牽動系統與資訊安全。動態產生網頁之程式若使用未經驗證的客戶輸入,便有可能造成如注入缺失、跨站腳本攻擊、跨站偽造要求等安全風險。雖然目前已有商業軟體安全檢測工具可以協助開發人員發現這類程式問題,但這些工具仍會出現誤報率偏高或漏報的情形。對第三方驗證者而言,往往因其對受檢程式結構所知有限,不理想的檢測工具很難達到節省驗證人力與時間的期待。為此,研究學者近年來持續努力研發更有效的分析與測試方法。在先前接受網路通訊國家型科技計畫補助的「軟硬體應用安全檢測平台建置計畫」中,我們也嘗試研發自主軟體安全檢測工具,企圖透過整合靜態與動態分析的方法,提升網站應用程式安全弱點分析的精準度。然而,在多重語言網頁程式的處理、靜態分析的深度以及適切滲透測試案例的自動產生等方面仍有許多改善的空間,對新式網站應用框架也極需較有系統的分析方法。
在本計畫中,我們預計研發並實作適用於網站應用程式正確性驗證之進階靜態分析與動態測試方法,更進一步提升網站應用安全弱點分析的精準度。首先,我們將延續原有利用中介語言之工具架構,完整轉譯多重語言之網頁程式並建立控制流程圖,以利後續分析與測試之進行。我們希望運用抽象化解譯的基本原理以及近年來在自動驗證中逐漸普及的反例導向抽象模型細步化的概念,加強靜態分析的深度。我們也將探討更多類型的程式安全弱點之分析。在滲透測試案例的自動產生方面,我們則希望不僅考慮字串限制條件,也能納入其他型別資料的限制。最後,我們希望針對一些較普遍的網站應用框架提出轉譯至中介語言的機制,使前述進階的分析與測試方法能有更廣泛的應用範圍。
Abstract: Correctness of a Web application not only affects the business process and the presentation of a webpage, but may also have security consequences. A program that dynamically generates webpages, if using input data without proper validation, may introduce security vulnerabilities such as Injection Flaws, Cross-Site Scripting, and Cross-Site Request Forgery. There are commercial code security analysis tools that may help programmers to find such problems, but they tend to produce high rates of false positives and sometimes even false negatives. For a third-party verifier who is usually unfamiliar with the code under evaluation, inadequate analysis tools would not meet the objective of reducing time and cost. Motivated researchers have been developing more efficient analysis methods and tools in the past few years. In a previous project ``Software/Hardware Application Security Testbeds`` sponsored by the NSC Networked Communications Program, we have also attempted to develop a tool for analyzing Web application security. The main idea was to combine static and dynamic analysis techniques to achieve higher precision. However, there leave large rooms for improvement regarding the treatment of Web applications with multiple languages, sophistication of static analysis, and automatic generation of penetration test cases. Applications using existing Web application frameworks also need a more systematic way of analysis.
In this project, we plan to develop advanced static analysis and dynamic testing techniques for verifying Web applications, aiming at achieving an even higher precision in security analysis. First of all, building on the use of an intermediate representation in our current tool, we will try to faithfully translate a Web application with multiple languages so that a complete control flow graph can be built for further analysis and testing. We plan to apply principles of abstract interpretation and techniques of counterexample-guided abstraction refinement that have become popular in automatic verification, in order to deepen the static analysis. We also plan to treat more kinds of security vulnerabilities. For test cases generation, we plan to consider not only string-valued, but also other types of, constraints. Finally, we plan to devise a mechanism for translating applications using popular Web application frameworks, in the hope of widening the applicability of the proposed analysis and testing techniques.
Keyword(s)
抽象化解譯
抽象模型細步化
自動驗證
動態分析
動態測試
模型檢測
安全弱點
軟體安全
字串分析
靜態分析
網站應用
Abstract Interpretation
Abstraction Refinement
Automatic Verification
Dynamic Analysis
Dynamic Testing
Model Checking
Security Vulnerabilities
Software Security
Static Analysis
String Analysis
Web Applications