The grant aims to improve the applicability of dynamic symbolic execution for JavaScript code and develop a flexible specification and testing methodology for security properties.

So-called dynamic languages like JavaScript and Python are immensely popular and are frequently cited as making programming accessible to a much broader audience. From origins as mostly toy languages these evolved to become essential building blocks of the modern IT infrastructure. Dynamic languages drive complex client applications, web frameworks, cloud infrastructure, and embedded devices, often handling security-sensitive data and even implementing cryptographic protocols. However, dynamic types and the often surprising semantics of languages like JavaScript make it difficult to spot subtle security bugs as long as they do not directly impact functionality.

Our main research hypothesis is that an inherently dynamic language is best served by a dynamic approach to verification that points to errors in the code without restricting the freedom of the developer. In this project, we will use test generation by dynamic symbolic execution (DSE) to systematically cover paths through programs and check security properties along those paths. On one hand, this means that we will not obtain any proofs over the entire program unless DSE terminates; on the other hand, all paths executed are guaranteed to be real (feasible) paths with respect to the execution environment. We see this project as an initial phase in a longer effort, to be continued in a follow-up project as part of VeTSS. We will initially focus on JavaScript as our target dynamic language, but are aiming to eventually generalise our work to other languages.

The Research Institute on Verified Trustworthy Software Systems (VeTSS) is a UK Academic Research Institute in Cyber Security at Imperial College London that is funded by the Engineering and Physical Sciences Research Council.