research-article

Towards a program logic for JavaScript

Authors:

Philippa Anne Gardner,

Sergio Maffeis,

Gareth David SmithAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 1

Pages 31 - 44

https://doi.org/10.1145/2103621.2103663

Published: 25 January 2012 Publication History

Abstract

JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts. We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and "with". We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.

Supplementary Material

JPG File (popl_1a_3.jpg)

Download
13.77 KB

MP4 File (popl_1a_3.mp4)

Download
212.44 MB

References

[1]

C. Anderson, P. Giannini, and S. Drossopoulou. Towards type inference for JavaScript. In Proc. of ECOOP'05, 2005.

Digital Library

[2]

J. Berdine, C. Calcagno, and P. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, 2005.

Digital Library

[3]

J. Berdine, B. Cook, and S. Ishtiaq. Slayer: Memory safety for systems-level code. In CAV, 2011.

Digital Library

[4]

G.M. Bierman, M.J. Parkinson, and A. M. Pitts. MJ: An imperative core calculus for java and java with effects. Technical report, Cambridge, 2003.

[5]

L. Birkedal and H. Yang. Relational parametricity and separation logic. In FoSSaCS, pages 93--107, 2007.

Digital Library

[6]

N. Charlton. Hoare logic for higher order store using simple semantics. In Proc. of WOLLIC 2011, 2011.

Digital Library

[7]

T. Dinsdale-Young, M. Dodds, P. Gardner, M. Parkinson, and V. Vafeiadis. Concurrent abstract predicates. ECOOP, 2010.

Digital Library

[8]

D. Distefano and M. Parkinson. jStar: towards practical verification for Java. In OOPSLA '08, pages 213--226. ACM, 2008.

Digital Library

[9]

M. Dodds, X. Feng, M.J. Parkinson, and V. Vafeiadis. Deny-guarantee reasoning, 2009.

[10]

D. Dreyer, G. Neis, and L. Birkedal. The impact of higher-order state and control effects on local relational reasoning. In ICFP, pages 143--156, 2010.

Digital Library

[11]

P. Gardner, S. Maffeis, and G. Smith. Towards a program logic for JavaScript. Imperial College London Technical Report number DTR11--11, November 2011.

[12]

A. Guha, C. Saftoiu, and S. Krishnamurthi. The Essence of JavaScript. ECOOP 2010, pages 126--150, 2010.

Digital Library

[13]

D. Herman and C. Flanagan. Status report: specifying JavaScript with ML. In Proc. of ML'07, pages 47--52, 2007.

Digital Library

[14]

ECMA International. ECMAScript language specification. stardard ECMA-262, 3rd Edition, 1999.

[15]

jQuery: The write less, do more, JavaScript library. http://jquery.com.

[16]

S. Maffeis, J. C. Mitchell, and A. Taly. Isolating javascript with filters, rewriting, and wrappers. In ESORICS, pages 505--522, 2009.

Digital Library

[17]

S. Maffeis, J. C. Mitchell, and A. Taly. Object capabilities and isolation of untrusted web applications. In IEEE Symposium on Security and Privacy, pages 125--140, 2010.

Digital Library

[18]

S. Maffeis, J.C. Mitchell, and A. Taly. An operational semantics for JavaScript. In Proc. of APLAS'08, LNCS, 2008.

Digital Library

[19]

S. Maffeis and A. Taly. Language-based isolation of untrusted javascript. In CSF, pages 77--91, 2009.

Digital Library

[20]

P. O'Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In CSL, 2001.

[21]

P. W. OHearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1--3):271--307, 2007.

Digital Library

[22]

Changhee Park, Hongki Lee, and Sukyoung Ryu. An empirical study on the rewritability of the with statement in javascript. In FOOL, 2011.

[23]

M. Parkinson and G. M. Bierman. Separation logic, abstraction and inheritance. In POPL, 2008.

Digital Library

[24]

M. J. Parkinson. Local reasoning for Java. Technical Report 654, Univ. of Cambridge Computer Laboratory, 2005. Ph.D. dissertation.

[25]

Prototype Core Team. Prototype JavaScript framework: Easy Ajax and DOM manipulation for dynamic web applications. http://www.prototypejs.org.

[26]

Dave Raggett. W3C Slidy. http://www.w3.org/Talks/Tools/Slidy2/, 2005.

[27]

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. Accepted for publication at ECOOP 2011.

Digital Library

[28]

G. Richards, S. Lebresne, B. Burg, and J. Vitek. An analysis of the dynamic behavior of JavaScript programs. In PLDI, 2010.

Digital Library

[29]

J. Schwinghammer, L. Birkedal, B. Reus, and H. Yang. Nested hoare triples and frame rules for higher-order store. In In Proc. of CSL'09, 2009.

Digital Library

[30]

