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. Springer, 2019.

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

Forthcoming

Documents

  • Accepted Manuscript

    Accepted author manuscript, 497 KB, PDF-document

Abstract

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
PublisherSpringer
Publication statusAccepted/In press - 9 Jul 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
https://esorics2019.uni.lu

Conference

ConferenceESORICS'19
Abbreviated titleESORICS'19
CountryLuxembourg
CityLuxembourg City
Period23/09/1927/09/19
Internet address

ID: 34218110