Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Aspects of Component Software

FACS 2019: Formal Aspects of Component Software pp 51–71Cite as

A Formally Verified Model of Web Components

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12018))

Abstract

The trend towards ever more complex client-side web applications is unstoppable. Compared to traditional software development, client-side web development lacks a well-established component model, i. e., a method for easily and safely reusing already developed functionality. To address this issue, the web community started to adopt shadow trees as part of the Document Object Model (DOM). Shadow trees allow developers to “partition” a DOM instance into parts that should be safely separated, e. g., code modifying one part should not unintentionally affect other parts of the DOM.

While shadow trees provide the technical basis for defining web components, the DOM standard neither defines the concept of web components nor specifies the safety properties that web components should guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying the DOM respect component boundaries.

In this paper, we present a formally verified model of web components and define safety properties which ensure that different web components can only interact with each other using well-defined interfaces. Moreover, our verification of the application programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM API need to preserve to ensure the integrity of components.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Akhawe, D., Barth, A., Lam, P.E., Mitchell, J., Song, D.: Towards a formal foundation of web security. In: IEEE Computer Security Foundations Symposium (CSF), pp. 290–304. IEEE Computer Society (2010). https://doi.org/10.1109/CSF.2010.27

  2. Andrews, P.B.: Introduction to Mathematical Logic and Type Theory: To Truth through Proof, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)

    Book  Google Scholar 

  3. Bidelman, E.: Shadow DOM v1: self-contained web components (2017). https://developers.google.com/web/fundamentals/getting-started/primers/shadowdom

  4. Bohannon, A., Pierce, B.C.: Featherweight firefox: formalizing the core of a web browser. In: Usenix Web Application Development (WebApps) (2010)

    Google Scholar 

  5. Brucker, A.D.: An interactive proof environment for object-oriented specifications. Ph.D. thesis, ETH Zurich (2007). ETH Dissertation No. 17097

    Google Scholar 

  6. Brucker, A.D., Herzberg, M.: The core DOM. Archive of formal proofs (2018). http://www.isa-afp.org/entries/Core_DOM.html. Formal proof development

  7. Brucker, A.D., Herzberg, M.: A formal semantics of the Core DOM in Isabelle/HOL. In: Champin, P., Gandon, F.L., Lalmas, M., Ipeirotis, P.G. (eds.) The 2018 Web Conference Companion (WWW), pp. 741–749. ACM Press (2018). https://doi.org/10.1145/3184558.3185980

  8. Brucker, A.D., Wolff, B.: An extensible encoding of object-oriented data models in HOL. J. Autom. Reasoning 41, 219–249 (2008). https://doi.org/10.1007/s10817-008-9108-3

    Article  MATH  Google Scholar 

  9. Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5(2), 56–68 (1940)

    Article  MathSciNet  Google Scholar 

  10. Clarke, D., Östlund, J., Sergey, I., Wrigstad, T.: Ownership types: a survey. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification. LNCS, vol. 7850, pp. 15–58. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36946-9_3

    Chapter  Google Scholar 

  11. Freyberger, M., He, W., Akhawe, D., Mazurek, M.L., Mittal, P.: Cracking shadowcrypt: exploring the limitations of secure I/O systems in internet browsers. In: PoPETs, vol. 2018, no. 2, pp. 47–63 (2018). https://doi.org/10.1515/popets-2018-0012

  12. Gardner, P., Smith, G., Wheelhouse, M.J., Zarfaty, U.: DOM: towards a formal specification. In: Programming Language Technologies for XML (PLAN-X). ACM (2008)

    Google Scholar 

  13. Guha, A., Fredrikson, M., Livshits, B., Swam, N.: Verified security for browser extensions. In: IEEE Symposium on Security and Privacy, pp. 115–130 (2011). https://doi.org/10.1109/SP.2011.36

  14. Jang, D., Tatlock, Z., Lerner, S.: Establishing browser security guarantees through formal shim verification. In: Kohno, T. (ed.) USENIX, pp. 113–128. USENIX (2012)

    Google Scholar 

  15. Jensen, S.H., Madsen, M., Møller, A.: Modeling the HTML DOM and browser API in static analysis of JavaScript web applications. In: ESEC/FSE, pp. 59–69. ACM (2011). https://doi.org/10.1145/2025113.2025125

  16. Légaré, J., Sumi, R., Aiello, W.: Beeswax: a platform for private web apps. In: PoPETs, vol. 2016, no. 3, pp. 24–40 (2016)

    Google Scholar 

  17. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  18. Poetzsch-Heffter, A., Geilmann, K., Schäfer, J.: Infering ownership types for encapsulated object-oriented program components. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Program Analysis and Compilation, Theory and Practice. LNCS, vol. 4444, pp. 120–144. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71322-7_6

    Chapter  MATH  Google Scholar 

  19. Raad, A., Santos, J.F., Gardner, P.: DOM: specification and client reasoning. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 401–422. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3_21

    Chapter  MATH  Google Scholar 

  20. Smith, G.D.: Local reasoning about web programs. Ph.D. thesis, Imperial College London, London, UK (2011)

    Google Scholar 

  21. Sternagel, C., Thiemann, R.: XML. Archive of formal proofs (2014). http://isa-afp.org/entries/XML.shtml. Formal proof development

  22. W3C: Web IDL (2017). https://heycam.github.io/webidl/

  23. W3C: Shadow DOM (2018). https://www.w3.org/TR/2018/NOTE-shadow-dom-20180301/. Last Updated 1 March 2018

  24. WHATWG: DOM - living standard (2019). https://dom.spec.whatwg.org/commit-snapshots/7fa83673430f767d329406d0aed901f296332216/. Last Updated 11 February 2019

  25. WHATWG: HTML - living standard (2019). https://html.spec.whatwg.org/commit-snapshots/b8c084e9d5461b858180e7f80ad6ca19c7963723/. Last Updated 19 February 2019

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Exeter, Exeter, UK

    Achim D. Brucker

  2. Department of Computer Science, The University of Sheffield, Sheffield, UK

    Michael Herzberg

Authors
  1. Achim D. Brucker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Herzberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Achim D. Brucker .

Editor information

Editors and Affiliations

  1. CWI, University of Leiden, Leiden, The Netherlands

    Farhad Arbab

  2. Open University of the Netherlands, Heerlen, The Netherlands

    Sung-Shik Jongmans

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Brucker, A.D., Herzberg, M. (2020). A Formally Verified Model of Web Components. In: Arbab, F., Jongmans, SS. (eds) Formal Aspects of Component Software. FACS 2019. Lecture Notes in Computer Science(), vol 12018. Springer, Cham. https://doi.org/10.1007/978-3-030-40914-2_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-40914-2_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-40913-5

  • Online ISBN: 978-3-030-40914-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation