Initial commit.
Este commit está contenido en:
padre
613d95a417
commit
8c3a75a34c
|
@ -0,0 +1,87 @@
|
|||
To cite the use of this formal theory, please use
|
||||
|
||||
Achim D. Brucker and Michael Herzberg. A Formalization of Web Components. In Archive of
|
||||
Formal Proofs, 2020. http://www.isa-afp.org/entries/DOM_Components.html,
|
||||
Formal proof development
|
||||
|
||||
|
||||
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},
|
||||
}
|
||||
|
||||
An overview of the formalization is given in:
|
||||
|
||||
Achim D. Brucker and Michael Herzberg. A Formally Verified Model of
|
||||
Web Components. In Formal Aspects of Component Software (FACS).
|
||||
Lecture Notes in Computer Science (12018), Springer-Verlag, 2020.
|
||||
http://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019
|
||||
|
||||
A BibTeX entry for LaTeX users is
|
||||
|
||||
|
||||
@InCollection{ brucker.ea:web-components:2019,
|
||||
abstract = {The trend towards ever more complex client-side web applications is unstoppable. Compared to
|
||||
traditional software development, client-side web development lacks a well-established component
|
||||
model, i.e., a method for easily and safely reusing already developed functionality. To address this
|
||||
issue, the web community started to adopt shadow trees as part of the Document Object Model (DOM):
|
||||
shadow trees allow developers to "partition" a DOM instance into parts that should be safely
|
||||
separated, e.g., code modifying one part should not, unintentionally, affect other parts of the DOM.
|
||||
|
||||
While shadow trees provide the technical basis for defining web components, the DOM standard neither
|
||||
defines the concept of web components nor specifies the safety properties that web components should
|
||||
guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying
|
||||
the DOM respect component boundaries. In this paper, we present a formally verified model of web
|
||||
components and define safety properties which ensure that different web components can only interact
|
||||
with each other using well-defined interfaces. Moreover, our verification of the application
|
||||
programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM
|
||||
API need to preserve to ensure the integrity of components.},
|
||||
keywords = {Web Component, Shadow Tree, DOM, Isabelle/HOL},
|
||||
location = {Amsterdam, The Netherlands},
|
||||
author = {Achim D. Brucker and Michael Herzberg},
|
||||
booktitle = {Formal Aspects of Component Software (FACS)},
|
||||
language = {USenglish},
|
||||
publisher = pub-springer,
|
||||
address = pub-springer:adr,
|
||||
series = s-lncs,
|
||||
number = 12018,
|
||||
isbn = {3-540-25109-X},
|
||||
doi = {10.1007/978-3-030-40914-2_3},
|
||||
editor = {Sung-Shik Jongmans and Farhad Arbab},
|
||||
pdf = {http://www.brucker.ch/bibliography/download/2019/brucker.ea-web-components-2019.pdf},
|
||||
title = {A Formally Verified Model of Web Components},
|
||||
classification= {conference},
|
||||
areas = {formal methods, software},
|
||||
year = 2020,
|
||||
public = {yes},
|
||||
url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019}
|
||||
}
|
||||
|
|
@ -0,0 +1,38 @@
|
|||
# A Formalization of Web Components (DOM_Components)
|
||||
|
||||
This git repository contains a local mirror of the [Archive of Formal Proofs (AFP)](https://www.isa-afp.org)
|
||||
entry [*A Formalization of Web Components*](https://www.isa-afp.org/entries/DOM_Components.shtml).
|
||||
|
||||
The official AFP releases are tagged. Additionally, this repository may contain extensions (i.e., a
|
||||
development version) that may be submitted at a later point in time.
|
||||
|
||||
## How to build
|
||||
|
||||
```console
|
||||
achim@logicalhacking:~$ isabelle build -D DOM_Components
|
||||
```
|
||||
|
||||
## Authors
|
||||
|
||||
* [Achim D. Brucker](http://www.brucker.ch/)
|
||||
* [Michael Herzberg](http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg)
|
||||
|
||||
## License
|
||||
|
||||
This project is licensed under a 3-clause BSD-style license.
|
||||
|
||||
SPDX-License-Identifier: BSD-3-Clause
|
||||
|
||||
## Master Repository
|
||||
|
||||
The master git repository for this project is hosted by the [Software
|
||||
Assurance & Security Research Team](https://logicalhacking.com) at
|
||||
<https://git.logicalhacking.com/afp-mirror/Core_DOM>.
|
||||
|
||||
## Publications
|
||||
|
||||
* Achim D. Brucker and Michael Herzberg. A Formally Verified Model of
|
||||
Web Components. In Formal Aspects of Component Software (FACS).
|
||||
Lecture Notes in Computer Science (12018), Springer-Verlag, 2020,
|
||||
[doi:10.1007/978-3-030-40914-2_3](https://doi.org/10.1007/978-3-030-40914-2_3).
|
||||
<http://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019>
|
Cargando…
Referencia en una nueva incidencia