PI: Johannes Kinder, Royal Holloway, University of London
- Dynamic languages like JavaScript and Python are immensely popular.
- Dynamic types and non-standard semantics make security bugs difficult to spot.
- EASTEND focused on automated security testing for dynamic languages, in particular JavaScript.
- EASTEND improves the applicability of dynamic symbolic execution for JavaScript code and develops a flexible specification and testing methodology for security properties.
EASTEND is based on the hypothesis that inherently dynamic languages are best served by a dynamic approach to verification that points to errors in the code without restricting the freedom of the developer. It uses test generation via dynamic symbolic execution (DSE) to systematically cover paths through programs and check security properties along those paths. The two main research objectives of EASTEND were: improving the applicability of dynamic symbolic execution (DSE) for real-world JavaScript code (RO1); and developing a flexible specification and testing methodology for security properties that goes beyond simple assertion checking (RO2).
Regular expressions (REs) limit applicability of DSE to testing code security in practical client- and server-side web applications, as modern solvers cannot reason about real-world REs as used by developers. We developed an encoding of complex REs and with a refinement scheme that soundly translates REs into the subset supported by state-of-the-art solvers. We implemented our approach in our DSE engine for JavaScript, ExpoSE [1], and evaluated it on 1,131 Node.js packages, demonstrating that the encoding is effective and can increase line coverage by up to 30%, meaning that more parts of the program can be reached, increasing the analysis surface for detecting bugs/vulnerabilities, e.g., using the specification and testing methods developed as part of RO2.
We have developed a methodology for specification-based testing of cryptographic applications based on type-like tags attached to runtime values that we call “Security Annotations” (SAs) [2]. We have developed explicit SAs for the widely-used JavaScript library Crypto.JS, which implements common cryptographic algorithms and primitives. These will allow developers using Crypto.JS to automatically inject our annotations into their testing environment at runtime without any expert knowledge required. By using DSE with ExpoSE on a program using an appropriately annotated API, developers will be able automatically detect cryptographic bugs without additional annotation requirements. The code and data that resulted from the project can be found here.
PUBLICATIONS. [1] B. Loring, D. Mitchell, J. Kinder. “ExpoSE: Practical Symbolic Execution of Standalone JavaScript”. In Proc. Int. Symp. on Model Checking of Software (SPIN), pp. 196–199, ACM, 2017. [2] D. Mitchell, L. T. van Binsbergen, B. Loring, and J. Kinder. “Checking Cryptographic API Usage with Composable Annotations”. In ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM), 2018. [3] D. Mitchell, J. Kinder. “A Formal Model for Checking Cryptographic API Usage in JavaScript”. ESORICS (1) 2019: 341-360. [4] B. Loring, D. Mitchell, and J. Kinder. “Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript“. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), pp. 425–438, ACM, 2019.
IMPACT. “We have started using ExpoSE as a key component of a research project on privacy-preserving proxy servers. To the best of my knowledge, it is the only existing tool for dynamic symbolic execution of modern real-world JavaScript code.”– Prof. James Mickens, Harvard University –