G. D. Smith. Local reasoning about web programs. PhD Thesis, Dep. of Computing, Imperial College London, 2011.

[31]

A. Taly, U. Erlingsson, M. S. Miller, J. C. Mitchell, and J. Nagra. Automated analysis of security-critical javascript apis. In Proc. of IEEE Security and Privacy '11. IEEE, 2011.

Digital Library

[32]

P. Thiemann. Towards a type system for analyzing javascript programs. In Proc. of ESOP '05, volume 3444 of LNCS, 2005.

Digital Library

[33]

P. Thiemann. A type safe DOM API. In Proc. of DBPL, pages 169--183, 2005.

Digital Library

[34]

V. Vafeiadis. Concurrent separation logic and operational semantics. In MFPS11, 2011.

Digital Library

[35]

Viktor Vafeiadis and M. Parkinson. A marriage of rely/guarantee and separation logic. In IN 18TH CONCUR. Springer, 2007.

Digital Library

[36]

H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. O'Hearn. Scalable shape analysis for systems code. In CAV, 2008.

Digital Library

[37]

D. Yu, A. Chander, N. Islam, and I. Serikov. JavaScript instrumentation for browser security. In Proc. of POPL'07, 2007.

Digital Library

Cited By

Schellhorn GBodenmüller SReif W(2023)Refinement and Separation: Modular Verification of Wandering TreesiFM 202310.1007/978-3-031-47705-8_12(214-234)Online publication date: 13-Nov-2023
https://dl.acm.org/doi/10.1007/978-3-031-47705-8_12
Raad ABerdine JDang HDreyer DO’Hearn PVillard J(2020)Local Reasoning About the Presence of Bugs: Incorrectness Separation LogicComputer Aided Verification10.1007/978-3-030-53291-8_14(225-252)Online publication date: 21-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-53291-8_14
Fragoso Santos JMaksimović PSampaio GGardner P(2019)JaVerT 2.0: compositional symbolic execution for JavaScriptProceedings of the ACM on Programming Languages10.1145/32903793:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290379
Show More Cited By

Index Terms

Towards a program logic for JavaScript
1. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Pre- and post-conditions

Recommendations

Towards a program logic for JavaScript
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe ...
Drupal 6 JavaScript and jQuery
Django JavaScript Integration: AJAX and jQuery

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 1

POPL '12

January 2012

569 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2103621

Issue’s Table of Contents

POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2012
602 pages
ISBN:9781450310833
DOI:10.1145/2103656
General Chair:
John Field
Google, USA
,
Program Chair:
Michael Hicks
University of Maryland, College Park, USA

Copyright © 2012 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 2012

Published in SIGPLAN Volume 47, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

76
Total Citations
View Citations
1,288
Total Downloads

Downloads (Last 12 months)49
Downloads (Last 6 weeks)6

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Schellhorn GBodenmüller SReif W(2023)Refinement and Separation: Modular Verification of Wandering TreesiFM 202310.1007/978-3-031-47705-8_12(214-234)Online publication date: 13-Nov-2023
https://dl.acm.org/doi/10.1007/978-3-031-47705-8_12
Raad ABerdine JDang HDreyer DO’Hearn PVillard J(2020)Local Reasoning About the Presence of Bugs: Incorrectness Separation LogicComputer Aided Verification10.1007/978-3-030-53291-8_14(225-252)Online publication date: 21-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-53291-8_14
Fragoso Santos JMaksimović PSampaio GGardner P(2019)JaVerT 2.0: compositional symbolic execution for JavaScriptProceedings of the ACM on Programming Languages10.1145/32903793:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290379
Cyphert JBreck JKincaid ZReps T(2019)Refinement of path expressions for static analysisProceedings of the ACM on Programming Languages10.1145/32903583:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290358
Bodin MGardner PJensen TSchmitt A(2019)Skeletal semantics and their interpretationsProceedings of the ACM on Programming Languages10.1145/32903573:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290357
Toman JGrossman D(2019)Concerto: a framework for combined concrete and abstract interpretationProceedings of the ACM on Programming Languages10.1145/32903563:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290356
Cousot PGiacobazzi RRanzato F(2019)A²I: abstract² interpretationProceedings of the ACM on Programming Languages10.1145/32903553:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290355
Singh GGehr TPüschel MVechev M(2019)An abstract domain for certifying neural networksProceedings of the ACM on Programming Languages10.1145/32903543:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290354
Alon UZilberstein MLevy OYahav E(2019)code2vec: learning distributed representations of codeProceedings of the ACM on Programming Languages10.1145/32903533:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290353
Cavallo EHarper R(2019)Higher inductive types in cubical computational type theoryProceedings of the ACM on Programming Languages10.1145/32903143:POPL(1-27)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290314
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 Issue’s Table of Contents