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

Standard

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

Harvard

Mitchell, D & Kinder, J 2019, A Formal Model for Checking Cryptographic API Usage in JavaScript. in ESORICS'19: Proceedings of the 24th European Symposium on Research in Computer Security. vol. 11735, Springer, pp. 341-360, ESORICS'19, Luxembourg City, Luxembourg, 23/09/19. https://doi.org/10.1007/978-3-030-29959-0_17

APA

Mitchell, D., & Kinder, J. (2019). A Formal Model for Checking Cryptographic API Usage in JavaScript. In ESORICS'19: Proceedings of the 24th European Symposium on Research in Computer Security (Vol. 11735, pp. 341-360). Springer. https://doi.org/10.1007/978-3-030-29959-0_17

Vancouver

Mitchell D, Kinder J. A Formal Model for Checking Cryptographic API Usage in JavaScript. In ESORICS'19: Proceedings of the 24th European Symposium on Research in Computer Security. Vol. 11735. Springer. 2019. p. 341-360 https://doi.org/10.1007/978-3-030-29959-0_17

Author

Mitchell, Duncan ; Kinder, Johannes. / A Formal Model for Checking Cryptographic API Usage in JavaScript. ESORICS'19: Proceedings of the 24th European Symposium on Research in Computer Security. Vol. 11735 Springer, 2019. pp. 341-360

BibTeX

@inproceedings{166aa057c02547bba9167e6b27385d62,
title = "A Formal Model for Checking Cryptographic API Usage in JavaScript",
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.",
author = "Duncan Mitchell and Johannes Kinder",
year = "2019",
month = sep,
day = "15",
doi = "10.1007/978-3-030-29959-0_17",
language = "English",
isbn = "978-3-030-29958-3",
volume = "11735",
pages = "341--360",
booktitle = "ESORICS'19",
publisher = "Springer",
note = "ESORICS'19 : 24th European Symposium on Research in Computer Security, ESORICS'19 ; Conference date: 23-09-2019 Through 27-09-2019",
url = "https://esorics2019.uni.lu",

}

RIS

TY - GEN

T1 - A Formal Model for Checking Cryptographic API Usage in JavaScript

AU - Mitchell, Duncan

AU - Kinder, Johannes

N1 - Conference code: 24

PY - 2019/9/15

Y1 - 2019/9/15

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-29959-0_17

DO - 10.1007/978-3-030-29959-0_17

M3 - Conference contribution

SN - 978-3-030-29958-3

VL - 11735

SP - 341

EP - 360

BT - ESORICS'19

PB - Springer

T2 - ESORICS'19

Y2 - 23 September 2019 through 27 September 2019

ER -