String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report)

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F20%3APU143338" target="_blank" >RIV/00216305:26230/20:PU143338 - isvavai.cz</a>

Result on the web

<a href="https://arxiv.org/abs/2010.15975" target="_blank" >https://arxiv.org/abs/2010.15975</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report)

Original language description

String analysis is the problem of reasoning about how strings are manipulated by a program. It has numerous applications including automatic detection of cross-site scripting (XSS). A popular string analysis technique includes symbolic executions, which at their core use string (constraint) solvers. Such solvers typically reason about constraints expressed in theories over strings with the concatenation operator as an atomic constraint. In recent years, researchers started to recognise the importance of incorporating the replace-all operator and finite transductions in the theories of strings with concatenation. Such string operations are typically crucial for reasoning about XSS vulnerabilities in web applications, especially for modelling sanitisation functions and implicit browser transductions (e.g. innerHTML). In this paper, we provide the first string solver that can reason about constraints involving both concatenation and finite transductions. Moreover, it has a completeness and t

Czech name

—

Czech description

—

Type

O - Miscellaneous

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2020

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů