The Safely Composable DOM

@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
               (e.g., \texttt{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.},
  filelabel = {Outline},
  file      = {download/2020/brucker.ea-afp-core-sc-dom-outline-2020.pdf},
  areas     = {formal methods, security, software engineering},
}