research-article

KJS: a complete formal semantics of JavaScript

Authors:

Andrei Stefănescu,

Grigore RoşuAuthors Info & Claims

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 346 - 356

https://doi.org/10.1145/2737924.2737991

Published: 03 June 2015 Publication History

Abstract

This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the existing implementations of JavaScript, only Chrome V8's passes all the tests, and no other semantics passes more than 90%. In addition to a reference implementation for JavaScript, KJS also yields a simple coverage metric for a test suite: the set of semantic rules it exercises. Our semantics revealed that the ECMAScript 5.1 conformance test suite fails to cover several semantic rules. Guided by the semantics, we wrote tests to exercise those rules. The new tests revealed bugs both in production JavaScript engines (Chrome V8, Safari WebKit, Firefox SpiderMonkey) and in other semantics. KJS is symbolically executable, thus it can be used for formal analysis and verification of JavaScript programs. We verified non-trivial programs and found a known security vulnerability.

References

[1]

E. Arvidsson. V8 Issue 2243. https://code.google.com/p/v8/ issues/detail?id=2243, 2012. Accessed: April 22, 2015.

[2]

S. Bandhakavi, S. T. King, P. Madhusudan, and M. Winslett. VEX: Vetting Browser Extensions for Security Vulnerabilities. In USENIX Security, pages 22–22. USENIX, 2010.

Digital Library

[3]

M. Bodin, A. Chargueraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, and G. Smith. A Trusted Mechanised JavaScript Specification. In POPL, pages 87–100. ACM, 2014.

Digital Library

[4]

D. Bogdanas and G. Rosu. K-Java: A Complete Semantics of Java. In POPL, pages 445–456. ACM, 2015.

Digital Library

[5]

D. Bruant. ECMAScript Bug 56. https://bugs.ecmascript.org/ show_bug.cgi?id=56#c3, 2011. Accessed: April 22, 2015.

[6]

D. Bruant. Mozilla Bug 641214. https://bugzilla.mozilla. org/show_bug.cgi?id=641214, 2011. Accessed: April 22, 2015.

[7]

M. Chevalier-Boisvert, E. Lavoie, M. Feeley, and B. Dufour. Bootstrapping a Self-hosted Research Virtual Machine for JavaScript: An Experience Report. In Proceedings of the 7th Symposium on Dynamic Languages, pages 61–72. ACM, 2011.

Digital Library

[8]

D. Crockford. JavaScript: The Good Parts. O’Reilly Media, 2008.

Digital Library

[9]

L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In TACAS, volume 4963, pages 337–340. LNCS, 2008.

Digital Library

[10]

Ecma TC39. ECMAScript Harmony. https://mail.mozilla.org/ pipermail/es-discuss/2008-August/003400.html, 2008. Accessed: April 22, 2015.

[11]

Ecma TC39. Standard ECMA-262 ECMAScript Language Specification Edition 5.1, June 2011.

[12]

Ecma TC39. Draft Specification of ECMA-262 6th Edition. http://wiki.ecmascript.org/doku.php?id=harmony: specification_drafts, 2014. Accessed: April 22, 2015.

[13]

Ecma TC39. TC39 Meeting Minutes. https://github.com/ rwaldron/tc39-notes/blob/master/es6/2014-09/sept-23. md#somehow-we-started-talking-about-test262, 2014.

[14]

Accessed: April 22, 2015.

[15]

Ecma TC39. Test262: ECMAScript Language Conformance Test Suite. http://test262.ecmascript.org, 2014. Accessed: April 22, 2015.

[16]

C. Ellison and G. Rosu. An Executable Formal Semantics of C with Applications. In POPL, pages 533–544. ACM, 2012.

Digital Library

[17]

D. Filaretti and S. Maffeis. An Executable Formal Semantics of PHP. In ECOOP, volume 8586, pages 567–592. LNCS, 2014.

[18]

C. Fournet, N. Swamy, J. Chen, P.-E. Dagand, P.-Y. Strub, and B. Livshits. Fully Abstract Compilation to JavaScript. In POPL, pages 371–384. ACM, 2013.

Digital Library

[19]

P. A. Gardner, S. Maffeis, and G. D. Smith. Towards a Program Logic for JavaScript. In POPL, pages 31–44. ACM, 2012.

Digital Library

[20]

S. Ghosh, D. Elenius, W. Li, P. Lincoln, N. Shankar, and W. Steiner. Automatically Extracting Requirements Specifications from Natural Language. CoRR, abs/1403.3142, 2014.

[21]

S. Guarnieri and B. Livshits. GATEKEEPER: Mostly Static Enforcement of Security and Reliability Policies for Javascript Code. In USENIX Security, pages 151–168. USENIX, 2009.

Digital Library

[22]

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. ACM, 2011.

Digital Library

[23]

A. Guha, S. Krishnamurthi, and T. Jim. Using Static Analysis for Ajax Intrusion Detection. In WWW, pages 561–570. ACM, 2009.

Digital Library

