How a Symbolic Evaluator Generates Test Input for this Example

Question

Say we have some complicated function that determines if a string matches an XSS attack string, and throws an error or does something else in that case.

function somethingWithXSSVulnerability(x) {
  var regex = /<script(.*)>(.*)<\/script>/
  if (x.match(regex)) {
    throw new Error('XSS')
  } else {
    return x
  }
}

In trying to understand symbolic evaluation in regards to test generation, I am wondering how it would generate a test for this case. How it would generate an x such that it matched the regex. It could be a lot more complicated than a regex, a grammar for example. The test case generating the error would be something like:

// yes case
somethingWithXSSVulnerability('<script>alert("foo")</script>')
// no case
somethingWithXSSVulnerability('anything else even <script> w/o closing tags')

To really test it, it might need to generate an alert or try setting a cookie or something, so there it is becoming even more complicated.

But I am trying to get a sense of how the symbolic evaluator generates a test for this case. How it determines the value of the input to the function. It seems like it would have to understand the structure of the regex, then reverse-engineer an input to match it. Wondering if that is so.

Answer 1

Tools that solve problems like this often use a SMT (Satisfiability Modulo Theories) solver. This a SAT solver combined with a "theory solver" that can understand operations in some domain.

For example, constraints involving = and != can be decided using union find; constraints involving < on numbers can be decided using the simplex algorithm.

Operations on strings are trickier. Searching "regex string constraint" on Google Scholar finds many papers discussing approaches.

The abstract of this survey papers gives a very brief preview From An Evaluation of Automata Algorithms for String Analysis but notes there is no consensus on a single algorithm (emphasis mine):

https://doi.org/10.1007/978-3-642-18275-4_18

There has been significant recent interest in automated reasoning techniques, in particular constraint solvers, for string variables. These techniques support a wide variety of clients, ranging from static analysis to automated testing. The majority of string constraint solvers rely on finite automata to support regular expression constraints. For these approaches, performance depends critically on fast automata operations such as intersection, complementation, and determinization. Existing work in this area has not yet provided conclusive results as to which core algorithms and data structures work best in practice.

It seems the best way to algorithmically process regexes is to operate on the NFAs/DFAs that they represent, and, judging by the number of papers on it, there are effective algorithms for making the required decisions.

HAMPI seems to be an important early paper describing how this can be done, which is provided online by one of the authors: https://homes.cs.washington.edu/~mernst/pubs/string-solver-tr004.pdf