A Formally Verified Model of Web Components

By Achim D. Brucker and Michael Herzberg.

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.

Keywords:
Web Component, Shadow Tree, DOM, Isabelle/HOL

Further Reading:
This presentation is based on the following publication:
A. D. Brucker and M. Herzberg, “A formally verified model of web components,” in Formal aspects of component software (FACS), S.-S. Jongmans and F. Arbab, Eds. Heidelberg: Springer-Verlag, 2020. doi: 10.1007/978-3-030-40914-2_3. Author copy: http://logicalhacking.com/publications/brucker.ea-web-components-2019/

Please cite this work as follows:
A. D. Brucker and M. Herzberg, “A formally verified model of web components,” presented at the International conference on formal aspects of component software (FACS 2019), Amsterdam, The Netherlands, Oct. 25, 2019. Author copy: http://logicalhacking.com/publications/talk-brucker.ea-web-components-2019/

BibTeX
@Unpublished{ talk:brucker.ea:web-components:2019,
  date       = {2019-10-25},
  author     = {Achim D. Brucker and Michael Herzberg},
  title      = {A Formally Verified Model of Web Components},
  keywords   = {Web Component, Shadow Tree, DOM, Isabelle/HOL},
  venue      = {Amsterdam, The Netherlands},
  eventtitle = {International Conference on Formal Aspects of Component
                Software (FACS 2019)},
  areas      = {formal methods, software},
  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.},
  note       = {Author copy: \url{http://logicalhacking.com/publications/talk-brucker.ea-web-components-2019/}},
}