[24]

A. Guha, C. Saftoiu, and S. Krishnamurthi. The Essence of Javascript. In ECOOP, volume 6183, pages 126–150. LNCS, 2010.

Digital Library

[25]

D. Guth. A Formal Semantics of Python 3.3. Master’s thesis, University of Illinois at Urbana-Champaign, July 2013.

[26]

D. Herman and C. Flanagan. Status Report: Specifying Javascript with ML. In Proceedings of the 2007 Workshop on Workshop on ML, pages 47–52. ACM, 2007.

Digital Library

[27]

D. Herman, L. Wagner, and A. Zakai. asm.js. http://asmjs.org, 2014. Accessed: April 22, 2015.

[28]

V. Kashyap, K. Dewey, E. A. Kuefner, J. Wagner, K. Gibbons, J. Sarracino, B. Wiedermann, and B. Hardekopf. JSAI: A Static Analysis Platform for JavaScript. In FSE, pages 121–132. ACM, 2014.

Digital Library

[29]

H. Lee, S. Won, J. Jin, J. Cho, and S. Ryu. SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript. In Proceedings of the 2012 International Workshop on Foundations of Object-Oriented Languages. ACM, 2012.

[30]

S. Maffeis, J. C. Mitchell, and A. Taly. An Operational Semantics for JavaScript. In APLAS, volume 5356, pages 307–325. LNCS, 2008.

Digital Library

[31]

Mean.io. MEAN: A Fullstack Javascript Framework. http://mean. io/, 2014. Accessed: April 22, 2015.

[32]

J. Meseguer. Conditional Rewriting Logic as a Unified Model of Concurrency. Theoretical Computer Science, 96(1):73–155, 1992.

Digital Library

[33]

M. Nordio, C. Calcagno, and C. A. Furia. Javanni: A Verifier for JavaScript. In Fundamental Approaches to Software Engineering, volume 7793, pages 231–234. LNCS, 2013.

Digital Library

[34]

J. Orendorff. Mozilla Bug 779682. https://bugzilla.mozilla. org/show_bug.cgi?id=779682, 2012. Accessed: April 22, 2015.

[35]

D. Park. WebKit Bug 138859, 138858; V8 Issue 3704; ECMA-262 Bug 3427, 3426; S5 Issues 55, 57, 59. https://bugs.webkit.org/show_bug.cgi?id=138859, https://bugs.webkit.org/show_bug.cgi?id=138858, https://code.google.com/p/v8/issues/detail?id=3704, https://bugs.ecmascript.org/show_bug.cgi?id=3427, https://bugs.ecmascript.org/show_bug.cgi?id=3426, https://github.com/brownplt/LambdaS5/issues/55, https://github.com/brownplt/LambdaS5/issues/57, https://github.com/brownplt/LambdaS5/issues/59, 2014.

[36]

Accessed: April 22, 2015.

[37]

D. Park and A. Stefanescu. Supplementary material. https:// github.com/kframework/javascript-semantics, 2014.

[38]

Accessed: April 22, 2015.

[39]

J. G. Politz, S. A. Eliopoulos, A. Guha, and S. Krishnamurthi. ADsafety: Type-based Verification of JavaScript Sandboxing. In USENIX Security, pages 12–12. USENIX, 2011.

Digital Library

[40]

J. G. Politz, M. J. Carroll, B. S. Lerner, J. Pombrio, and S. Krishnamurthi. A Tested Semantics for Getters, Setters, and Eval in JavaScript. In Proceedings of the 8th Symposium on Dynamic Languages, pages 1–16. ACM, 2012.

Digital Library

[41]

J. Regehr, Y. Chen, P. Cuoq, E. Eide, C. Ellison, and X. Yang. Test-case Reduction for C Compiler Bugs. In PLDI, pages 335–346. ACM, 2012.

Digital Library

[42]

G. Rosu and T. F. Serbanuta. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming, 79(6): 397–434, 2010.

[43]

G. Rosu and A. Stefanescu. Checking Reachability Using Matching Logic. In OOPSLA, pages 555–574. ACM, 2012.

Digital Library

[44]

M. Samuel. Properties of Interpreters or the Browser Environment that allow Privilege Escalation. https://code.google.com/p/ google-caja/wiki/AttackVectors, 2009. Accessed: April 22, 2015.

[45]

M. Samuel. Attack Vectors: Global Object Poisoning. https://code. google.com/p/google-caja/wiki/GlobalObjectPoisoning, 2009. Accessed: April 22, 2015.

[46]

T. F. Serbanuta, A. Arusoaie, D. Lazar, C. Ellison, D. Lucanu, and G. Rosu. The K Primer (version 3.3). In Proceedings of the Second International Workshop on the K Framework and its Applications, volume 304, pages 57–80. ENTCS, 2013.

[47]

G. Smith. ECMA-262 Bug 1444. https://bugs.ecmascript.org/ show_bug.cgi?id=1444, 2013. Accessed: April 22, 2015.

