Formal Foundations of Web Components

By Achim D. Brucker and Michael Herzberg.

Compared to 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 talk, 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.

Please cite this work as follows:
A. D. Brucker and M. Herzberg, “Formal foundations of web components,” presented at the FoMSESS jahrestreffen 2020, Online, Oct. 12, 2020.

BibTeX
@Unpublished{ talk:brucker.ea:safe-web-components:2020,
  author     = {Achim D. Brucker and Michael Herzberg},
  date       = {2020-10-12},
  title      = {Formal Foundations of Web Components},
  abstract   = {Compared to 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 talk, 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.},
  eventtitle = {{FoMSESS} Jahrestreffen 2020},
  venue      = {Online},
  areas      = {security, formal methods},
}