Here are some of the documents that were produced as part of my project:
My name is Daniel Connor and I am a 4th year student at IT Carlow studying Software Development.
The source code is available on github.
In writing JSSeek we set out to see whether it would be possible to build a symbolic execution engine for javascript that would find statements where errors can occur. We highlighted that the most common type of error in Javascript is the type error which is thrown when an operation is performed on a variable whose type does not support the operation. This happens because Javascript is a dynamically typed language and variables can contain any of the 6 different types in Javascript.
There are many approaches to patching Javascript and some of the problems it has. Some of those being TypeScript and GWT, which both attempt to bring some kind of static typing to Javascript by adding features to the language. They are then compiled to Javascript so that it can be run in the browser. While JSSeek sets out to solve a similar problem, it does it in a different way.
JSSeek uses symbolic execution which is the execution of code using symbolic inputs rather than real world ones. As a result of Javascript being dynamically typed, it is very hard to do symbolic execution. One of the benefits of using symbolic execution is that it is possible to create a specification for a function which defines the input and return types, then because JSSeek covers all paths in a function we can easily tell all of the return types that are possible. This is useful because a developer can then be sure that the function will always return a specific type such as in a statically typed language while still having the benefits of dynamic typing.
There are a some other tools that use symbolic execution to find security vulnerabilities or errors in Javascript[5, 6], however the majority of them limit the types of inputs to a subset of all Javascript types. Kudzu[6], which uses symbolic execution to find security vulnerabilities, allows strings integers and booleans as inputs but does not allow for symbolic objects. It mostly focuses on string inputs. Rozzle[5] also uses symbolic execution to find security vulnerabilities but instead of using symbolic inputs uses a tree of possible concrete values.
Another benefit of symbolic execution is that it is possible to create a specification for a function which defines the input and return types, then because JSSeek covers all paths in a function we can easily tell all of the return types that can be returned. This is useful because a developer can then be sure that the function will always return a specific type such as in a statically typed language while still having the benefits of dynamic typing.
Other tools use random testing, which proves to be quite effective seeing as errors are mostly type errors and are caused by null or undefined values. As a result a lot of errors can be found by just using null or undefined as input values. Random testing is not very good however where there are more complex constraints in a function or if complex objects are required as inputs. In these situations a guided approach such as symbolic execution is more useful.
At the moment Javascript is the only language supported by the major browsers, as a result, to help solve some of the problems with Javascript is to create a new superset or completely different language that compiles to Javascript. Now many changes are coming to Javascript as part of upcoming standards that solve a lot of the problems that developers complain about in the language. These changes involve introducing classes and block scoping for example. Javascript will however remain a dynamically typed language. This means that even though classes will be introduced, the properties of any object can still be changed, and variables will function in the same way as before. As a result JSSeek would be an important tool even in the foreseeable future of Javascript.
JSSeek was built as part of my final year project.