diff --git a/CITATION b/CITATION index bcf1200..cd60c61 100644 --- a/CITATION +++ b/CITATION @@ -7,36 +7,35 @@ To cite the use of this formal theory, please use 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}, -} +@Article{ brucker.ea:afp-dom-components:2020, + author = {Achim D. Brucker and Michael Herzberg}, + title = {A Formalization of Web Components}, + journal = {Archive of Formal Proofs}, + month = sep, + year = 2020, + date = {2020-09-28}, + note = {\url{http://www.isa-afp.org/entries/DOM_Components.html}, Formal proof development}, + issn = {2150-914x}, + public = {yes}, + classification= {formal}, + categories = {websecurity}, + pdf = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-dom-components-2020.pdf}, + filelabel = {Outline}, + file = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-dom-components-outline-2020.pdf}, + areas = {formal methods, security, software engineering}, + abstract = { While the DOM with 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 AFP entry, 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. }, + url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-dom-components-2020} +} + An overview of the formalization is given in: