A Formalization of Web Components

By Achim D. Brucker and Michael Herzberg.

While the DOM with 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 AFP entry, 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.

Please cite this work as follows:
A. D. Brucker and M. Herzberg, “A formalization of web components,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/DOM_Components.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-afp-dom-components-2020/

BibTeX
@Article{ brucker.ea:afp-dom-components:2020,
  author    = {Achim D. Brucker and Michael Herzberg},
  title     = {A Formalization of Web Components},
  journal   = {Archive of Formal Proofs},
  month     = {sep},
  year      = {2020},
  date      = {2020-09-28},
  note      = {\url{https://www.isa-afp.org/entries/DOM_Components.html},
               Formal proof development. 
               Author copy: \url{https://logicalhacking.com/publications/brucker.ea-afp-dom-components-2020/}},
  issn      = {2150-914x},
  filelabel = {Outline},
  file      = {download/2020/brucker.ea-afp-dom-components-outline-2020.pdf},
  areas     = {formal methods, security, software engineering},
  abstract  = {While the DOM with 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 AFP entry, 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.},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-afp-dom-components-2020/brucker.ea-afp-dom-components-2020.pdf},
}