[48]

A. Taly, U. Erlingsson, J. C. Mitchell, M. S. Miller, and J. Nagra. Automated Analysis of Security-Critical JavaScript APIs. In S&P (Oakland), pages 363––378. IEEE, 2011.

Digital Library

[49]

A. Zakai. Emscripten: An LLVM-to-JavaScript Compiler. In SPLASH, pages 301–312. ACM, 2011.

Digital Library

Cited By

Bevilacqua JChiodini LMoreno Santos IHauswirth M(2024)Assessing the Understanding of Expressions: A Qualitative Study of Notional-Machine-Based Exam QuestionsProceedings of the 24th Koli Calling International Conference on Computing Education Research10.1145/3699538.3699554(1-12)Online publication date: 12-Nov-2024
https://dl.acm.org/doi/10.1145/3699538.3699554
De Santo NBarrière APit-Claudel C(2024)A Coq Mechanization of JavaScript Regular Expression SemanticsProceedings of the ACM on Programming Languages10.1145/36746668:ICFP(1003-1031)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674666
Youn DShin WLee JRyu SBreitner JGardner PLindley SPretnar MRao XWatt CRossberg A(2024)Bringing the WebAssembly Standard up to Speed with SpecTecProceedings of the ACM on Programming Languages10.1145/36564408:PLDI(1559-1584)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656440
Show More Cited By

Index Terms

KJS: a complete formal semantics of JavaScript
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

K-Java: A Complete Semantics of Java
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

This paper presents K-Java, a complete executable formal semantics of Java 1.4. K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology. In order to maintain clarity while ...
KJS: a complete formal semantics of JavaScript
PLDI '15

This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the ...
Mutode: generic JavaScript and Node.js mutation testing tool
ISSTA 2018: Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis

Mutation testing is a technique in which faults (mutants) are injected into a program or application to assess its test suite effectiveness. It works by inserting mutants and running the application’s test suite to identify if the mutants are detected (...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2015

630 pages

ISBN:9781450334686

DOI:10.1145/2737924

General Chair:
David Grove
IBM Research, USA
,
Program Chair:
Steve Blackburn
Australian National University, Australia

ACM SIGPLAN Notices Volume 50, Issue 6
PLDI '15
June 2015
630 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2813885
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 June 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

PLDI '15

Sponsor:

SIGPLAN

PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 13 - 17, 2015

OR, Portland, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

83
Total Citations
View Citations
1,040
Total Downloads

Downloads (Last 12 months)98
Downloads (Last 6 weeks)9

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bevilacqua JChiodini LMoreno Santos IHauswirth M(2024)Assessing the Understanding of Expressions: A Qualitative Study of Notional-Machine-Based Exam QuestionsProceedings of the 24th Koli Calling International Conference on Computing Education Research10.1145/3699538.3699554(1-12)Online publication date: 12-Nov-2024
https://dl.acm.org/doi/10.1145/3699538.3699554
De Santo NBarrière APit-Claudel C(2024)A Coq Mechanization of JavaScript Regular Expression SemanticsProceedings of the ACM on Programming Languages10.1145/36746668:ICFP(1003-1031)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674666
Youn DShin WLee JRyu SBreitner JGardner PLindley SPretnar MRao XWatt CRossberg A(2024)Bringing the WebAssembly Standard up to Speed with SpecTecProceedings of the ACM on Programming Languages10.1145/36564408:PLDI(1559-1584)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656440
Zhao CWang YWang DSun GMeng B(2024)A Language-independent Quantitative Analysis Method on Conformance between Legal Contract and Smart ContractDistributed Ledger Technologies: Research and Practice10.1145/36536793:3(1-17)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3653679
Gauthier LPrevosto VSignoles JFuria CLopes APlat NGnesi S(2024)A Semantics of Structures, Unions, and Underspecified Terms for Formal SpecificationProceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE)10.1145/3644033.3644380(100-110)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3644033.3644380
Ryu SPark J(2024)JavaScript Language Design and Implementation in TandemCommunications of the ACM10.1145/362472367:5(86-95)Online publication date: 1-May-2024
https://dl.acm.org/doi/10.1145/3624723
Lee JBae K(2024)Formal Semantics and Analysis of Multitask PLC ST Programs with PreemptionFormal Methods10.1007/978-3-031-71162-6_22(425-442)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_22
Park JYoun DLee KRyu S(2023)Feature-Sensitive Coverage for Conformance Testing of Programming Language ImplementationsProceedings of the ACM on Programming Languages10.1145/35912407:PLDI(493-515)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591240
Watt CTrela MLammich PMärkl F(2023)WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssemblyProceedings of the ACM on Programming Languages10.1145/35912247:PLDI(100-123)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591224
Lin ZChen XTrinh MWang JRoşu G(2023)Generating Proof Certificates for a Language-Agnostic Deductive Program VerifierProceedings of the ACM on Programming Languages10.1145/35860297:OOPSLA1(56-84)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586029
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents