research-article

Towards a program logic for JavaScript

Authors:

Philippa Anne Gardner,

Sergio Maffeis,

Gareth David SmithAuthors Info & Claims

POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 31 - 44

https://doi.org/10.1145/2103656.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

Vanilla OYu JAbdalla H(2024)Cesno: The Initial Design of a New Programming Language8th International Conference on Computing, Control and Industrial Engineering (CCIE2024)10.1007/978-981-97-6937-7_17(128-146)Online publication date: 22-Sep-2024
https://doi.org/10.1007/978-981-97-6937-7_17
Maksimović PAyoun SSantos JGardner P(2021)Gillian, Part II: Real-World Verification for JavaScript and CComputer Aided Verification10.1007/978-3-030-81688-9_38(827-850)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_38
Bodin MDiaz TTanter É(2020)A trustworthy mechanized formalization of RACM SIGPLAN Notices10.1145/3393673.327694653:8(13-24)Online publication date: 6-Apr-2020
https://dl.acm.org/doi/10.1145/3393673.3276946
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

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
JavaScript: Moving to ES2015

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

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

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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 2012

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '12

Sponsor:

SIGPLAN

POPL '12: The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 25 - 27, 2012

PA, Philadelphia, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

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 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Vanilla OYu JAbdalla H(2024)Cesno: The Initial Design of a New Programming Language8th International Conference on Computing, Control and Industrial Engineering (CCIE2024)10.1007/978-981-97-6937-7_17(128-146)Online publication date: 22-Sep-2024
https://doi.org/10.1007/978-981-97-6937-7_17
Maksimović PAyoun SSantos JGardner P(2021)Gillian, Part II: Real-World Verification for JavaScript and CComputer Aided Verification10.1007/978-3-030-81688-9_38(827-850)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_38
Bodin MDiaz TTanter É(2020)A trustworthy mechanized formalization of RACM SIGPLAN Notices10.1145/3393673.327694653:8(13-24)Online publication date: 6-Apr-2020
https://dl.acm.org/doi/10.1145/3393673.3276946
Brown FRenner JNötzli ALerner SShacham HStefan DDonaldson ATorlak E(2020)Towards a verified range analysis for JavaScript JITsProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3385968(135-150)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3385968
van Ginkel NDe Groef WMassacci FPiessens FTolomei G(2019)A Server-Side JavaScript Security Architecture for Secure Integration of Third-Party LibrariesSecurity and Communication Networks10.1155/2019/96290342019Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.1155/2019/9629034
Wang SCao QMohan AHobor A(2019)Certifying graph-manipulating C programs via localizations within data structuresProceedings of the ACM on Programming Languages10.1145/33605973:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360597
Miltner AGulwani SLe VLeung ARadhakrishna ASoares GTiwari AUdupa A(2019)On the fly synthesis of edit suggestionsProceedings of the ACM on Programming Languages10.1145/33605693:OOPSLA(1-29)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360569
Chen JWei JFeng YBastani ODillig I(2019)Relational verification using reinforcement learningProceedings of the ACM on Programming Languages10.1145/33605673:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360567
Stein BNielsen BChang BMøller A(2019)Static analysis with demand-driven value refinementProceedings of the ACM on Programming Languages10.1145/33605663:OOPSLA(1-29)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360566
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

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