Martin Bodin
Skip Abstract Section
Skip Supplemental Material SectionAbstract
JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties.
We present JSCert, a formalisation of the current ECMA standard in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We give a Coq proof that JSRef is correct with respect to JSCert and assess JSRef using test262, the ECMA conformance test suite. Our methodology ensures that JSCert is a comparatively accurate formulation of the English standard, which will only improve as time goes on. We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript.
Supplemental Material
- J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in weak memory models. In Proc. CAV: 22nd International Conference on Computer Aided Verification, LNCS 6174, pages 258--272, 2010. Google Scholar
Digital Library
- C. Anderson, P. Giannini, and S. Drossopoulou. Towards type inference for JavaScript. In ECOOP'05, pages 428--452. Springer, 2005. Google ScholarDigital Library
- A. W. Appel. Verified software toolchain - (invited talk). In ESOP, pages 1--17, 2011. Google ScholarDigital Library
- M. Batty, S. Owens, S. Sarkar, P. Sewell, and T.Weber. Mathematizing C++ concurrency. In POPL, pages 55--66, 2011. Google ScholarDigital Library
- M. Batty, M. Dodds, and A. Gotsman. Library abstraction for C/C++ concurrency. In POPL, 2013. Google ScholarDigital Library
- K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis. Language-based defenses against untrusted browser origins. In USENIX Security Symposium, 2013. Google ScholarDigital Library
- S. Bishop, M. Fairbairn, M. Norrish, P. Sewell, M. Smith, and K. Wansbrough. Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. In POPL, pages 55--66, 2006. Google ScholarDigital Library
- S. Blazy and X. Leroy. Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning, 43(3):263--288, 2009.Google ScholarCross Ref
- E. Börger, N. G. Fruja, V. Gervasi, and R. F. Stärk. A high-level modular definition of the semantics of C#. Theor. Comput. Sci., 336 (2-3):235--284, 2005. Google ScholarDigital Library
- C11. ISO/IEC 9899:2011. http://www.iso.org/iso/iso_catalogue/catalogue_tc/catalogue_detail.htm?csnumber=57853, 2011.Google Scholar
- A. Charguéraud. Pretty-big-step semantics. In ESOP, pages 41--60, 2013. Google ScholarDigital Library
- R. Chugh and R. Jhala. Dependent types for JavaScript. CoRR, abs/1112.4106, 2011.Google Scholar
- R. Chugh, J. A. Meister, R. Jhala, and S. Lerner. Staged information flow for JavaScript. In PLDI'09, pages 50--62. ACM, 2009. Google ScholarDigital Library
- X. Clerc. Bisect. http://bisect.x9c.fr/, 2012.Google Scholar
- Compcert Team. Compcert. http://compcert.inria.fr/, 2013.Google Scholar
- D. Crockford. ADSafe: Making JavaScript safe for advertising. http://adsafe.org/, 2007.Google Scholar
- S. Drossopoulou and S. Eisenbach. Is the Java type system sound? In FOOL4, 1997.Google Scholar
- ECMA International. Test262. http://test262.ecmascript.org/, 2010.Google Scholar
- C. Ellison and G. Rosu. An executable formal semantics of C with applications. In POPL, pages 533--544, 2012. Google ScholarDigital Library
- A. Farzan, F. Chen, J. Meseguer, and G. Rosu. Formal analysis of Java programs in JavaFAN. In CAV, pages 501--505, 2004.Google Scholar
- C. Fournet, N. Swamy, J. Chen, P.-É. Dagand, P.-Y. Strub, and B. Livshits. Fully abstract compilation to JavaScript. In POPL, pages 371--384, 2013. Google ScholarDigital Library
- Free Software Foundation. C language testsuites: "C-torture" version 4.4.2. http://gcc.gnu.org/onlinedocs/gccint/C-Tests.html, 2010.Google Scholar
- D. Fugate. Test262 bug 56. https://bugs.ecmascript.org/show_bug.cgi?id=56, 2011.Google Scholar
- P. Gardner, S. Maffeis, and G. D. Smith. Towards a program logic for JavaScript. In POPL'12, pages 31--44. ACM, 2012. Google ScholarDigital Library
- Google Inc. The Closure Compiler. https://developers.google.com/closure/compiler/, 2009.Google Scholar
- S. Guarnieri and V. B. Livshits. GATEKEEPER: Mostly static enforcement of security and reliability policies for JavaScript code. In USENIX Security Symposium, pages 151--168, 2009. Google ScholarDigital Library
- S. Guarnieri, M. Pistoia, O. Tripp, J. Dolby, S. Teilhet, and R. Berg. Saving the world wide web from vulnerable JavaScript. In ISSTA, pages 177--187, 2011. Google ScholarDigital Library
- A. Guha, C. Saftoiu, and S. Krishnamurthi. The essence of JavaScript. ECOOP 2010, pages 126--150, 2010. Google ScholarDigital Library
- Y. Gurevich. Evolving algebras. In IFIP Congress (1), pages 423--427, 1994.Google Scholar
- D. Hedin and A. Sabelfeld. Information-flow security for a core of JavaScript. In CSF'12, pages 3--18. IEEE, 2012. Google ScholarDigital Library
- D. Herman and C. Flanagan. Status report: specifying JavaScript with ML. In ML, pages 47--52, 2007. Google ScholarDigital Library
- D. Jang and K. Choe. Points-to analysis for JavaScript. Proc. of SAC'09, page 1930, 2009. Google ScholarDigital Library
- S. H. Jensen, A. Møller, and P. Thiemann. Type analysis for JavaScript. In SAS '09. Springer, 2009. Google ScholarDigital Library
- D. K. Lee, K. Crary, and R. Harper. Towards a mechanized metatheory of Standard ML. In POPL, pages 173--184, 2007. Google ScholarDigital Library
- S. Maffeis and A. Taly. Language-based isolation of untrusted JavaScript. In CSF'09. IEEE, 2009. Google ScholarDigital Library
- S. Maffeis, J. Mitchell, and A. Taly. ECMA 262-3 operational semantics. http://jssec.net/semantics/, 2007.Google Scholar
- S. Maffeis, J. Mitchell, and A. Taly. An operational semantics for JavaScript. In APLAS'08, pages 307--325. Springer, 2008. Google ScholarDigital Library
- S. Maffeis, J. Mitchell, and A. Taly. Isolating JavaScript with filters, rewriting, and wrappers. In ESORICS'09. Springer, 2009. Google ScholarDigital Library
- S. Maffeis, J. C. Mitchell, and A. Taly. Object capabilities and isolation of untrusted web applications. In Security and Privacy (SP), pages 125--140. IEEE, 2010. Google ScholarDigital Library
- G. Melquiond. Floats for Coq 2.1.0. http://flocq.gforge.inria.fr/, 2012.Google Scholar
- R. Milner, M. Tofte, and D. Macqueen. The Definition of Standard ML. MIT Press, Cambridge, MA, USA, 1997. ISBN 0262631814. Google ScholarDigital Library
- Mozilla. Mozilla automated JavaScript tests. https://developer.mozilla.org/en-US/docs/SpiderMonkey/Running_Automated_JavaScript_Tests, 2013.Google Scholar
- T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. Google ScholarDigital Library
- M. Norrish. Formalising C in HOL. PhD thesis, Computer Lab., University of Cambridge, 1998.Google Scholar
- D. S. P. Phung and A. Chudnov. Lightweight self protecting JavaScript. In ASIACCS 2009. ACM Press, 2009. Google ScholarDigital Library
- C. Park, H. Lee, and S. Ryu. An empirical study on the rewritability of the with statement in JavaScript. In FOOL, 2011.Google Scholar
- C. Park, H. Lee, and S. Ryu. SAFE: Formal specification and implementation of a scalable analysis framewrok for ECMAscript. In FOOL, 2012.Google Scholar
- F. Pfenning and C. Schürmann. System description: Twelf - a metalogical framework for deductive systems. In CADE, pages 202--206, 1999. Google ScholarDigital Library
- J. G. Politz, S. A. Eliopoulos, A. Guha, and S. Krishnamurthi. ADsafety: Type-based verification of JavaScript sandboxing. In USENIX Security Symposium, 2011. Google ScholarDigital Library
- J. G. Politz, M. J. Carroll, B. S. Lerner, J. Pombrio, and S. Krishnamurthi. A tested semantics for getters, setters, and eval in JavaScript. SIGPLAN Not., 48(2):1--16, Oct. 2012. Google ScholarDigital Library
- J. G. Politz, B. S. Lerner, H. Q. de la Vallee, T. Nelson, A. Guha, M. Carroll, and S. Krishnamurthi. Mechanized λJS. http://blog.brownplt.org/2012/06/04/lambdajs-coq.html, 2012.Google Scholar
- G. Richards, C. Hammer, B. Burg, and J. Vitek. The eval that men do - A large-scale study of the use of eval in JavaScript applications. In ECOOP'11, pages 52--78. Springer, 2011. Google ScholarDigital Library
- G. Roşu and T. F. Şerbǎnuţǎ. An overview of the K semantic framework. Journal of Logic and Algebraic Programming, 79(6):397--434, 2010.Google ScholarCross Ref
- T. Schneidereit. Convert some array extras to self-hosted js implementations. https://hg.mozilla.org/mozilla-central/rev/5593cd83590e, 2012.Google Scholar
- P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge, S. Sarkar, and R. Strnisa. Ott: Effective tool support for the working semanticist. J. Funct. Program., 20(1):71--122, 2010. Google ScholarDigital Library
- D. Syme. Proving Java type soundness. In Formal Syntax and Semantics of Java, pages 83--118, 1999. Google ScholarDigital Library
- A. Taly, Ú. Erlingsson, J. C. Mitchell, M. S. Miller, and J. Nagra. Automated analysis of security-critical JavaScript APIs. In IEEE Symposium on Security and Privacy, pages 363--378, 2011. Google ScholarDigital Library
- The JSCert Team. Mozilla Bug 862771, V8 Issue 2529, ES6 Bugs 1442-1444, Test262 Bug 1445, 1450, 1600. https://bugzilla.mozilla.org/show_bug.cgi?id=862771, http://code.google.com/p/v8/issues/detail?id=2529, https://bugs.ecmascript.org/show_bug.cgi?id={1442-1445,1450,1600}, 2013.Google Scholar
- P. Thiemann. Towards a type system for analyzing JavaScript programs. In ESOP'05, pages 140--140. Springer, 2005. Google ScholarDigital Library
- Various developers. Bugs in ES6, Test262 and browsers. https://bugs.webkit.org/show_bug.cgi?id={38970,104309} http://code.google.com/p/v8/issues/detail?id={705,2446} https://bugzilla.mozilla.org/show_bug.cgi?id=819125, 2010--2012.Google Scholar
- J. Ševčík, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, and P. Sewell. Relaxed-memory concurrency and verified compilation. In Proc. POPL, 2011. Google ScholarDigital Library
Index Terms
- A trusted mechanised JavaScript specification
Recommendations
A trusted mechanised JavaScript specification
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesJavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a ...
Towards Mechanised Semantics of HPC: The BSP with Subgroup Synchronisation Case
Proceedings of the ICA3PP International Workshops and Symposiums on Algorithms and Architectures for Parallel Processing - Volume 9532The underlying objective of this article is to exhibit the problems that might be encountered when working on a mechanised semantics of an hpc language. We take for instance a language to program bsp algorithms with subgroup synchronisation í la mpi. We ...
Formal specification of a JavaScript module system
OOPSLA '12: Proceedings of the ACM international conference on Object oriented programming systems languages and applicationsThe JavaScript programming language, originally developed as a simple scripting language, is now the language of choice for web applications. All the top 100 sites on the web use JavaScript and its use outside web pages is rapidly growing. However, ...
Comments