A trusted infrastructure for symbolic analysis of event-driven web applications
File(s) LIPIcs-ECOOP-2020-28.pdf (1.72 MB)
Published version
Author(s)
Sampaio, Gabriela
Fragoso Santos, Jose
Maksimovic, Petar
Gardner, Philippa
Type
Conference Paper
Abstract
We introduce a trusted infrastructure for the symbolic analysis of modern event-driven Web applica-tions. This infrastructure consists of reference implementations of the DOM Core Level 1, DOM UIEvents, JavaScript Promises and the JavaScriptasync/awaitAPIs, all underpinned by a simpleCore Event Semantics which is sufficiently expressive to describe the event models underlying theseAPIs. Our reference implementations are trustworthy in that three follow the appropriate standardsline-by-line and all are thoroughly tested against the official test-suites, passing all the applicabletests. Using the Core Event Semantics and the reference implementations, we develop JaVerT.Click,a symbolic execution tool for JavaScript that, for the first time, supports reasoning about JavaScriptprograms that use multiple event-related APIs. We demonstrate the viability of JaVerT.Click byproving both the presence and absence of bugs in real-world JavaScript code.
Date Issued
2020-11-06
Date Acceptance
2020-04-08
Citation
LIPIcs : Leibniz International Proceedings in Informatics, 2020, 166, pp.28:1-28:29
ISSN
1868-8969
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Start Page
28:1
End Page
28:29
Journal / Book Title
LIPIcs : Leibniz International Proceedings in Informatics
Volume
166
Copyright Statement
© 2020 Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner;
licensed under Creative Commons License CC-BY
licensed under Creative Commons License CC-BY
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Grant Number
EP/K008528/1 - RG65358
EP/K008528/1
EP/R034567/1
Source
34th European Conference on Object-Oriented Programming (ECOOP 2020)
Publication Status
Published
Start Date
2020-07-13
Finish Date
2020-07-17
Coverage Spatial
Berlin, Germany
Date Publish Online
2020-11-06
