Defensive JavaScript: Building and Verifying Secure Web Components

Karthikeyan Bhargavan 1 Antoine Delignat-Lavaud 1 Sergio Maffeis 2
1 PROSECCO - Programming securely with cryptography
Inria Paris-Rocquencourt
2 Department of Computing [London]
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.
Type de document :
Chapitre d'ouvrage
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〉
Liste complète des métadonnées
https://hal.inria.fr/hal-01102144
Contributeur : Bruno Blanchet <>
Soumis le : vendredi 15 avril 2016 - 04:31:38
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mardi 15 novembre 2016 - 04:05:23

Fichier

djs-tutorial.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA

Citation

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

160

Téléchargements de fichiers

146

Contact


archive-ouverte@inria.fr