A Formal Semantics of the Core DOM in Isabelle/HOL

By Achim D. Brucker and Michael Herzberg.

At its core, the Document Object Model (DOM) defines a tree-like data structure for representing documents in general and HTML documents in particular. It forms the heart of any rendering engine of modern web browsers. Formalizing the key concepts of the DOM is a pre-requisite for the formal reasoning over client-side JavaScript programs as well as for the analysis of security concepts in modern web browsers. In this paper, 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.

Keywords:
Document Object Model, DOM, Formal Semantics, Isabelle/HOL

Please cite this work as follows:
A. D. Brucker and M. Herzberg, “A formal semantics of the Core DOM in Isabelle/HOL,” in The 2018 web conference companion (WWW), 2018, pp. 741–749. doi: 10.1145/3184558.3185980. Author copy: https://logicalhacking.com/publications/brucker.ea-core-dom-2018/

BibTeX
@InProceedings{ brucker.ea:core-dom:2018,
  author    = {Achim D. Brucker and Michael Herzberg},
  title     = {A Formal Semantics of the {Core} {DOM} in {Isabelle/HOL}},
  booktitle = {The 2018 Web Conference Companion (WWW)},
  editor    = {Pierre{-}Antoine Champin and Fabien L. Gandon and Mounia
               Lalmas and Panagiotis G. Ipeirotis},
  publisher = {ACM Press },
  location  = {Lyon, France},
  conf_date = {April 23-27, 2018},
  address   = {New York, NY, USA },
  isbn      = {9781450356404},
  pages     = {741--749},
  doi       = {10.1145/3184558.3185980},
  year      = {2018},
  abstract  = {At its core, the Document Object Model (DOM) defines a
               tree-like data structure for representing documents in general
               and HTML documents in particular. It forms the heart of any
               rendering engine of modern web browsers. Formalizing the key
               concepts of the DOM is a pre-requisite for the formal
               reasoning over client-side JavaScript programs as well as for
               the analysis of security concepts in modern web browsers. In
               this paper, 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.},
  keywords  = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},
  areas     = {formal methods, security},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-core-dom-2018/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-core-dom-2018/brucker.ea-core-dom-2018.pdf},
}