Starting Date: Summer 2017
Prerequisites: 2nd year
Will results be assigned to University:
Dynamic symbolic execution (DSE) is an effective tool for bug detection in real software. Like unit testing and fuzzing DSE executes portions of a program, exposing bugs through runtime program exceptions. In DSE, some inputs to the program under test are made “symbolic” while the rest are fixed. Whenever the symbolic execution encounters a conditional operation depending on symbolic inputs, it uses a constraint solver to derive inputs that would drive down execution on either side. In principle, this allows to fully automatically generate test cases covering all possible paths in a program.
Some external functions are opaque to DSE, however, and it is unable to derive their effects on symbolic variables. To allow successful exploration of programs using external functions (which can involve standard library functions for input / output / string processing, etc.), one must declare equivalent models, which are simplified versions of the library functions focusing on possible return values and effects on arguments. Each additional model increases the effectiveness of DSE.
In this project, you will be helping to improve bug finding and code coverage of ExpoSE, Royal Holloway’s in-house DSE engine for JavaScript. ExpoSE has been developed to find bugs and security vulnerabilities in JavaScript programs and has shown promising initial results, successfully exploring several popular JavaScript libraries. Your role will be to improve ExpoSE’s program coverage. This will involve executing ExpoSE on a selection of real JavaScript applications and then using the results to develop or refine models so that ExpoSE can generate more test cases thereby exploring more of a program.
You should be comfortable working on Linux (preferred) or Mac OS X. Prior JavaScript experience very desirable, C/C++ knowledge and some knowledge (or at least curiosity) about the inner workings of compilers/interpreters a plus.