Document Open Access Logo

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

Authors Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, Philippa Gardner

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.28.pdf
  • Filesize: 1.72 MB
  • 29 pages

Document Identifiers

Author Details

Gabriela Sampaio
  • Imperial College London, United Kingdom
José Fragoso Santos
  • INESC-ID/Instituto Superior Técnico, Universidade de Lisboa, Portugal
  • Imperial College London, United Kingdom
Petar Maksimović
  • Imperial College London, United Kingdom
Philippa Gardner
  • Imperial College London, United Kingdom

Funding

Fragoso Santos, Gardner, and Maksimović were partially supported by the EPSRC Programme Grant "REMS: Rigorous Engineering for Mainstream Systems" (EP/K008528/1) and the EPSRC Fellowship "VetSpec: Verified Trustworthy Software Specification" (EP/R034567/1).
  • Sampaio, Gabriela: Sampaio was supported by a CAPES Foundation Scholarship, process number 88881.129599/2016-01.
  • Fragoso Santos, José: Fragoso Santos was partially supported by national funds through Fundação para a Ciência e a Tecnologia (FCT), with reference UIDB 2020 (INESC-ID multi-annual funding).

Cite AsGet BibTex

Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 28:1-28:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.28

Abstract

We introduce a trusted infrastructure for the symbolic analysis of modern event-driven Web applications. This infrastructure consists of reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises and the JavaScript async/await APIs, all underpinned by a simple Core Event Semantics which is sufficiently expressive to describe the event models underlying these APIs. Our reference implementations are trustworthy in that three follow the appropriate standards line-by-line and all are thoroughly tested against the official test-suites, passing all the applicable tests. 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 JavaScript programs that use multiple event-related APIs. We demonstrate the viability of JaVerT.Click by proving both the presence and absence of bugs in real-world JavaScript code.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Software and its engineering → Software testing and debugging
Keywords
  • Events
  • DOM
  • JavaScript
  • promises
  • symbolic execution
  • bug-finding

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. S. Alimadadi, D. Zhong, M. Madsen, and F. Tip. Finding Broken Promises in Asynchronous JavaScript Programs. PACMPL, 2(OOPSLA):162:1-162:26, 2018. Google Scholar
  2. R. Baldoni, E. Coppa, D. Cono D'Elia, C. Demetrescu, and I. Finocchi. A Survey of Symbolic Execution Techniques. ACM Computing Surveys, 51(3):50:1-50:39, 2018. Google Scholar
  3. C. Cadar, P. Godefroid, S. Khurshid, C. S. Păsăreanu, K. Sen, N. Tillmann, and W. Visser. Symbolic Execution for Software Testing in Practice: Preliminary Assessment. In ICSE, 2011. Google Scholar
  4. C. Cadar and K. Sen. Symbolic Execution for Software Testing: Three Decades Later. Commun. ACM, 56:82-90, 2013. Google Scholar
  5. C. Calcagno, P. Gardner, and U. Zarfaty. Context logic and tree update. In POPL, 2005. Google Scholar
  6. ECMA TC39. Test262 Test Suite. https://github.com/tc39/test262, visited 05/2020.
  7. ECMA TC39. The ECMAScript Standard. https://www.ecma-international.org/publications/standards/Ecma-262.htm, visited 05/2020.
  8. ECMA TC39. The ECMAScript Standard - 6th Edition. http://www.ecma-international.org/ecma-262/6.0/, visited 05/2020.
  9. ECMA TC39. The ECMAScript Standard - 9th Edition. http://www.ecma-international.org/ecma-262/9.0/, visited 05/2020.
  10. A. M. Fard, A. Mesbah, and E. Wohlstadter. Generating Fixtures for JavaScript Unit Testing (T). In ASE, 2015. Google Scholar
  11. J. Fragoso Santos, P. Maksimović, S.-E. Ayoun, and Philippa G. Gillian, Part 1: A Multi-language Framework for Symbolic Execution. In PLDI, 2020. Google Scholar
  12. J. Fragoso Santos, P. Maksimović, T. Grohens, J. Dolby, and P. Gardner. Symbolic Execution for JavaScript. In PPDP, 2018. Google Scholar
  13. J. Fragoso Santos, P. Maksimović, G. Sampaio, and P. Gardner. JaVerT 2.0: Compositional Symbolic Execution for JavaScript. PACMPL, 3(POPL):66, 2019. Google Scholar
  14. K. Gallaba, A. Mesbah, and I. Beschastnikh. Don't Call Us, We'll Call You: Characterizing Callbacks in Javascript. In ESEM, 2015. Google Scholar
  15. P. Gardner, G. Smith, M. J. Wheelhouse, and U. Zarfaty. Local Hoare Reasoning about DOM. In PODS, 2008. Google Scholar
  16. Gargoyle Software Inc. HTMUnit. http://htmlunit.sourceforge.io/, visited 05/2020.
  17. A. Guha, C. Saftoiu, and S. Krishnamurthi. The Essence of Javascript. In ECOOP, 2010. Google Scholar
  18. S. Holm Jensen, M. Madsen, and A. Møller. Modeling the HTML DOM and Browser API in Static Analysis of JavaScript Web Applications. In ESEC/FSE, 2011. Google Scholar
  19. B. S. Lerner, M. J. Carroll, D. P. Kimmel, H. Quay-De La Vallee, and S. Krishnamurthi. Modeling and Reasoning about DOM Events. In WebApps, 2012. Google Scholar
  20. G. Li, E. Andreasen, and I. Ghosh. SymJS: Automatic Symbolic Testing of JavaScript Web Applications. In FSE, 2014. Google Scholar
  21. M. Loring, M. Marron, and D. Leijen. Semantics of asynchronous javascript. In DLS, 2017. Google Scholar
  22. M. Madsen, O. Lhoták, and F. Tip. A Model for Reasoning about JavaScript Promises. PACMPL, 1(OOPSLA):86:1-86:24, 2017. Google Scholar
  23. M. Madsen, F. Tip, and O. Lhotak. Static Analysis of Event-Driven Node.js JavaScript Applications. In OOPSLA, 2015. Google Scholar
  24. A. Almeida Matos, J. Fragoso Santos, and T. Rezk. An Information Flow Monitor for a Core of DOM - Introducing References and Live Primitives. In TGC, 2014. Google Scholar
  25. Mozilla. MDN Web Docs. http://developer.mozilla.org/en-US/, visited 05/2020.
  26. Mozilla. Using Shadow DOM. https://developer.mozilla.org/en-US/docs/Web/Web_Components/Using_shadow_DOM, visited 05/2020.
  27. C. Park, S. Won, J. Jin, and S. Ryu. Static Analysis of JavaScript Web Applications in the Wild via Practical DOM Modeling (T). In ASE, 2015. Google Scholar
  28. J. Gibbs Politz, S. A. Eliopoulos, A. Guha, and S. Krishnamurthi. ADsafety: Type-Based Verification of JavaScript Sandboxing. In USENIX Security Symposium, 2011. Google Scholar
  29. V. Rajani, A. Bichhawat, D. Garg, and C. Hammer. Information Flow Control for Event Handling and the DOM in Web Browsers. In CSF, 2015. Google Scholar
  30. Alejandro Russo, Andrei Sabelfeld, and Andrey Chudnov. Tracking Information Flow in Dynamic Tree Structures. In ESORICS, 2009. Google Scholar
  31. G. Sampaio, J. Fragoso Santos, P. Maksimović, and P. Gardner. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Technical Report). https://vtss.doc.ic.ac.uk/publications/Sampaio2020Trusted.pdf, visited 05/2020.
  32. J. Fragoso Santos, P. Maksimović, D. Naudžiūnienė, T. Wood, and P. Gardner. JaVerT: JavaScript Verification Toolchain. PACMPL, 2(POPL):50:1-50:33, 2018. Google Scholar
  33. K. Sen, S. Kalasapur, T. G. Brutch, and S. Gibbs. Jalangi: A Selective Record-Replay and Dynamic Analysis Framework for JavaScript. In ESEC/FSE'13, 2013. Google Scholar
  34. G. Smith. Local reasoning about Web programs. PhD thesis, Imperial College, UK, 2011. Google Scholar
  35. S. Sorhus. p-map (GitHub). https://github.com/sindresorhus/p-map, visited 05/2020.
  36. S. Sorhus. p-map (npm). https://www.npmjs.com/package/p-map, visited 05/2020.
  37. C. Sung, M. Kusano, N. Sinha, and C. Wang. Static DOM Event Dependency Analysis for Testing Web Applications. In FSE, 2016. Google Scholar
  38. Scheme Team. The Revised Report on the Algorithmic Language Scheme. https://schemers.org/Documents/Standards/R5RS/r5rs.pdf, visited 05/2020.
  39. The PreactJS Team. PreactJS library. http://preactjs.com, visited 05/2020.
  40. The ReactJS Team. ReactJS library. http://reactjs.org, visited 05/2020.
  41. The WebKit Team. WebKit Browser Engine. https://webkit.org, visited 05/2020.
  42. Peter Thiemann. A Type Safe DOM API. In DBPL, 2005. Google Scholar
  43. E. Torlak and R. Bodík. Growing Solver-Aided Languages with Rosette. In Onward!, 2013. Google Scholar
  44. E. Torlak and R. Bodík. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In PLDI, 2014. Google Scholar
  45. M. Vanhoef, W. De Groef, D. Devriese, F. Piessens, and T. Rezk. Stateful Declassification Policies for Event-Driven Programs. In CSF, 2014. Google Scholar
  46. W3C. DOM Core Level 1 Official Test Suite. http://www.w3.org/2004/04/ecmascript/level1/core/, visited 05/2020.
  47. W3C. DOM Core Level 1 Specification. http://www.w3.org/TR/1998/REC-DOM-Level-1-19981001/level-one-core.html, visited 05/2020.
  48. W3C. DOM Core Level 2 Specification. http://www.w3.org/TR/2000/REC-DOM-Level-2-Core-20001113/, visited 05/2020.
  49. W3C. DOM Core Level 3 Specification. http://www.w3.org/TR/2004/REC-DOM-Level-3-Core-20040407/, visited 05/2020.
  50. W3C. DOM Events Official Test Suite. https://github.com/web-platform-tests/wpt/tree/master/dom/events, visited 05/2020.
  51. W3C. File API. http://www.w3.org/TR/FileAPI/, visited 05/2020.
  52. W3C. HTML Standard. http://html.spec.whatwg.org/multipage/workers.html#workers, visited 05/2020.
  53. WHATWG. DOM API Specification. http://dom.spec.whatwg.org, visited 05/2020.
  54. WHATWG. The postMessage API. https://html.spec.whatwg.org/multipage/web-messaging.html#posting-messages, visited 05/2020.
  55. K. Wheeler, S. Shaw, and F. Spampinato. cash (GitHub). https://github.com/kenwheeler/cash, visited 05/2020.
  56. K. Wheeler, S. Shaw, and F. Spampinato. cash (npm). https://www.npmjs.com/package/cash-dom, visited 05/2020.
  57. wpt.fyi. Events Browser Compliance. http://wpt.fyi/results/dom/events, visited 05/2020.
  58. Y. Nashwaan. xml-js: Converter Utility between XML Text and Javascript Objects/JSON Text. http://www.npmjs.com/package/xml-js, visited 05/2020.
  59. Y. Zou, Z. Chen, Y. Zheng, X. Zhang, and Z. Gao. Virtual DOM Coverage: Drive an Effective Testing for Dynamic Web Applications. ISSTA, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact