pdfreaders.org

A Formal Semantics of the Core DOM in Isabelle/HOL

Achim D. Brucker und 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.

Schlüsselwörter: Document Object Model, DOM, Formal Semantics, Isabelle/HOL
Kategorien: ,
Dokumente:

QR Code for brucker.ea:fdom:2018.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker und Michael Herzberg. A Formal Semantics of the Core DOM in Isabelle/HOL. In Proceedings of the Web Programming, Design, Analysis, And Implementation (WPDAI) track at WWW 2018. , 2018.
Schlüsselwörter: Document Object Model, DOM, Formal Semantics, Isabelle/HOL
(BibTeX) (Endnote) (RIS) (Word) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InProceedings{ brucker.ea:fdom: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.},
author = {Achim D. Brucker and Michael Herzberg},
booktitle = {Proceedings of the Web Programming, Design, Analysis, And Implementation (WPDAI) track at WWW 2018},
keywords = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},
location = {Lyon, France},
title = {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-fdom-2018},
year = {2018},
}