Publications-NSC Projects

Article View/Open

Publication Export

Google ScholarTM

NCCU Library

Citation Infomation

Related Publications in TAIR

題名 符號式字串驗證:對網路應用程式自動化弱點掃描與補正的正規方法研究與工具開發(I)
其他題名 Symbolic String Verification---A Formal Approach for Automatic Web Application Vulnerability Detection and Sanitization Synthesis
作者 郁方
貢獻者 國立政治大學資訊管理學系
行政院國家科學委員會
關鍵詞 符號式字串驗證;網路
日期 2010
上傳時間 30-Aug-2012 15:48:51 (UTC+8)
摘要 本計畫將探討符號式字串分析的相關技術,運用自動機表示字串變數的可能值來 進行字串運算程式的驗證。以此技術為基礎,開發全自動化的程式分析工具,針對網 路應用程式可能存在的安全漏洞(弱點)進行正規化的掃描與補正。 我們的方法包含三個步驟:首先,我們先以正向分析辨識應用程式內所有可能的安全 漏洞。一個安全漏洞表式程式的某個敏感函數可能在執行時使用不適當(給定)的字 串值,從而允許使用者對應用程式進行惡意攻擊。針對每一個安全漏洞,我們接著計 算所有可能會導致此惡意攻擊的使用者輸入值。我們稱此為漏洞表徵。要避免使用者 攻擊,我們自動化產生淨化程式。此淨化程式會在應用程式執行時,對符合漏洞表徵 的使用者輸入值進行(最少化的)修改,從而避免可能的惡意攻擊發生。對多個輸入 源的安全漏洞,我們運用多軌自動機描述輸入值之間的關連性,從而產生更有效率的 淨化程式。我們也將探討與整合靜態字串分析的先進技術,包含字串抽象化、符號式 自動機、語言替代運算與最小終結點運算加速。這增強我們分析的實用性。 我們將發展一開放的網路平台提供嚴謹的字串分析服務。針對目前最嚴重的惡意攻擊 (如SQL Injection, XSS),偵測與移除網路應用程式可能的安全漏洞。
We investigate automata‐based string verification techniques and apply the techniques for automatic vulnerability detection and sanitization synthesis for Web applications. Our approach consists of three phases: Given an attack pattern we first conduct a vulnerability analysis to identify if strings that match the attack pattern can reach the security‐sensitive functions. Next, we compute vulnerability signatures that characterize all input strings that can exploit the discovered vulnerability. Given the vulnerability signatures, we then construct sanitization statements that 1) check if a given input matches the vulnerability signature and 2) modify the input in a minimal way so that the modified input does not match the vulnerability signature. Particularly, we are interested in generating relational vulnerability signatures (and corresponding sanitization statements) for vulnerabilities that are due to more than one input. Our approach also features other advance techniques including string abstractions, symbolic automata encoding, fixpoint acceleration, and language‐based replacement. We provide a scalable web service using cloud‐computing techniques. Public users can find and eliminate string‐related security vulnerabilities, such as SQL Injections and XSS attacks, in their Web applications. Based on our automata‐based string analysis, the service is capable of identifying potential vulnerabilities, generating effective patches for vulnerable applications, and proving the absence of vulnerabilities in well‐developed applications.
關聯 基礎研究
學術補助
研究期間:9911~ 10007
研究經費:520仟元
資料類型 report
dc.contributor 國立政治大學資訊管理學系en_US
dc.contributor 行政院國家科學委員會en_US
dc.creator (作者) 郁方zh_TW
dc.date (日期) 2010en_US
dc.date.accessioned 30-Aug-2012 15:48:51 (UTC+8)-
dc.date.available 30-Aug-2012 15:48:51 (UTC+8)-
dc.date.issued (上傳時間) 30-Aug-2012 15:48:51 (UTC+8)-
dc.identifier.uri (URI) http://nccur.lib.nccu.edu.tw/handle/140.119/53422-
dc.description.abstract (摘要) 本計畫將探討符號式字串分析的相關技術,運用自動機表示字串變數的可能值來 進行字串運算程式的驗證。以此技術為基礎,開發全自動化的程式分析工具,針對網 路應用程式可能存在的安全漏洞(弱點)進行正規化的掃描與補正。 我們的方法包含三個步驟:首先,我們先以正向分析辨識應用程式內所有可能的安全 漏洞。一個安全漏洞表式程式的某個敏感函數可能在執行時使用不適當(給定)的字 串值,從而允許使用者對應用程式進行惡意攻擊。針對每一個安全漏洞,我們接著計 算所有可能會導致此惡意攻擊的使用者輸入值。我們稱此為漏洞表徵。要避免使用者 攻擊,我們自動化產生淨化程式。此淨化程式會在應用程式執行時,對符合漏洞表徵 的使用者輸入值進行(最少化的)修改,從而避免可能的惡意攻擊發生。對多個輸入 源的安全漏洞,我們運用多軌自動機描述輸入值之間的關連性,從而產生更有效率的 淨化程式。我們也將探討與整合靜態字串分析的先進技術,包含字串抽象化、符號式 自動機、語言替代運算與最小終結點運算加速。這增強我們分析的實用性。 我們將發展一開放的網路平台提供嚴謹的字串分析服務。針對目前最嚴重的惡意攻擊 (如SQL Injection, XSS),偵測與移除網路應用程式可能的安全漏洞。en_US
dc.description.abstract (摘要) We investigate automata‐based string verification techniques and apply the techniques for automatic vulnerability detection and sanitization synthesis for Web applications. Our approach consists of three phases: Given an attack pattern we first conduct a vulnerability analysis to identify if strings that match the attack pattern can reach the security‐sensitive functions. Next, we compute vulnerability signatures that characterize all input strings that can exploit the discovered vulnerability. Given the vulnerability signatures, we then construct sanitization statements that 1) check if a given input matches the vulnerability signature and 2) modify the input in a minimal way so that the modified input does not match the vulnerability signature. Particularly, we are interested in generating relational vulnerability signatures (and corresponding sanitization statements) for vulnerabilities that are due to more than one input. Our approach also features other advance techniques including string abstractions, symbolic automata encoding, fixpoint acceleration, and language‐based replacement. We provide a scalable web service using cloud‐computing techniques. Public users can find and eliminate string‐related security vulnerabilities, such as SQL Injections and XSS attacks, in their Web applications. Based on our automata‐based string analysis, the service is capable of identifying potential vulnerabilities, generating effective patches for vulnerable applications, and proving the absence of vulnerabilities in well‐developed applications.en_US
dc.language.iso en_US-
dc.relation (關聯) 基礎研究en_US
dc.relation (關聯) 學術補助en_US
dc.relation (關聯) 研究期間:9911~ 10007en_US
dc.relation (關聯) 研究經費:520仟元en_US
dc.subject (關鍵詞) 符號式字串驗證;網路en_US
dc.title (題名) 符號式字串驗證:對網路應用程式自動化弱點掃描與補正的正規方法研究與工具開發(I)zh_TW
dc.title.alternative (其他題名) Symbolic String Verification---A Formal Approach for Automatic Web Application Vulnerability Detection and Sanitization Synthesisen_US
dc.type (資料類型) reporten