Initial commit.

CITATION

@@ -0,0 +1,88 @@
+To cite the use of this formal theory, please use
+
+  Achim D. Brucker and Michael Herzberg. A Formal Model of the Safely Composable Document Object Model
+  with Shadow Roots. In Archive of Formal Proofs, 2020. http://www.isa-afp.org/entries/Shadow_SC_DOM.html,
+  Formal proof development
+
+
+A BibTeX entry for LaTeX users is
+
+@Article{         brucker.ea:afp-shadow-sc-dom:2020,
+  author        = {Achim D. Brucker and Michael Herzberg},
+  title         = {Shadow SC DOM: A Formal Model of the Safelty Composable Document Object Model with Shadow Roots},
+  journal       = {Archive of Formal Proofs},
+  month         = sep,
+  year          = 2020,
+  date          = {2020-09-28},
+  note          = {\url{http://www.isa-afp.org/entries/Shadow_SC_DOM.html}, Formal proof development},
+  issn          = {2150-914x},
+  abstract      = { In this AFP entry, we extend our formalization of the safely composable DOM with \emph{Shadow
+                  Roots}. Shadow roots are a recent proposal of the web community to support a component-based
+                  development approach for client-side web applications.
+
+                  Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be
+                  backward compatible, such extensions often result in complex specification that may contain unwanted
+                  subtleties that can be detected by a formalization.
+
+                  Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our
+                  formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can
+                  be extended without the need of re-proving already proven properties and executable, i.e., we can
+                  generate executable code from our specification. We exploit the executability to show that our
+                  formalization complies to the official standard of the W3C, respectively, the WHATWG. },
+  public        = {yes},
+  classification= {formal},
+  categories    = {websecurity},
+  pdf           = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-shadow-sc-dom-2020.pdf},
+  filelabel     = {Outline},
+  file          = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-shadow-sc-dom-outline-2020.pdf},
+  areas         = {formal methods, security, software engineering},
+  url           = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-shadow-sc-dom-2020}
+}
+
+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}
+}
+

README.md

@@ -0,0 +1,38 @@
+# A Formal Model of the Safely Composable Document Object Model with Shadow Roots (Shadow_SC_DOM)
+
+This git repository contains a local mirror of the [Archive of Formal Proofs (AFP)](https://www.isa-afp.org)
+entry [*A Formal Model of the Safely Composable Document Object Model with Shadow Roots*](https://www.isa-afp.org/entries/Shadow_SC_DOM.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 Shadow_SC_DOM
+```
+
+## 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_SC_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>