Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Book sections

Defensive JavaScript: Building and Verifying Secure Web Components

Abstract : Defensive JavaScript (DJS) is a typed subset of JavaScript that guarantees that the functional behavior of a program cannot be tampered with even if it is loaded by and executed within a malicious environment under the control of the attacker. As such, DJS is ideal for writing JavaScript security components, such as bookmarklets, single sign-on widgets, and cryptographic libraries, that may be loaded within untrusted web pages alongside unknown scripts from arbitrary third parties. We present a tutorial of the DJS language along with motivations for its design. We show how to program security components in DJS, how to verify their defensiveness using the DJS typechecker, and how to analyze their security properties automatically using ProVerif.
Document type :
Book sections
Complete list of metadata
Contributor : Bruno Blanchet Connect in order to contact the contributor
Submitted on : Friday, April 15, 2016 - 4:31:38 AM
Last modification on : Wednesday, April 6, 2022 - 3:48:25 PM
Long-term archiving on: : Tuesday, November 15, 2016 - 4:05:23 AM


Files produced by the author(s)




Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Sergio Maffeis. Defensive JavaScript: Building and Verifying Secure Web Components. Alessandro Aldini; Javier Lopez; Fabio Martinelli. Foundations of Security Analysis and Design VII, 8604, Springer, pp.88-123, 2014, Lecture Notes in Computer Science, 978-3-319-10081-4. ⟨10.1007/978-3-319-10082-1_4⟩. ⟨hal-01102144⟩



Record views


Files downloads