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 language | English |
|---|---|
| Title of host publication | ESORICS'19 |
| Subtitle of host publication | Proceedings of the 24th European Symposium on Research in Computer Security |
| Publisher | Springer |
| Pages | 341-360 |
| Number of pages | 20 |
| Volume | 11735 |
| ISBN (Electronic) | 978-3-030-29959-0 |
| ISBN (Print) | 978-3-030-29958-3 |
| DOIs | |
| Publication status | E-pub ahead of print - 15 Sept 2019 |
| Event | ESORICS'19: 24th European Symposium on Research in Computer Security - Parc Alvisse Hotel, Luxembourg City, Luxembourg Duration: 23 Sept 2019 → 27 Sept 2019 Conference number: 24 https://esorics2019.uni.lu |
Conference
| Conference | ESORICS'19 |
|---|---|
| Abbreviated title | ESORICS'19 |
| Country/Territory | Luxembourg |
| City | Luxembourg City |
| Period | 23/09/19 → 27/09/19 |
| Internet address |