A Formal Model for Checking Cryptographic API Usage in JavaScript. / Mitchell, Duncan; Kinder, Johannes.

ESORICS'19: Proceedings of the 24th European Symposium on Research in Computer Security. Vol. 11735 Springer, 2019. p. 341-360.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

E-pub ahead of print



Modern JavaScript implementations include APIs offering strong cryptography, but it is easy for non-expert developers to misuse them and introduce potentially critical security bugs. In this paper, we formalize a mechanism to rule out such bugs through runtime enforcement of cryptographic API specifications. In particular, we construct a dynamic variant of Security Annotations, which represent security properties of values via type-like information. We formalize Security Annotations within an existing JavaScript semantics and mechanize it to obtain a reference interpreter for JavaScript with embedded Security Annotations. We provide a specification for a fragment of the W3C WebCrypto standard and demonstrate how this specification can reveal security vulnerabilities in JavaScript code with the help of a case study. We define a notion of safety with respect to Security Annotations and extend this to security guarantees for individual programs.
Original languageEnglish
Title of host publicationESORICS'19
Subtitle of host publicationProceedings of the 24th European Symposium on Research in Computer Security
Number of pages20
ISBN (Electronic)978-3-030-29959-0
ISBN (Print)978-3-030-29958-3
Publication statusE-pub ahead of print - 15 Sep 2019
EventESORICS'19: 24th European Symposium on Research in Computer Security - Parc Alvisse Hotel, Luxembourg City, Luxembourg
Duration: 23 Sep 201927 Sep 2019
Conference number: 24


Abbreviated titleESORICS'19
CityLuxembourg City
Internet address
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 34218110