| dc.contributor | 資管系 | en_US |
| dc.creator (作者) | 郁方;Tevfik Bultan;Oscar H. Ibarra | zh_TW |
| dc.date (日期) | 2011-05 | en_US |
| dc.date.accessioned | 6-Aug-2014 14:07:37 (UTC+8) | - |
| dc.date.available | 6-Aug-2014 14:07:37 (UTC+8) | - |
| dc.date.issued (上傳時間) | 6-Aug-2014 14:07:37 (UTC+8) | - |
| dc.identifier.uri (URI) | http://nccur.lib.nccu.edu.tw/handle/140.119/68333 | - |
| dc.description.abstract (摘要) | Verification of string manipulation operations is a crucial problem in computer security. In this paper, we present a new relational string verification technique based on multi-track automata. Our approach is capable of verifying properties that depend on relations among string variables. This enables us to prove that vulnerabilities that result from improper string manipulation do not exist in a given program. Our main contributions in this paper can be summarized as follows: (1) We formally characterize the string verification problem as the reachability analysis of string systems and show decidability/undecidability results for several string analysis problems. (2) We develop a sound symbolic analysis technique for string verification that over-approximates the reachable states of a given string system using multi-track automata and summarization. (3) We evaluate the presented techniques with respect to several string analysis benchmarks extracted from real web applications. | en_US |
| dc.format.extent | 114275 bytes | - |
| dc.format.mimetype | application/pdf | - |
| dc.language.iso | en_US | - |
| dc.relation (關聯) | International Journal of Foundations of Computer Science, 22(8), 1909-1924 | en_US |
| dc.subject (關鍵詞) | String analysis; verification; multi-track automata; word equation; security | en_US |
| dc.title (題名) | Relational String Verification Using Multi-track Automata | en_US |
| dc.type (資料類型) | article | en |
| dc.identifier.doi (DOI) | 10.1142/S0129054111009112 | en_US |
| dc.doi.uri (DOI) | http://dx.doi.org/10.1142/S0129054111009112 | en_US |
