Gradual Typing Embedded Securely in JavaScript

Abstract : JavaScript's flexible semantics makes writing correct code hard and writing secure code extremely difficult. To address the former problem, various forms of gradual typing have been proposed, such as Closure and TypeScript. However, supporting all common programming idioms is not easy; for example, TypeScript deliberately gives up type soundness for programming convenience. In this paper, we propose a gradual type system and implementation techniques that provide important safety and security guarantees. We present TS*, a gradual type system and source-to-source compiler for JavaScript. In contrast to prior gradual type systems, TS* features full runtime reflection over three kinds of types: (1) simple types for higher-order functions, recursive datatypes and dictionary-based extensible records; (2) the type any, for dynamically type-safe TS* expressions; and (3) the type un, for untrusted, potentially malicious JavaScript contexts in which TS* is embedded. After type-checking, the compiler instruments the program with various checks to ensure the type safety of TS* despite its interactions with arbitrary JavaScript contexts, which are free to use eval, stack walks, prototype customizations, and other offensive features. The proof of our main theorem employs a form of type-preserving compilation, wherein we prove all the runtime invariants of the translation of TS* to JavaScript by showing that translated programs are well-typed in JS*, a previously proposed dependently typed language for proving functional correctness of JavaScript programs. We describe a prototype compiler, a secure runtime, and sample applications for TS*. Our examples illustrate how web security patterns that developers currently program in JavaScript (with much difficulty and still with dubious results) can instead be programmed naturally in TS*, retaining a flavor of idiomatic JavaScript, while providing strong safety guarantees by virtue of typing.
Type de document :
Communication dans un congrès
POPL 2014 - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, CA, United States. ACM, pp.425-437, 2014, 〈10.1145/2535838.2535889〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00940836
Contributeur : Ben Smyth <>
Soumis le : lundi 3 février 2014 - 09:21:16
Dernière modification le : mardi 17 avril 2018 - 11:23:45

Lien texte intégral

Identifiants

Collections

Citation

Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, et al.. Gradual Typing Embedded Securely in JavaScript. POPL 2014 - 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2014, San Diego, CA, United States. ACM, pp.425-437, 2014, 〈10.1145/2535838.2535889〉. 〈hal-00940836〉

Partager

Métriques

Consultations de la notice

708