Shadow SC DOM: A Formal Model of the Safelty Composable Document Object Model with Shadow Roots

By Achim D. Brucker and Michael Herzberg.

In this AFP entry, we extend our formalization of the safely composable DOM with Shadow Roots. Shadow roots are a recent proposal of the web community to support a component-based development approach for client-side web applications.

Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be backward compatible, such extensions often result in complex specification that may contain unwanted subtleties that can be detected by a formalization.

Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can be extended without the need of re-proving already proven properties and executable, i.e., we can generate executable code from our specification. We exploit the executability to show that our formalization complies to the official standard of the W3C, respectively, the WHATWG.

Please cite this work as follows:
A. D. Brucker and M. Herzberg, “Shadow SC DOM: A formal model of the safelty composable document object model with shadow roots,” Archive of Formal Proofs, Sep. 2020. https://www.isa-afp.org/entries/Shadow_SC_DOM.html, Formal proof development. Author copy: https://logicalhacking.com/publications/brucker.ea-afp-shadow-sc-dom-2020/

BibTeX
@Article{ brucker.ea:afp-shadow-sc-dom:2020,
  author    = {Achim D. Brucker and Michael Herzberg},
  title     = {Shadow SC DOM: A Formal Model of the Safelty Composable
               Document Object Model with Shadow Roots},
  journal   = {Archive of Formal Proofs},
  month     = {sep},
  year      = {2020},
  date      = {2020-09-28},
  note      = {\url{https://www.isa-afp.org/entries/Shadow_SC_DOM.html},
               Formal proof development. 
               Author copy: \url{https://logicalhacking.com/publications/brucker.ea-afp-shadow-sc-dom-2020/}},
  issn      = {2150-914x},
  abstract  = {In this AFP entry, we extend our formalization of the safely
               composable DOM with \emph{Shadow Roots}. Shadow roots are a
               recent proposal of the web community to support a
               component-based development approach for client-side web
               applications.
               
               Shadow roots are a significant extension to the DOM standard
               and, as web standards are condemned to be backward compatible,
               such extensions often result in complex specification that may
               contain unwanted subtleties that can be detected by a
               formalization.
               
               Our Isabelle/HOL formalization is, in the sense of
               object-orientation, an extension of our formalization of the
               core DOM and enjoys the same basic properties, i.e., it is
               extensible, i.e., can be extended without the need of
               re-proving already proven properties and executable, i.e., we
               can generate executable code from our specification. We
               exploit the executability to show that our formalization
               complies to the official standard of the W3C, respectively,
               the WHATWG.},
  filelabel = {Outline},
  file      = {download/2020/brucker.ea-afp-shadow-sc-dom-outline-2020.pdf},
  areas     = {formal methods, security, software engineering},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-afp-shadow-sc-dom-2020/brucker.ea-afp-shadow-sc-dom-2020.pdf},
}