EASTEND: Efficient Automatic Security Testing for Dynamic Languages

The two main objectives of EASTEND are improving the applicability of dynamic symbolic execution for JavaScript code and developing 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.

A range of methods are available to statically verify implementations of security properties; however, despite efforts to formalise the JavaScript language specification, verification of general

JavaScript applications is still out of reach. Python is lacking even a rigorous specification in natural language: the Python Language Reference openly states that “if you […] tried to re-implement Python from this document alone, you might […] end up implementing quite a different language.” And even if a complete formal specification were available, typical dynamic language features such as heavy use of reflection, eval and ad-hoc polymorphism pose substantial challenges to static verification. For instance, JavaScript functions will often check dynamically for undefined arguments to determine the number of parameters they were invoked with and perform different computations based on the outcome. Consequently, approaches that rely on applying static type systems to JavaScript have to restrict the language or encode complex predicates to distinguish types.

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.

Blake Loring, Duncan Mitchell, and Johannes Kinder. ExpoSE: Practical Symbolic Execution of Standalone JavaScript. In Proc. Int. SPIN Symp. Model Checking of Software (SPIN), pp. 196–199, ACM, 2017

Researcher: Johannes Kinder, Royal Holloway, University of London