學術產出-Theses
Article View/Open
Publication Export
-
題名 程式弱點視覺化技術
Visualizing Web Application Vulnerabilities作者 董亦揚
Tung, Yi Yang貢獻者 郁方
Yu, Fang
董亦揚
Tung, Yi Yang關鍵詞 視覺化
網路安全
字串分析
程式理解
Visualization
Web security
String Analysis
Program Comprehension日期 2012 上傳時間 2-Sep-2013 16:01:32 (UTC+8) 摘要 網路應用程式在網際網路的發展中扮演了很重要的角色，並經常處理客戶敏感資料。但網路應用程式開發很容易產生漏洞，並導致網站容易受到駭客的攻擊。並取得網站的管理者存取權限，這是一個極其嚴重的問題。我們提出了一個新的線上服務，檢測網路應用程式中的漏洞，查看和修補。這項服務的後端是建立在一個基於網路應用程式原始碼的靜態字符串分析。我們檢測了數個 open source 的網站，並報告各種未知的漏洞及其修補的程式碼。
Web application security has become a critical issue as more and more personal and business applications have appeared in recent years. It is known that Web applications are vulnerable due to software defects. Open to public users, vulnerable Websites may experience malicious attacks from the Internet. We present a new Web-service platform with which system developers can detect and patch potential vulnerabilities of their Web applications online. Taking advantage of static string analysis techniques, our analysis ensures that the patched programs are free from vulnerabilities with respect to given attack patterns. Specifically, we integrate the service front end with program-visualization techniques, developing a 3D interface/presentation that allows users to access and view the analysis results in a visualization environment with the aim of improving users’ comprehension of programs, and especially of how vulnerabilities get exploited and patched. We report our analysis results on several open-source applications, finding and patching various previously unknown as well as known vulnerabilities.參考文獻 [1] Hamed Ahmadi and Jun Kong. User-centric adaptation of Web information for small screens. Journal of Visual Languages and Computing ,Vol.23, No.1,pages 13-28, 2012.[2] Johannes Bohnet and Jürgen Döllner. Visual exploration of function call graphs for feature location in complex software systems. In Proc. of the ACM 2006 Symposium on Software Visualization, SOFTVIS `06, pages 95-104, Brighton, UK, September 4-5, 2006.[3] Johannes Bohnet, Stefan Voigt, and Jürgen Döllner. Locating and understanding features of complex software systems by synchronizing time-, collaboration- and code-focused views on execution traces. In Proc. of the 16th IEEE International Conference on Program Comprehension, ICPC `08, pages 268-271, Amsterdam, The Netherlands, June 10-13, 2008.[4] Manuel Costa, Miguel Castro, Lidong Zhou, Lintao Zhang, and Marcus Peinado. Bouncer: securing software by blocking bad input. In Proc. of the 21st ACM Symposium on Operating Systems Principles, SOSP `07, pages 117-130, Stevenson, Washington, USA, October 14-17, 2007.[5] Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Precise analysis of string expressions. In Proc. of the 10th International Static Analysis Symposium, SAS `03, pages 1-18, San Diego, CA, USA, June 11-13, 2003.[6] Kunrong Chen and Vaclav Rajlich. RIPPLES: Tool for Change in Legacy Software. In Proc. of the IEEE International Conference on Software Maintenance, ICSM `01 pages 230-239, Florence, Italy, November 6-10, 2001.[7] Tsung-Hsiang Chang, Tom Yeh, and Rob Miller. Associating the visual representation of user interfaces with their internal structures and metadata. In Proc. of the 24th Annual ACM Symposium on User Interface Software and Technology, UIST `11, pages 245-256, Santa Barbara, CA, USA, October 16-19, 2011.[8] Pierre Dragicevic, Stéphane Huot, and Fanny Chevalier. Gliimpse:Animating from markup code to rendered documents and vice versa. In Proc. of the 24th annual ACMsymposium on User interface software and technology, UIST `11, pages 245-256, Santa Barbara, CA, USA, October 16-19, 2011.[9] Xiang Fu, Xin Lu, Boris Peltsverger, Shijun Chen, Kai Qian, and Lixin Tao. A static analysis framework for detecting sql injection vulnerabilities. In Proc. of the 31st Annual International Computer Software and Applications Conference, COMPSAC `07, pages 87-96, Beijing, China, , July 24-2, 2007.[10] gotoAndPlay(). Smartfoxserver @ONLINE, http://www.smartfoxserver.com/. Jan. 2013.[11] David Grove, Greg DeFouw, Jeffrey Dean ,and Craig Chambers. Call Graph Construction in Object-Oriented Languages. In Proc. of the 1997 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications, OOPSLA `97, pages 108-124, Atlanta, Georgia, USA, October 5-9, 1997. [12] Paul A. Gross and Caitlin Kelleher. Non-programmers identifying functionality in unfamiliar code: strategies and barriers. Journal of Visual Languages and Computing, Vol. 21 No. 5, pages263-276, December 2010.[13] Susan L. Graham, Peter B. Kessler, and Marshall K. McKusick. gprof: a call graph execution profiler. In Proc. of the SIGPLAN Symposium on Compiler Construction, SIGPLAN `82, pages 120-126, Boston, Massachusetts, USA, June 23-25, 1982.[14]Carl Gould, Zhendong Su and Premkumar Devanbu. Static checking of dynamically generated queries in database applications. In Proc. of the 26th International Conference on Software Engineering, ICSE `04, pages 645-654, Edinburgh, United Kingdom, May 23-28, 2004.[15] Paul A. Gross, Jennifer Yang, and Caitlin Kelleher. Dinah: an interface to assist non-programmers with selecting program code causing graphical output. In Proc. of the International Conference on Human Factors in Computing Systems, CHI `11, pages 3397-3400, Vancouver, BC, Canada, May 7-12, 2011.[16] Liviu Iftode, Cristian Borcea, Nishkam Ravi, Porlin Kang, and Peng Zhou. Smart phone: An embedded system for universal interactions. In Proc. of the 10th IEEE International Workshop on Future Trends of Distributed Computing Systems FTDCS `04, pages 88-94, Suzhou, China, May 26-28, 2004.[17] James A. Jones, Mary Jean Harrold and John Stasko. Visualization of test information to assist fault localization. In Proc. of the 24th International Conference on Software Engineering, ICSE `02, pages 467-477, New York, NY, USA, May 19-25, 2002.[18] Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer and Michael D. Ernst. Hampi: a solver for string constraints. In Proc. of the 18th International Symposium on Software Testing and Analysis ,ISSTA `09, pages 105-116, Chicago, IL, USA, July 19-23, 2009 [19] Thorsten Karrer, Jan-Peter Krämer, Jonathan Diehl, Björn Hartmann and Jan Borchers. Stacksplorer: call graph navigation helps increasing code maintenance efficiency. In Proc. of the 24th annual ACM symposium on User interface software and technology, UIST `11, pages 217-224, New York, NY, USA, October 16-19, 2011. [20] Kazimiras Lukoit, Norman Wilde, Scott Stowell, and Tim Hennessey. TraceGraph: Immediate Visual Location of Software Features. In Proc. International Conference on Software Maintenance, ICSM `00, pages 33-39, San Jose, California, USA, October 11-14, 2000.[21] Bonnie MacKay. The gateway: a navigation technique for migrating to small screens. In the Proc. of Extended abstracts of the 2003 Conference on Human Factors in Computing Systems ,CHI `03, pages 684-685, Ft. Lauderdale, Florida, USA, April 5-10, 2003.[22] Alessandro Orso, James A. Jones, Mary Jean Harrold, and John T. Stasko. Gammatella: Visualization of program-execution data for deployed software. In the Proc. of 26th International Conference on Software Engineering, ICSE `04, pages 699-700, Edinburgh, United Kingdom, May 23-28, 2004.[23] Karl J. Ottenstein and Linda M. Ottenstein. The Program Dependence Graph in a Software Development Environment. In Proc. of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, SDE `84, pages 177-184, Pittsburgh, Pennsylvania, USA, April 23-25, 1984.[24] Michael J. Pacione. Software visualization for object-oriented program comprehension. In Proc. of the 26th International Conference on Software Engineering, ICSE `04, pages 63-65, Edinburgh, United Kingdom, May 23-28, 2004.[25] Virpi Roto, Andrei Popescu, Antti Koivisto, and Elina Vartiainen.Minimap: a Web page visualization method for mobile phones. In the Proc. of the 2006 Conference on Human Factors in Computing Systems, CHI `06, pages 35-44, Montreal, Quebec, Canada, April 22-27, 2006.[26] Michael Risi and Giuseppe Scanniello. Metricattitude: a visualization tool for the reverse engineering of object oriented software. In the Proc. of International Working Conference on Advanced Visual Interfaces, AVI `12, pages 449-456, Capri Island, Naples, Italy, May 22-25 2012.[27] Nicolas Surribas. Wapiti @ONLINE,Jan. 2013.[28] Mavituna Security. Netsparker@ONLINE,Jan. 2013.[29] D. Shannon, S. Hajra, A. Lee, D. Zhan, and S. Khurshid. Abstracting symbolic execution with string analysis. In the Proc. of Testing: Academic and Industrial Conference Practice and Research Techniques-MUTATION, TAICPART-MUTATION `07, pages 13-22, Washington, DC, USA, September10-14 2007. [30] Tarja Systä, Kai Koskimies and Hausi A. Müller. Shimba -an environment for reverse engineering java software systems. Journal of Software: Practice and Experience, Vol.31 No.4, pages 371-394, 2001.[31] Unity Technologies. Unity documentation @ONLINE,Jan. 2013.[32] Stanford University. IPhone application development @ONLINE, Jan. 2013.[33] Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses. In Proc. of the 24th IEEE/ACM International Conference on Automated Software Engineering ASE `09, pages 605-609, Auckland, New Zealand, November 16-20, 2009.[34] Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Stranger: An automata-based string analysis tool for php. In Proc. of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS`10, pages 154-15, Paphos, Cyprus, March 20-28, 2010.[35] Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Patching vulnerabilities with sanitization synthesis. In Proc. of the 33rd International Conference on Software Engineering, ICSE `11, pages 251-260, Waikiki, Honolulu , HI, USA, May 21-28, 2011. [36] Fang Yu, Tevfik Bultan, Marco Cova, and Oscar H. Ibarra. Symbolic string verification: An automata-based approach. In Proc. of the 15th International SPIN Workshop on Model Checking Software, SPIN `08, pages 306-324 Los Angeles, CA, USA, August 10-12, 2008.[37] Fang Yu, Tevfik Bultan, and Ben Hardekopf. String abstractions for string verification. In Proc. of the 15th International SPIN Workshop on Model Checking Software, SPIN `11, pages 20-37, Snowbird, UT, USA, July 14-15, 2011.[38] Fang Yu, Tevfik Bultan, and Oscar H. Ibarra. Relational string verification using multi-track. In Proc. of the 15th International Conference on Implementation and Application of Automata, CIAA `10, pages 290-299, Winnipeg, MB, Canada, August 12-15, 2010. 描述 碩士
國立政治大學
資訊管理研究所
100356021
101資料來源 http://thesis.lib.nccu.edu.tw/record/#G0100356021 資料類型 thesis dc.contributor.advisor 郁方 zh_TW dc.contributor.advisor Yu, Fang en_US dc.contributor.author (Authors) 董亦揚 zh_TW dc.contributor.author (Authors) Tung, Yi Yang en_US dc.creator (作者) 董亦揚 zh_TW dc.creator (作者) Tung, Yi Yang en_US dc.date (日期) 2012 en_US dc.date.accessioned 2-Sep-2013 16:01:32 (UTC+8) - dc.date.available 2-Sep-2013 16:01:32 (UTC+8) - dc.date.issued (上傳時間) 2-Sep-2013 16:01:32 (UTC+8) - dc.identifier (Other Identifiers) G0100356021 en_US dc.identifier.uri (URI) http://nccur.lib.nccu.edu.tw/handle/140.119/59298 - dc.description (描述) 碩士 zh_TW dc.description (描述) 國立政治大學 zh_TW dc.description (描述) 資訊管理研究所 zh_TW dc.description (描述) 100356021 zh_TW dc.description (描述) 101 zh_TW dc.description.abstract (摘要) 網路應用程式在網際網路的發展中扮演了很重要的角色，並經常處理客戶敏感資料。但網路應用程式開發很容易產生漏洞，並導致網站容易受到駭客的攻擊。並取得網站的管理者存取權限，這是一個極其嚴重的問題。我們提出了一個新的線上服務，檢測網路應用程式中的漏洞，查看和修補。這項服務的後端是建立在一個基於網路應用程式原始碼的靜態字符串分析。我們檢測了數個 open source 的網站，並報告各種未知的漏洞及其修補的程式碼。 zh_TW dc.description.abstract (摘要) Web application security has become a critical issue as more and more personal and business applications have appeared in recent years. It is known that Web applications are vulnerable due to software defects. Open to public users, vulnerable Websites may experience malicious attacks from the Internet. We present a new Web-service platform with which system developers can detect and patch potential vulnerabilities of their Web applications online. Taking advantage of static string analysis techniques, our analysis ensures that the patched programs are free from vulnerabilities with respect to given attack patterns. Specifically, we integrate the service front end with program-visualization techniques, developing a 3D interface/presentation that allows users to access and view the analysis results in a visualization environment with the aim of improving users’ comprehension of programs, and especially of how vulnerabilities get exploited and patched. We report our analysis results on several open-source applications, finding and patching various previously unknown as well as known vulnerabilities. en_US dc.description.tableofcontents Abstract iCONTENTS iiList of Figures iiiList of Tables vCHAPTER 1 INTRODUCTION 11.1 Background and Motivation 11.2 Approach: Patching Vulnerabilities Online 11.3 Contribution 21.4 Content Organization 2CHAPTER 2 LITERATURE REVIEW 42.1 Content Presentation 42.2 Program Visualization 62.3 String Analysis and Vulnerability Detection 8CHAPTER 3 PATCHER: THE WEB SERVICE 113.1 Web Service 123.2 Architecture 12CHAPTER 4 VISUALIZATION 194.1 Software Comprehension 204.1.1 Program Visualization Design and Implementation 224.2 Graphic Visualization 294.2.1 Processing Graphic Inputs 324.2.2 Building Interactive Graphs 344.3 App: The Mobile Application on the Client Side 354.4 Integration of the Web Service, the Visualization Device, and the App 37CHAPTER 5 EVALUATION 41CHAPTER 6 CONCLUSION 456.1 Conclusion 456.2 Ongoing Work 45References 46 zh_TW dc.format.extent 2193419 bytes - dc.format.mimetype application/pdf - dc.language.iso en_US - dc.source.uri (資料來源) http://thesis.lib.nccu.edu.tw/record/#G0100356021 en_US dc.subject (關鍵詞) 視覺化 zh_TW dc.subject (關鍵詞) 網路安全 zh_TW dc.subject (關鍵詞) 字串分析 zh_TW dc.subject (關鍵詞) 程式理解 zh_TW dc.subject (關鍵詞) Visualization en_US dc.subject (關鍵詞) Web security en_US dc.subject (關鍵詞) String Analysis en_US dc.subject (關鍵詞) Program Comprehension en_US dc.title (題名) 程式弱點視覺化技術 zh_TW dc.title (題名) Visualizing Web Application Vulnerabilities en_US dc.type (資料類型) thesis en dc.relation.reference (參考文獻) [1] Hamed Ahmadi and Jun Kong. User-centric adaptation of Web information for small screens. Journal of Visual Languages and Computing ,Vol.23, No.1,pages 13-28, 2012.[2] Johannes Bohnet and Jürgen Döllner. Visual exploration of function call graphs for feature location in complex software systems. In Proc. of the ACM 2006 Symposium on Software Visualization, SOFTVIS `06, pages 95-104, Brighton, UK, September 4-5, 2006.[3] Johannes Bohnet, Stefan Voigt, and Jürgen Döllner. Locating and understanding features of complex software systems by synchronizing time-, collaboration- and code-focused views on execution traces. In Proc. of the 16th IEEE International Conference on Program Comprehension, ICPC `08, pages 268-271, Amsterdam, The Netherlands, June 10-13, 2008.[4] Manuel Costa, Miguel Castro, Lidong Zhou, Lintao Zhang, and Marcus Peinado. Bouncer: securing software by blocking bad input. In Proc. of the 21st ACM Symposium on Operating Systems Principles, SOSP `07, pages 117-130, Stevenson, Washington, USA, October 14-17, 2007.[5] Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Precise analysis of string expressions. In Proc. of the 10th International Static Analysis Symposium, SAS `03, pages 1-18, San Diego, CA, USA, June 11-13, 2003.[6] Kunrong Chen and Vaclav Rajlich. RIPPLES: Tool for Change in Legacy Software. In Proc. of the IEEE International Conference on Software Maintenance, ICSM `01 pages 230-239, Florence, Italy, November 6-10, 2001.[7] Tsung-Hsiang Chang, Tom Yeh, and Rob Miller. Associating the visual representation of user interfaces with their internal structures and metadata. In Proc. of the 24th Annual ACM Symposium on User Interface Software and Technology, UIST `11, pages 245-256, Santa Barbara, CA, USA, October 16-19, 2011.[8] Pierre Dragicevic, Stéphane Huot, and Fanny Chevalier. Gliimpse:Animating from markup code to rendered documents and vice versa. In Proc. of the 24th annual ACMsymposium on User interface software and technology, UIST `11, pages 245-256, Santa Barbara, CA, USA, October 16-19, 2011.[9] Xiang Fu, Xin Lu, Boris Peltsverger, Shijun Chen, Kai Qian, and Lixin Tao. A static analysis framework for detecting sql injection vulnerabilities. In Proc. of the 31st Annual International Computer Software and Applications Conference, COMPSAC `07, pages 87-96, Beijing, China, , July 24-2, 2007.[10] gotoAndPlay(). Smartfoxserver @ONLINE, http://www.smartfoxserver.com/. Jan. 2013.[11] David Grove, Greg DeFouw, Jeffrey Dean ,and Craig Chambers. Call Graph Construction in Object-Oriented Languages. In Proc. of the 1997 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications, OOPSLA `97, pages 108-124, Atlanta, Georgia, USA, October 5-9, 1997. [12] Paul A. Gross and Caitlin Kelleher. Non-programmers identifying functionality in unfamiliar code: strategies and barriers. Journal of Visual Languages and Computing, Vol. 21 No. 5, pages263-276, December 2010.[13] Susan L. Graham, Peter B. Kessler, and Marshall K. McKusick. gprof: a call graph execution profiler. In Proc. of the SIGPLAN Symposium on Compiler Construction, SIGPLAN `82, pages 120-126, Boston, Massachusetts, USA, June 23-25, 1982.[14]Carl Gould, Zhendong Su and Premkumar Devanbu. Static checking of dynamically generated queries in database applications. In Proc. of the 26th International Conference on Software Engineering, ICSE `04, pages 645-654, Edinburgh, United Kingdom, May 23-28, 2004.[15] Paul A. Gross, Jennifer Yang, and Caitlin Kelleher. Dinah: an interface to assist non-programmers with selecting program code causing graphical output. In Proc. of the International Conference on Human Factors in Computing Systems, CHI `11, pages 3397-3400, Vancouver, BC, Canada, May 7-12, 2011.[16] Liviu Iftode, Cristian Borcea, Nishkam Ravi, Porlin Kang, and Peng Zhou. Smart phone: An embedded system for universal interactions. In Proc. of the 10th IEEE International Workshop on Future Trends of Distributed Computing Systems FTDCS `04, pages 88-94, Suzhou, China, May 26-28, 2004.[17] James A. Jones, Mary Jean Harrold and John Stasko. Visualization of test information to assist fault localization. In Proc. of the 24th International Conference on Software Engineering, ICSE `02, pages 467-477, New York, NY, USA, May 19-25, 2002.[18] Adam Kiezun, Vijay Ganesh, Philip J. Guo, Pieter Hooimeijer and Michael D. Ernst. Hampi: a solver for string constraints. In Proc. of the 18th International Symposium on Software Testing and Analysis ,ISSTA `09, pages 105-116, Chicago, IL, USA, July 19-23, 2009 [19] Thorsten Karrer, Jan-Peter Krämer, Jonathan Diehl, Björn Hartmann and Jan Borchers. Stacksplorer: call graph navigation helps increasing code maintenance efficiency. In Proc. of the 24th annual ACM symposium on User interface software and technology, UIST `11, pages 217-224, New York, NY, USA, October 16-19, 2011. [20] Kazimiras Lukoit, Norman Wilde, Scott Stowell, and Tim Hennessey. TraceGraph: Immediate Visual Location of Software Features. In Proc. International Conference on Software Maintenance, ICSM `00, pages 33-39, San Jose, California, USA, October 11-14, 2000.[21] Bonnie MacKay. The gateway: a navigation technique for migrating to small screens. In the Proc. of Extended abstracts of the 2003 Conference on Human Factors in Computing Systems ,CHI `03, pages 684-685, Ft. Lauderdale, Florida, USA, April 5-10, 2003.[22] Alessandro Orso, James A. Jones, Mary Jean Harrold, and John T. Stasko. Gammatella: Visualization of program-execution data for deployed software. In the Proc. of 26th International Conference on Software Engineering, ICSE `04, pages 699-700, Edinburgh, United Kingdom, May 23-28, 2004.[23] Karl J. Ottenstein and Linda M. Ottenstein. The Program Dependence Graph in a Software Development Environment. In Proc. of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, SDE `84, pages 177-184, Pittsburgh, Pennsylvania, USA, April 23-25, 1984.[24] Michael J. Pacione. Software visualization for object-oriented program comprehension. In Proc. of the 26th International Conference on Software Engineering, ICSE `04, pages 63-65, Edinburgh, United Kingdom, May 23-28, 2004.[25] Virpi Roto, Andrei Popescu, Antti Koivisto, and Elina Vartiainen.Minimap: a Web page visualization method for mobile phones. In the Proc. of the 2006 Conference on Human Factors in Computing Systems, CHI `06, pages 35-44, Montreal, Quebec, Canada, April 22-27, 2006.[26] Michael Risi and Giuseppe Scanniello. Metricattitude: a visualization tool for the reverse engineering of object oriented software. In the Proc. of International Working Conference on Advanced Visual Interfaces, AVI `12, pages 449-456, Capri Island, Naples, Italy, May 22-25 2012.[27] Nicolas Surribas. Wapiti @ONLINE,Jan. 2013.[28] Mavituna Security. Netsparker@ONLINE,Jan. 2013.[29] D. Shannon, S. Hajra, A. Lee, D. Zhan, and S. Khurshid. Abstracting symbolic execution with string analysis. In the Proc. of Testing: Academic and Industrial Conference Practice and Research Techniques-MUTATION, TAICPART-MUTATION `07, pages 13-22, Washington, DC, USA, September10-14 2007. [30] Tarja Systä, Kai Koskimies and Hausi A. Müller. Shimba -an environment for reverse engineering java software systems. Journal of Software: Practice and Experience, Vol.31 No.4, pages 371-394, 2001.[31] Unity Technologies. Unity documentation @ONLINE,Jan. 2013.[32] Stanford University. IPhone application development @ONLINE, Jan. 2013.[33] Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses. In Proc. of the 24th IEEE/ACM International Conference on Automated Software Engineering ASE `09, pages 605-609, Auckland, New Zealand, November 16-20, 2009.[34] Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Stranger: An automata-based string analysis tool for php. In Proc. of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS`10, pages 154-15, Paphos, Cyprus, March 20-28, 2010.[35] Fang Yu, Muath Alkhalaf, and Tevfik Bultan. Patching vulnerabilities with sanitization synthesis. In Proc. of the 33rd International Conference on Software Engineering, ICSE `11, pages 251-260, Waikiki, Honolulu , HI, USA, May 21-28, 2011. [36] Fang Yu, Tevfik Bultan, Marco Cova, and Oscar H. Ibarra. Symbolic string verification: An automata-based approach. In Proc. of the 15th International SPIN Workshop on Model Checking Software, SPIN `08, pages 306-324 Los Angeles, CA, USA, August 10-12, 2008.[37] Fang Yu, Tevfik Bultan, and Ben Hardekopf. String abstractions for string verification. In Proc. of the 15th International SPIN Workshop on Model Checking Software, SPIN `11, pages 20-37, Snowbird, UT, USA, July 14-15, 2011.[38] Fang Yu, Tevfik Bultan, and Oscar H. Ibarra. Relational string verification using multi-track. In Proc. of the 15th International Conference on Implementation and Application of Automata, CIAA `10, pages 290-299, Winnipeg, MB, Canada, August 12-15, 2010. zh_TW
