String solving with word equations and transducers: towards a logic for analysing mutation XSS
We study the fundamental issue of decidability of satisfiability over string logics with concatenations and finite-state transducers as atomic operations. Although restricting to one type of operations yields decidability, little is known about the decidability of their combined theory, which is esp...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Published: |
Association for Computing Machinery
2016
|
| _version_ | 1826259429859786752 |
|---|---|
| author | Lin, A Barceló, P |
| author_facet | Lin, A Barceló, P |
| author_sort | Lin, A |
| collection | OXFORD |
| description | We study the fundamental issue of decidability of satisfiability over string logics with concatenations and finite-state transducers as atomic operations. Although restricting to one type of operations yields decidability, little is known about the decidability of their combined theory, which is especially relevant when analysing security vulnerabilities of dynamic web pages in a more realistic browser model. On the one hand, word equations (string logic with concatenations) cannot precisely capture sanitisation functions (e.g. htmlescape) and implicit browser transductions (e.g. innerHTML mutations). On the other hand, transducers suffer from the reverse problem of being able to model sanitisation functions and browser transductions, but not string concatenations. Naively combining word equations and transducers easily leads to an undecidable logic. Our main contribution is to show that the "straight-line fragment" of the logic is decidable (complexity ranges from PSPACE to EXPSPACE). The fragment can express the program logics of straight-line string-manipulating programs with concatenations and transductions as atomic operations, which arise when performing bounded model checking or dynamic symbolic executions. We demonstrate that the logic can naturally express constraints required for analysing mutation XSS in web applications. Finally, the logic remains decidable in the presence of length, letter-counting, regular, indexOf, and disequality constraints. |
| first_indexed | 2024-03-06T18:49:44Z |
| format | Conference item |
| id | oxford-uuid:0fd0b793-bdf5-4fa3-8e36-4e9144e4025e |
| institution | University of Oxford |
| last_indexed | 2024-03-06T18:49:44Z |
| publishDate | 2016 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:0fd0b793-bdf5-4fa3-8e36-4e9144e4025e2022-03-26T09:53:02ZString solving with word equations and transducers: towards a logic for analysing mutation XSSConference itemhttp://purl.org/coar/resource_type/c_5794uuid:0fd0b793-bdf5-4fa3-8e36-4e9144e4025eSymplectic Elements at OxfordAssociation for Computing Machinery2016Lin, ABarceló, PWe study the fundamental issue of decidability of satisfiability over string logics with concatenations and finite-state transducers as atomic operations. Although restricting to one type of operations yields decidability, little is known about the decidability of their combined theory, which is especially relevant when analysing security vulnerabilities of dynamic web pages in a more realistic browser model. On the one hand, word equations (string logic with concatenations) cannot precisely capture sanitisation functions (e.g. htmlescape) and implicit browser transductions (e.g. innerHTML mutations). On the other hand, transducers suffer from the reverse problem of being able to model sanitisation functions and browser transductions, but not string concatenations. Naively combining word equations and transducers easily leads to an undecidable logic. Our main contribution is to show that the "straight-line fragment" of the logic is decidable (complexity ranges from PSPACE to EXPSPACE). The fragment can express the program logics of straight-line string-manipulating programs with concatenations and transductions as atomic operations, which arise when performing bounded model checking or dynamic symbolic executions. We demonstrate that the logic can naturally express constraints required for analysing mutation XSS in web applications. Finally, the logic remains decidable in the presence of length, letter-counting, regular, indexOf, and disequality constraints. |
| spellingShingle | Lin, A Barceló, P String solving with word equations and transducers: towards a logic for analysing mutation XSS |
| title | String solving with word equations and transducers: towards a logic for analysing mutation XSS |
| title_full | String solving with word equations and transducers: towards a logic for analysing mutation XSS |
| title_fullStr | String solving with word equations and transducers: towards a logic for analysing mutation XSS |
| title_full_unstemmed | String solving with word equations and transducers: towards a logic for analysing mutation XSS |
| title_short | String solving with word equations and transducers: towards a logic for analysing mutation XSS |
| title_sort | string solving with word equations and transducers towards a logic for analysing mutation xss |
| work_keys_str_mv | AT lina stringsolvingwithwordequationsandtransducerstowardsalogicforanalysingmutationxss AT barcelop stringsolvingwithwordequationsandtransducerstowardsalogicforanalysingmutationxss |