The Core DOM

By Achim D. Brucker and Michael Herzberg.

In this AFP entry, we formalize the core of the Document Object Model (DOM). At its core, the DOM defines a tree-like data structure for representing documents in general and HTML documents in particular. It is the heart of any modern web browser. Formalizing the key concepts of the DOM is a prerequisite for the formal reasoning over client-side JavaScript programs and for the analysis of security concepts in modern web browsers. We present a formalization of the core DOM, with focus on the node-tree and the operations defined on node-trees, in Isabelle/HOL. We use the formalization to verify the functional correctness of the most important functions defined in the DOM standard. Moreover, our formalization is 1) extensible, i.e., can be extended without the need of re-proving already proven properties and 2) executable, i.e., we can generate executable code from our specification.

Please cite this work as follows:
A. D. Brucker and M. Herzberg, “The Core DOM,” Archive of Formal Proofs, Dec. 2018. https://www.isa-afp.org/entries/Core_DOM.html, Formal proof development. Author copy: http://logicalhacking.com/publications/brucker.ea-afp-core-dom-2018/

BibTeX
@Article{ brucker.ea:afp-core-dom:2018,
  author    = {Achim D. Brucker and Michael Herzberg},
  title     = {The {Core} {DOM}},
  journal   = {Archive of Formal Proofs},
  month     = {dec},
  year      = {2018},
  date      = {2018-12-26},
  note      = {\url{https://www.isa-afp.org/entries/Core_DOM.html}, Formal
               proof development. 
               Author copy: \url{http://logicalhacking.com/publications/brucker.ea-afp-core-dom-2018/}},
  issn      = {2150-914x},
  abstract  = {In this AFP entry, we formalize the core of the Document
               Object Model (DOM). At its core, the DOM defines a tree-like
               data structure for representing documents in general and HTML
               documents in particular. It is the heart of any modern web
               browser. Formalizing the key concepts of the DOM is a
               prerequisite for the formal reasoning over client-side
               JavaScript programs and for the analysis of security concepts
               in modern web browsers. We present a formalization of the core
               DOM, with focus on the node-tree and the operations defined on
               node-trees, in Isabelle/HOL. We use the formalization to
               verify the functional correctness of the most important
               functions defined in the DOM standard. Moreover, our
               formalization is 1) extensible, i.e., can be extended without
               the need of re-proving already proven properties and 2)
               executable, i.e., we can generate executable code from our
               specification.},
  filelabel = {Outline},
  file      = {download/2018/brucker.ea-afp-core-dom-outline-2018.pdf},
  areas     = {formal methods, security, software engineering},
}