Before we can symbolically execute JavaScript we need a way to invoke an SMT solver directly from JavaScript, however we found that there is almost no existing language support for Node.js. To remedy this we developed Z3JavaScript, an NPM-installable set of bindings to the popular SMT solver Z3. In addition to a set of primitive bindings we provide a set of wrapper classes to simplify usage from JavaScript. We also provide a regular expression rewriter which allows for reasoning about regular expressions, capture groups, and backreferences in programs.

The tool is open source and is available here

Tags: projects Created On: 2018-08-09 17:09:57

© Blake Loring 2018