A formalization of the fDOM in Isabelle/HOL.
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.
Achim D. Brucker c114b9d9ec Merge branch 'master' of git.logicalhacking.com:BrowserSecurity/fDOM-formalization 2 weeks ago
AFP Merge branch 'master' of git.logicalhacking.com:BrowserSecurity/fDOM-formalization 2 weeks ago
example Removed unused facny_tabs example. 1 month ago
quirks Added some comments about official test cases. 3 years ago
scripts Fixed syntax after renaming. 7 months ago
.gitignore Ignore syncthing files. 1 year ago
AFP-Planning-and-ToDos.md Initial commit. 7 months ago
LICENSE initial commit 4 years ago
README.md Removed Core_DOM and switched depending projects to offical AFP entry. 1 year ago
benchmark.csv Added benchmark file for thesis. 11 months ago
fdom.thy Removed non-functional/empty HTML sessions. 3 months ago
fdom_Scope_Components.thy Removed non-functional/empty HTML sessions. 3 months ago
test_case_analysis.csv Restructered test case analysis a bit. 3 years ago
test_status.ods current status of test_status.odf. 3 years ago


fDOM: A Formalization of the DOM in Isabelle/HOL

The project fDOM is a formalization of the DOM (and related standards) in Isabelle/HOL. The project has the following sub-projects:

  • Core_DOM: This Isabelle projects contains the formalization of the Document Object Model (DOM) without the support for Web components (Shadow Roots). This project is now an official part of the Archive of Formal Proofs.
  • Shadow_DOM: This Isabelle projects extents the Core_DOM with support for Web components (Shadow Roots) and, thus, reflects the latest developments in the DOM standardisation efforts.
  • DOM_Components: A formalization of web components.
  • HTML: This Isabelle projects contains a formalisation of a few core elements of the HTML standard (extending the the Shadow_DOM. Its main purpose is to allow for comparing componentization concepts (namely, Shadow Roots and iFrames) with respect to their security and safety properties.




Interactive Mode

If you want to load all theories into Isabelle “at once”, you can execute the following command in the top level directory:

isabelle jedit -d . -l HOL-Library Shadow_DOM/*.thy HTML/*.thy                                                    

This is, in particular, useful for refactoring tasks. If you only want to work with one specific project, e.g., the Shadow_DOM, you can call Isabelle as follows.

isabelle jedit -d . -l Core_DOM Shadow_DOM/*.thy                                           

Before pushing changes to the main repository, please ensure that the batch build of the project HTML works; including the generation of the LaTeX documentation.

Batch Mode:

To ensure that all projects build correctly (including the document preparation), it is sufficient to execute the following command:

isabelle build -c -j 4 -d . HTML

Of course, each project can also be build in individually.


Main developers:


This project is licensed under a 2-clause BSD-style license.

SPDX-License-Identifier: BSD-2-Clause