|
- To cite the use of this formal theory, please use
-
- Achim D. Brucker and Michael Herzberg. The Safely Composable DOM. In Archive of
- Formal Proofs, 2020. http://www.isa-afp.org/entries/Core_SC_DOM.html,
- Formal proof development
-
- A BibTeX entry for LaTeX users is
-
- @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{http://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., 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. },
- public = {yes},
- classification= {formal},
- categories = {websecurity},
- pdf = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-core-sc-dom-2020.pdf},
- filelabel = {Outline},
- file = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-core-sc-dom-outline-2020.pdf},
- areas = {formal methods, security, software engineering},
- url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-sc-dom-2020}
- }
-
-
- An overview of the formalization is given in:
-
- Achim D. Brucker and Michael Herzberg. A Formal Semantics of the Core DOM
- in Isabelle/HOL. In The 2018 Web Conference Companion (WWW). Pages 741-749,
- ACM Press, 2018. doi:10.1145/3184558.3185980
-
- A BibTeX entry for LaTeX users is
-
- @InProceedings{ brucker.ea:core-dom: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.},
- address = {New York, NY, USA},
- author = {Achim D. Brucker and Michael Herzberg},
- booktitle= {The 2018 Web Conference Companion (WWW)},
- conf_date= {April 23-27, 2018},
- doi = {10.1145/3184558.3185980},
- editor = {Pierre{-}Antoine Champin and Fabien L. Gandon and Mounia Lalmas and Panagiotis G. Ipeirotis},
- isbn = {978-1-4503-5640-4/18/04},
- keywords = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},
- location = {Lyon, France},
- pages = {741--749},
- pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-core-dom-2018.pdf},
- publisher= {ACM Press},
- title = {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}},
- url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018},
- year = {2018},
- }
|
