You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
76 lines
4.3 KiB
76 lines
4.3 KiB
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}, |
|
}
|
|
|