@inproceedings{,
    author = {Mitchell, Duncan; Kinder, Johannes},
    title = {A Formal Model for Checking Cryptographic API Usage in JavaScript},
    editor = {Sako, Kazue; Schneider, Steve; Ryan, Peter Y. A.},
    booktitle = {Computer Security – ESORICS 2019 : 24th European Symposium on Research in Computer Security, Luxembourg, September 23–27, 2019, Proceedings, Part I},
    series = {Lecture Notes in Computer Science},
    journal = {},
    address = {Cham},
    publisher = {Springer},
    edition = {},
    year = {2019},
    isbn = {978-3-030-29958-3 ; 978-3-030-29959-0},
    volume = {11735},
    number =  {},
    pages = {341-360},
    url = {https://doi.org/10.1007/978-3-030-29959-0_17},
    doi = {10.1007/978-3-030-29959-0_17},
    keywords = {},
    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.},
    note = {},
    institution = {Universität der Bundeswehr München, Fakultät für Informatik, INF 6 - Institut für Systemsicherheit, Professur: Kinder, Johannes},
    
    
}