通訊協定與網路應用程式安全性驗證方法之研究

Abstract

因為網路已經成為一個溝通上的基本要件，所以網路的安全性也跟著變得相當重要。而網路的安全性又可以從兩部分去看：安全性通訊協定和網路應用程式。在安全性通訊協定方面，隱私性和身份確認是兩樣常常被用來當作安全性驗證的共同目標。隱私性代表溝通過程中，訊息不能被非預期的對象所取得；身份確認則是用來防止網路中惡意的使用者假冒別人的身份去傳送訊息。在網路應用程式方面，跨站腳本攻擊和資料隱碼是OWASP在2007年排名出來最常發生的破壞行為的前兩名，因此也常被驗證方法用來當作偵測的目標。跨站腳本攻擊允許惡意使用者在受害者的瀏覽器上執行一些腳本語言，以達到偷取使用者cookie，插入惡意內容，甚至是控制整個瀏覽器等目的。資料隱碼則是藉由輸入一些不尋常的字串到網路應用程式裡，用來破壞或竊取資料庫。 在這篇論文裡面，我們總結了許多具代表性的驗證方法，不管是針對安全性通訊協定或是網路應用程式。在安全性通訊協定方面，我們主要深入研究兩個專案：AVISPA和ProVerif。這兩個專案的共通特性是他們都是state-exploration的方法。不過AVISPA又多了一些協助的機制，像是lazy intruder可以控制state的擴張。同時我們也概括收錄了其他驗證方法，例如定理證明、首階邏輯，或是模型檢驗。在網路應用程式方面，我們則是總結並探討了PQL和WebSSARI這兩個系統。PQL系統自己開發了一套用來描述弱點形態的語言。它最主要包括了可以保證不會漏報弱點的一套靜態分析方法，以及利用靜態分析結果來提高運作效率的動態偵測方法。WebSSARI則是先定義好污染數據和弱點函數，再將PHP程式碼轉換成一連串的邏輯限制式，用找反例的方式去找尋弱點。我們也說明了其他相關的系統，像是AspectJ，SQLCheck，和PTQL等。最後我們也對AVISPA和ProVerif作了一些比較。

Network security is essential because networks have become a basic element of communications. There are two critical parts of network security: security protocols and web applications. For security protocols, secrecy and authentication are two common properties that are usually checked by security protocol verifiers. Secrecy means that no unexpected agents could get the secret contents of messages. Authentication basically indicates that a message which appears to be from some agent is actually sent by the same agent. For web applications, there are many kinds of vulnerabilities. Between them, cross site scripting and injection flaws like SQL injection are the most common vulnerabilities summarized by OWASP. Cross site scripting allows attackers to execute script in the victim's browser, which can steal user sessions, insert malicious context, and even control the browser. SQL injection inputs unexpected string as queries and can be used to operate the database without authorization. In this thesis, we review several representative verification methods for security protocols and web applications in detail. For security protocols, we study two projects in depth: AVISPA and ProVerif. The commonality of these two projects is that they are both state-exploration methods. However, the AVISPA project has some additional assistant mechanisms such as the lazy intruder to control over the state exploration. We also survey other methods using theorem proving, first-order logic, and model checking. For web applications, the two systems, PQL and WebSSARI, are summarized and discussed. PQL has its own query language to specify vulnerable patterns and utilizes static analysis, which guarantee no false negatives, and dynamic monitoring, which is based on the result of the static analysis. WebSSARI defines the tainted data and sinks in advance and transforms the verification into SAT. It also provides a strategy of efficiently sanitizing. Other related works like AspectJ, SQLCheck, and PTQL are also briefly explained. Finally, we compare AVISPA with ProVerif, and PQL with WebSSARI.