申請免費試用帳號
與我們聯繫
資源中心
|
|
|
學術出版品
|
|
以錯誤植入和行為監控，進行 Web 應用程式安全的評估
網際網路是一個龐大而複雜的應用程式平台，能夠傳送相當多樣、複雜的軟體。然而，許多 Web 應用程式在極短的往返時間內，經歷快速的開發階段，難以排除漏洞
在此，我們分析 Web 應用程式安全評估機制的設計，來發現使 Web 應用程式產生弱點而遭受攻擊的不安全源碼撰寫，例如跨站腳本攻擊和 SQL 注入。我們說明了一些軟體測 試技巧的用法 （包括動態分析、黑箱測試、錯誤植入和行為監控） ，並建議將這些技術應用於 Web 應用程式的機制。真實情境慣於測試我們稱之為 Web 應用程式漏洞 和錯誤掃描器的工具 （WAVES，一個開放源碼的專案，相關內容可連結至http://waves.sourceforge.net） ，並與其他工具相 比。我們的結果顯示， WAVES 是評估 Web 應用程式安全的可行平台。
|
|
以錯誤植入和行為監控，進行 Web 應用程式安全的評估
|
|
Web 應用程式安全評估的測試架構
快速發展階段和極簡短的 Web 應用程式往返時間，難以排除他們的漏洞
我們研究軟體的測試技巧，像是錯誤植入和執行監控，都可應用於 Web 應用程式中。我們在 Web 應用程式弱點和誤差掃描 （WAVES） 中導入了我們所提供的機制 - 即自動 Web 應用程式安全評估的黑箱測試架構。於真實情況下測試 WAVES ，並和其他工具比較
我們的結果顯示， WAVES 是評估 Web 應用程式安全的可行平台。© 2005 Elsevier B.V. 版權所有。
|
|
Web 應用程式安全評估的測試架構
|
|
無危害 Web 應用程式安全掃描
網際網路已成為一個可提供廣泛用途應用程式的複雜平台。然而，它的急速成長卻導致許多現代科技所無法處理的資安問題。學術研究機構與私人單位的研究員都不約而同地投入相當可觀的資源，開發 Web 應用程式安全掃描器，並且頗有斬獲（例如，供 Web 應用程式安全稽核的自動軟體測試平台）。但對於其潛在的副作用，卻一無所悉
稽核程序可能導致應用程式狀態永久的改變。基於這個潛在因子，我們已盡可能避免 Web 應用程式漏洞與誤差掃描器 （WAVES） 的大規模實證評估
我們在論文中介紹了可進行無害稽核的測試方法論，定義三種測試模式 - 沉重、寬鬆與安全模式，並提出這兩個測驗的結果報告。首先，我們利用先前靜態驗證工作中找到38個弱點中所挑選出的5個真實世界 Web 應用程式，比較三種掃描模式的涵蓋範圍和副作用。接著，我們採用寬鬆模式，執行48小時測試，範圍涵蓋1120個隨機網站，其中找到55個含有漏洞。
|
|
無危害 Web 應用程式安全掃描
|
|
以靜態分析和動態防護來確保 Web 應用程式的安全
安全性仍普遍被認為是各種網路交易大量普及的主要障礙，特別是近來因 Web 應用程式中的瑕疵或錯誤，進而導致可遠距攻擊的漏洞急遽增加。許多驗證工具仍持續在一些老舊、多年未碰的的傳統語言程式中不斷發現先前未知的漏洞，而要在快速變化更動的 Web 應用程式找到這些錯誤的機率相對地是非常高的
在論文中，我們舉出了健全且全面的方法，以確保 Web 應用程式的安全。將 Web 應用程式漏洞視為安全資訊流量問題，我們從類型系統和類型狀態建立出點陣式靜態 分析運算法則，使其更健全。分析過程中，被視為弱點的程式碼部分被配上執行防護，從而確保 Web 應用程式將不再受到使用者的干預
在充分的註解與說明，執行時期成本可降到零。我們更建立了名為 WebSSARI （靜態分析與執行檢視的 Web 應用程式安全） 的工具，測試我們的運算法則，利用該程 式檢驗 SourceForge.net 上230個來源開放的 Web 應用程式專案，這些專案被挑選代表它們具備不同成熟度、知名度和規模。其中69個含有弱點，並且已通知其開發者
當中有38個開發者肯定我們的發現，並進一步說明其修補計畫。我們的數據同時顯示，靜態分析所降低的執行時期動態檢測成本高達98.4%
|
|
以靜態分析和動態防護來確保 Web 應用程式的安全
|
|
使用有界模型檢查 （Bounded Model Checking） 來驗證 Web 應用程式
作者提出一個可驗證網路應用程式源碼的有界模型檢查 （Bounded Model Checking，BMC）
不安全的程式碼區段會以執行時期防護功能自動修正，在使用者不需介入的情形下，進行驗證與確認的動作。雖然模型檢查技術比我們在之前論文中的 Typestate 型多項式時間演算法 （TS） 更複雜，但其具備三項優勢：提供反例、更精確的模型，以及完整健全的驗證。
與傳統模型檢查技術相比， BMC 提供更實用的程式驗證方法，其中包含大量的變數，但需要固定的程式範圍才可完成
要確保 BMC 應用程式內沒有錯誤產生，必須將 Web 應用程式內的弱點形式化為安全資料流問題，並為固定範圍。若使用 BMC 產生的反例，由相同初始錯誤衍生的其他錯誤則可通報為同一組錯誤，而非個別的錯誤
|
|
使用有界模型檢查 （Bounded Model Checking） 來驗證 Web 應用程式
|
|
