By Achim D. Brucker and Michael Herzberg.
In this AFP entry, we formalize the core of the Safely Composable Document Object Model (SC DOM). The SC DOM improve the standard DOM by strengthening the tree boundaries set by shadow roots: in the SC DOM, the shadow root is a sub-class of the document class (instead of a base class).
This modifications also results in changes to some API methods (e.g.,
getOwnerDocument
) to return the nearest shadow root rather
than the document root. As a result, many API methods that, when called
on a node inside a shadow tree, would previously ``break out” and return
or modify nodes that are possibly outside the shadow tree, now stay
within its boundaries. This change in behavior makes programs that
operate on shadow trees more predictable for the developer and allows
them to make more assumptions about other code accessing the DOM.
Please cite this work as follows: A. D. Brucker and M. Herzberg, “The safely composable DOM,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/Core_SC_DOM.html, Formal proof development
@Article{ brucker.ea:afp-core-sc-dom:2020,
author = {Achim D. Brucker and Michael Herzberg},
title = {The Safely Composable {DOM}},
journal = {Archive of Formal Proofs},
month = {sep},
year = {2020},
date = {2020-09-28},
note = {\url{https://www.isa-afp.org/entries/Core_SC_DOM.html},
Formal proof development},issn = {2150-914x},
abstract = {In this AFP entry, we formalize the core of the Safely
Composable Document Object Model (SC DOM). The SC DOM improve
the standard DOM by strengthening the tree boundaries set by
shadow roots: in the SC DOM, the shadow root is a sub-class of
the document class (instead of a base class).
This modifications also results in changes to some API methods\texttt{getOwnerDocument}) to return the nearest shadow
(e.g.,
root rather than the document root. As a result, many API
methods that, when called on a node inside a shadow tree,
would previously ``break out'' and return or modify nodes that
are possibly outside the shadow tree, now stay within its
boundaries. This change in behavior makes programs that
operate on shadow trees more predictable for the developer and
allows them to make more assumptions about other code
accessing the DOM.},filelabel = {Outline},
file = {download/2020/brucker.ea-afp-core-sc-dom-outline-2020.pdf},
areas = {formal methods, security, software engineering},
}