pdfreaders.org

A Formalization of Safely Composable Web Components

by Achim D. Brucker and Michael Herzberg

Cover for brucker.ea:afp-sc-dom-components:2020.While the (safely composable) DOM with shadow trees provide the technical basis for defining web components, it does 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 safely composable 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:
Categories: , ,
Documents: (full text as PDF file) (Outline)

QR Code for brucker.ea:afp-sc-dom-components:2020.Please cite this article as follows:
Achim D. Brucker and Michael Herzberg. A Formalization of Safely Composable Web Components. In Archive of Formal Proofs, 2020. http://www.isa-afp.org/entries/SC_DOM_Components.html, Formal proof development
(full text as PDF file) (Outline) (BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@Article{ brucker.ea:afp-sc-dom-components:2020,
abstract = {While the (safely composable) DOM with shadow trees provide the technical basis for defining web components, it does 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 safely composable 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.},
author = {Achim D. Brucker and Michael Herzberg},
date = {2020-09-28},
file = {https://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-sc-dom-components-outline-2020.pdf},
filelabel = {Outline},
issn = {2150-914x},
journal = {Archive of Formal Proofs},
month = {sep},
note = {\url{http://www.isa-afp.org/entries/SC_DOM_Components.html}, Formal proof development},
pdf = {https://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-sc-dom-components-2020.pdf},
title = {A Formalization of Safely Composable Web Components},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-afp-sc-dom-components-2020},
year = {2020},
}