A Formal Model for Checking Cryptographic API Usage in JavaScript

Duncan Mitchell, Johannes Kinder

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

151 Downloads (Pure)


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 Sept 2019
EventESORICS'19: 24th European Symposium on Research in Computer Security - Parc Alvisse Hotel, Luxembourg City, Luxembourg
Duration: 23 Sept 201927 Sept 2019
Conference number: 24


Abbreviated titleESORICS'19
CityLuxembourg City
Internet address

Cite this