EASTEND: Efficient Automatic Security Testing for Dynamic Languages

Sponsored by the UK Research Institute in Verified Trustworthy Software Systems and the Royal Holloway Centre for Doctoral Training in Cyber Security.

The project sought to prove that an inherently dynamic language is best served by a dynamic approach to verification. We therefore chose to use test generation by dynamic symbolic execution (DSE) to systematically cover paths through programs and check security properties along those paths. While this prevents generating proofs, it ensures that all paths executed are feasible with respect to the execution environment. The two main lines of work were to improve DSE for real-world JavaScript code and to develop a flexible specification methodology for security properties.

JavaScript Symbolic Execution

ExpoSE, the open source DSE engine for JavaScript that we developed as part of the project, is able to automatically generate test cases for most Node.js programs without modifications. The main challenge faced by ExpoSE is that it needs to reason about the effects of the rich JavaScript semantics, including its vast standard library. In particular, most JavaScript programs process strings in some form and often rely on regular expressions, which are often a limiting factor for any kind of automated analysis.

In this project, we devised the first complete strategy to automatically reason about JavaScript regular expressions. We encoded the semantics of regular expression operations using string constraints and classical regular expressions and we devised a refinement scheme to address the problem of matching precedence and greediness: regular expressions will consume as many input characters as possible, from left to right. This constraint has so far been ignored in related work and existing solvers for regular expressions.

Our survey of over 400,000 JavaScript packages from the NPM software repository shows that one fifth makes use of complex regular expressions features. We implemented our encoding and refinement scheme in ExpoSE and evaluated it on 1,131 Node.js packages, demonstrating that the encoding is effective and can increase line coverage by up to 30%. We used line coverage here as a proxy metric for the effectiveness of the encoding: it demonstrates that more parts of the program can be reached, increasing the analysis surface for detecting bugs and vulnerabilities. We describe the encoding, refinement, and evaluation in an article published at PLDI 2019. ExpoSE is available on GitHub.

JavaScript Security Annotations

Several security-relevant properties, such as data provenance or integrity, cannot be written as assertions in JavaScript itself. We therefore developed an approach to attach additional security annotations to a language. This lightweight metatheory of security annotations allows tests to encode properties not present in the program state. We demonstrated the consistency of our system in a statically typed lambda calculus (published at PEPM 2018) and then followed up with a fully dynamic reference implementation for JavaScript. We specified a partial fragment of the WebCrypto API in terms of Security Annotations and demonstrated how to use it to detect security vulnerabilities. .

Software

ExpoSE Dynamic Symbolic Execution Engine for JavaScript [ GitHub ]

Reference Interpreter for Security Annotations [ GitHub ]

Publications

@inproceedings{esorics19-secannjs,
  author    = {Duncan Mitchell and Johannes Kinder},
  title     = {A Formal Model for Checking Cryptographic API Usage in JavaScript},
  booktitle = {Proc. European Symposium on Research in Computer Security (ESORICS)},
  series    = {LNCS},
  volume    = {11735},
  pages     = {341--360},
  year      = {2019},
  publisher = {Springer},
  doi       = {10.1007/978-3-030-29959-0\_17},
  rate      = {19.5},
}

@inproceedings{pldi19-regex,
  author    = {Blake Loring and Duncan Mitchell and Johannes Kinder},
  title     = {Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript},
  booktitle = {Proc. ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI)},
  pages     = {425--438},
  publisher = {ACM},
  year      = {2019},
  doi       = {10.1145/3314221.3314645},
}

@techreport{regex-arxiv,
  author      = {Blake Loring and Duncan Mitchell and Johannes Kinder},
  title       = {Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript},
  institution = {arXiv},
  number      = {CoRR:abs/1810.05661},
  year        = {2018},
  url         = {https://arxiv.org/abs/1810.05661},
}

@inproceedings{pepm18-security-annotations,
  author    = {Duncan Mitchell and L. Thomas van Binsbergen and Blake Loring and Johannes Kinder},
  title     = {Checking Cryptographic {API} Usage with Composable Annotations},
  booktitle = {ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM)},
  year      = {2018},
  doi       = {10.1145/3162071},
  rate      = {50},
}

@inproceedings{spin17-expose,
  author    = {Blake Loring and Duncan Mitchell and Johannes Kinder},
  title     = {{ExpoSE}: Practical Symbolic Execution of Standalone {JavaScript}},
  booktitle = {Proc. Int. SPIN Symp. Model Checking of Software (SPIN)},
  pages     = {196--199},
  publisher = {ACM},
  year      = {2017},
  rate      = {47},
}