Commit 4aa5b379 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

new entry Shadow_SC_DOM

parent 78358736c8d0
......@@ -470,6 +470,7 @@ Separata
Separation_Algebra
Separation_Logic_Imperative_HOL
SequentInvertibility
Shadow_SC_DOM
Shivers-CFA
ShortestPath
Show
......
chapter AFP
session "Shadow_SC_DOM" (AFP) = "Core_SC_DOM" +
options [timeout = 1200]
directories
classes
monads
tests
theories
Shadow_DOM
Shadow_DOM_Tests
document_files
"root.tex"
"root.bib"
This diff is collapsed.
(***********************************************************************************
* Copyright (c) 2016-2020 The University of Sheffield, UK
* 2019-2020 University of Exeter, UK
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
***********************************************************************************)
section\<open>Shadow DOM Tests\<close>
theory Shadow_DOM_Tests
imports
"tests/slots"
"tests/slots_fallback"
"tests/Shadow_DOM_Document_adoptNode"
"tests/Shadow_DOM_Document_getElementById"
"tests/Shadow_DOM_Node_insertBefore"
"tests/Shadow_DOM_Node_removeChild"
begin
end
This diff is collapsed.
This diff is collapsed.
\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]
{scrreprt}
\usepackage[USenglish]{babel}
\usepackage[numbers, sort&compress]{natbib}
\usepackage{isabelle,isabellesym}
\usepackage{booktabs}
\usepackage{paralist}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{xspace}
\usepackage{xcolor}
\usepackage{listings}
\lstloadlanguages{HTML}
\usepackage[]{mathtools}
\usepackage[pdfpagelabels, pageanchor=false, plainpages=false]{hyperref}
\lstdefinestyle{html}{language=XML,
basicstyle=\ttfamily,
commentstyle=\itshape,
keywordstyle=\color{blue},
ndkeywordstyle=\color{blue},
}
\lstdefinestyle{displayhtml}{style=html,
floatplacement={tbp},
captionpos=b,
framexleftmargin=0pt,
basicstyle=\ttfamily\scriptsize,
backgroundcolor=\color{black!2},
frame=lines,
}
\lstnewenvironment{html}[1][]{\lstset{style=displayhtml, #1}}{}
\def\inlinehtml{\lstinline[style=html, columns=fullflexible]}
\pagestyle{headings}
\isabellestyle{default}
\setcounter{tocdepth}{1}
\newcommand{\ie}{i.\,e.\xspace}
\newcommand{\eg}{e.\,g.\xspace}
\newcommand{\thy}{\isabellecontext}
\renewcommand{\isamarkupsection}[1]{%
\begingroup%
\def\isacharunderscore{\textunderscore}%
\section{#1 (\thy)}%
\endgroup%
}
\title{Shadow SC DOM\\\medskip \Large
A Formal Model of the Safely Composable Document Object Model \emph{with Shadow Roots}}%
\author{%
\href{https://www.brucker.ch/}{Achim~D.~Brucker}\footnotemark[1]
\and
\href{https://www.michael-herzberg.de/}{Michael Herzberg}\footnotemark[2]
}
\publishers{
\footnotemark[1]~Department of Computer Science, University of Exeter, Exeter, UK\texorpdfstring{\\}{, }
\texttt{a.brucker@exeter.ac.uk}\\[2em]
%
\footnotemark[2]~ Department of Computer Science, The University of Sheffield, Sheffield, UK\texorpdfstring{\\}{, }
\texttt{msherzberg1@sheffield.ac.uk}
}
\begin{document}
\maketitle
\begin{abstract}
\begin{quote}
In this AFP entry, we extend our formalization of the safely
composable DOM
(\href{https://www.isa-afp.org/entries/Core_SC_DOM.html}
{Core\_SC\_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
\begin{inparaenum}
\item \emph{extensible}, i.e., can be extended without the need of
re-proving already proven properties and
\item \emph{executable}, i.e., we can generate executable code
from our specification.
\end{inparaenum}
We exploit the executability to show that our formalization
complies to the official standard of the W3C, respectively,
the WHATWG.
\bigskip
\noindent{\textbf{Keywords:}}
Document Object Model, DOM, Shadow Root, Web Component, Formal
Semantics, Isabelle/HOL
\end{quote}
\end{abstract}
\tableofcontents
\cleardoublepage
\chapter{Introduction}
In a world in which more and more applications are offered as services
on the internet, web browsers start to take on a similarly central
role in our daily IT infrastructure as operating systems. Thus, web
browsers should be developed as rigidly and formally as operating
systems. While formal methods are a well-established technique in the
development of operating systems (see,
\eg,~\citet{klein:operating:2009} for an overview of formal
verification of operating systems), there are few proposals for
improving the development of web browsers using formal
approaches~\cite{gardner.ea:dom:2008,raad.ea:dom:2016,jang.ea:establishing:2012,bohannon.ea:featherweight:2010}.
In~\cite{brucker.ea:afp-core-sc-dom:2020}, we formalized the core of
the safely composable Document Object Model (DOM) in
Isabelle/HOL\@. The DOM~\cite{whatwg:dom:2017,w3c:dom:2015} is
\emph{the} central data structure of all modern web browsers. In this
work, we extend the formalization presented
in~\cite{brucker.ea:afp-core-dom:2018} with support for \emph{shadow
trees}. Shadow trees are a recent addition to the DOM
standard~\cite{whatwg:dom:2017} that promise support for web
components. As we will see, this promise is not fully achieved and,
for example, the DOM standard itself does not formally define what a
component should be. In this work, we focus on a standard compliant
representation of the DOM with shadow
trees. As~\cite{brucker.ea:afp-core-sc-dom:2020}, our formalization has
the following properties:
\begin{itemize}
\item It provides a \emph{consistency guarantee.} Since all
definitions in our formal semantics are conservative and all rules
are derived, the logical consistency of the DOM node-tree is reduced
to the consistency of HOL.
\item It serves as a \emph{technical basis for a proof system.} Based
on the derived rules and specific setup of proof tactics over
node-trees, our formalization provides a generic proof environment
for the verification of programs manipulating node-trees.
\item It is \emph{executable}, which allows to validate its compliance
to the standard by evaluating the compliance test suite on the
formal model and
\item It is \emph{extensible} in the sense
of~\cite{brucker.ea:extensible:2008-b,brucker:interactive:2007},
\ie, properties proven over the core DOM do not need to be re-proven
for object-oriented extensions such as the HTML document model.
\end{itemize}
In this AFP entry, we limit ourselves to the faithful formalization of
the DOM. As the DOM standard does not formally define web components,
we address the question of formally defining web components and
discussing their safety properties
elsewhere~\cite{brucker.ea:afp-sc-dom-components:2020,brucker.ea:web-components:2019}.
The rest of this document is automatically generated from the formalization
in Isabelle/HOL, i.e., all content is checked by Isabelle (for a more
abstract presentation and more explanations, please
see~\cite{herzberg:web-components:2020}). The structure follows the theory
dependencies (see \autoref{fig:session-graph}): first, we formalize the DOM
with Shadow Roots (\autoref{cha:dom}) and then formalize we the relevant
compliance test cases in \autoref{cha:tests}.
\paragraph{Important Note:} This document describes the formalization
of the \emph{Safely Composable Document Object Model with Shadow
Roots} (SC DOM with Shadow Roots), which deviated in one important
aspect from the official DOM standard: in the SC DOM, the shadow root
is a sub-class of the document class (instead of a base class). This
modification results in a stronger notion of web components that
provide improved safety properties for the composition of web
components. While the SC DOM still passes the compliance test suite as
provided by the authors of the DOM standard, its data model is
different. We refer readers interested in a formalisation of the
standard compliant DOM to the AFP entries
``Core\_DOM''~\cite{brucker.ea:afp-core-dom:2018} and
``Shadow\_DOM''~\cite{brucker.ea:afp-shadow-dom:2020}.
\begin{figure}
\centering
\includegraphics[angle=90,scale=0.5]{session_graph}
\caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}}
\end{figure}
\clearpage
\chapter{The Shadow DOM}
\label{cha:dom}
In this chapter, we introduce the formalization of the core DOM
\emph{with Shadow Roots}, i.e., the most important algorithms for
querying or modifying the Shadow DOM, as defined in the standard.
\input{ShadowRootClass.tex}
\input{ShadowRootMonad.tex}
\input{Shadow_DOM.tex}
\chapter{Test Suite}
\label{cha:tests}
In this chapter, we present the formalized compliance test cases for
the core DOM. As our formalization is executable, we can
(symbolically) execute the test cases on top of our model. Executing
these test cases successfully shows that our model is compliant to the
official DOM standard. As future work, we plan to generate test cases
from our formal model (e.g.,
using~\cite{brucker.ea:interactive:2005,brucker.ea:theorem-prover:2012})
to improve the quality of the official compliance test suite. For more
details on the relation of test and proof in the context of web
standards, we refer the reader to
\cite{brucker.ea:standard-compliance-testing:2018}.
\input{Shadow_DOM_BaseTest.tex}
\input{slots.tex}
\input{slots_fallback.tex}
\input{Shadow_DOM_Document_adoptNode.tex}
\input{Shadow_DOM_Document_getElementById.tex}
\input{Shadow_DOM_Node_insertBefore.tex}
\input{Shadow_DOM_Node_removeChild.tex}
\input{Shadow_DOM_Tests.tex}
{\small
\bibliographystyle{abbrvnat}
\bibliography{root}
}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
This diff is collapsed.
<!doctype html>
<meta charset=utf-8>
<title>Document.adoptNode</title>
<link rel=help href="https://dom.spec.whatwg.org/#dom-document-adoptnode">
<script src="/resources/testharness.js"></script>
<script src="/resources/testharnessreport.js"></script>
<div id="log"></div>
<x<>x</x<>
<script>
test(function() {
var y = document.getElementsByTagName("x<")[0]
var child = y.firstChild
assert_equals(y.parentNode, document.body)
assert_equals(y.ownerDocument, document)
assert_equals(document.adoptNode(y), y)
assert_equals(y.parentNode, null)
assert_equals(y.firstChild, child)
assert_equals(y.ownerDocument, document)
assert_equals(child.ownerDocument, document)
var doc = document.implementation.createDocument(null, null, null)
assert_equals(doc.adoptNode(y), y)
assert_equals(y.parentNode, null)
assert_equals(y.firstChild, child)
assert_equals(y.ownerDocument, doc)
assert_equals(child.ownerDocument, doc)
}, "Adopting an Element called 'x<' should work.")
test(function() {
var x = document.createElement(":good:times:")
assert_equals(document.adoptNode(x), x);
var doc = document.implementation.createDocument(null, null, null)
assert_equals(doc.adoptNode(x), x)
assert_equals(x.parentNode, null)
assert_equals(x.ownerDocument, doc)
}, "Adopting an Element called ':good:times:' should work.")
</script>
<!DOCTYPE html>
<meta charset=utf-8>
<title>Document.getElementById</title>
<link rel="author" title="Tetsuharu OHZEKI" href="mailto:saneyuki.snyk@gmail.com">
<link rel=help href="https://dom.spec.whatwg.org/#dom-document-getelementbyid">
<script src="/resources/testharness.js"></script>
<script src="/resources/testharnessreport.js"></script>
<body>
<div id="log"></div>
<div id=""></div>
<div id="test1"></div>
<div id="test5" data-name="1st">
<p id="test5" data-name="2nd">P</p>
<input id="test5" type="submit" value="Submit" data-name="3rd">
</div>
<div id="outer">
<div id="middle">
<div id="inner"></div>
</div>
</div>
<script>
test(function() {
var gBody = document.body;
var TEST_ID = "test2";
var test = document.createElement("div");
test.setAttribute("id", TEST_ID);
gBody.appendChild(test);
// test: appended element
var result = document.getElementById(TEST_ID);
assert_not_equals(result, null, "should not be null.");
assert_equals(result.tagName, "div", "should have appended element's tag name");
// test: removed element
gBody.removeChild(test);
var removed = document.getElementById(TEST_ID);
// `document.getElementById()` returns `null` if there is none.
// https://dom.spec.whatwg.org/#dom-nonelementparentnode-getelementbyid
assert_equals(removed, null, "should not get removed element.");
}, "Document.getElementById with a script-inserted element");
test(function() {
var gBody = document.body;
// setup fixtures.
var TEST_ID = "test3";
var test = document.createElement("div");
test.setAttribute("id", TEST_ID);
gBody.appendChild(test);
// update id
var UPDATED_ID = "test3-updated";
test.setAttribute("id", UPDATED_ID);
var e = document.getElementById(UPDATED_ID);
assert_equals(e, test, "should get the element with id.");
var old = document.getElementById(TEST_ID);
assert_equals(old, null, "shouldn't get the element by the old id.");
// remove id.
test.removeAttribute("id");
var e2 = document.getElementById(UPDATED_ID);
assert_equals(e2, null, "should return null when the passed id is none in document.");
}, "update `id` attribute via setAttribute/removeAttribute");
test(function() {
var TEST_ID = "test4-should-not-exist";
var e = document.createElement('div');
e.setAttribute("id", TEST_ID);
assert_equals(document.getElementById(TEST_ID), null, "should be null");
document.body.appendChild(e);
assert_equals(document.getElementById(TEST_ID), e, "should be the appended element");
}, "Ensure that the id attribute only affects elements present in a document");
test(function() {
var gBody = document.body;
// the method should return the 1st element.
var TEST_ID = "test5";
var target = document.getElementById(TEST_ID);
assert_not_equals(target, null, "should not be null");
assert_equals(target.getAttribute("data-name"), "1st", "should return the 1st");
// even if after the new element was appended.
var element4 = document.createElement("div");
element4.setAttribute("id", TEST_ID);
element4.setAttribute("data-name", "4th");
gBody.appendChild(element4);
var target2 = document.getElementById(TEST_ID);
assert_not_equals(target2, null, "should not be null");
assert_equals(target2.getAttribute("data-name"), "1st", "should be the 1st");
// should return the next element after removed the subtree including the 1st element.
target2.parentNode.removeChild(target2);
var target3 = document.getElementById(TEST_ID);
assert_not_equals(target3, null, "should not be null");
assert_equals(target3.getAttribute("data-name"), "4th", "should be the 4th");
}, "in tree order, within the context object's tree");
test(function() {
var TEST_ID = "test6";
var s = document.createElement("div");
s.setAttribute("id", TEST_ID);
// append to Element, not Document.
document.createElement("div").appendChild(s);
assert_equals(document.getElementById(TEST_ID), null, "should be null");
}, "Modern browsers optimize this method with using internal id cache. This test checks that their optimization should effect only append to `Document`, not append to `Node`.");
test(function() {
var gBody = document.body;
var TEST_ID = "test7"
var element = document.createElement("div");
element.setAttribute("id", TEST_ID);
gBody.appendChild(element);
var target = document.getElementById(TEST_ID);
assert_equals(target, element, "should return the element before changing the value");
element.setAttribute("id", TEST_ID + "-updated");
var target2 = document.getElementById(TEST_ID);
assert_equals(target2, null, "should return null after updated id via Attr.value");
var target3 = document.getElementById(TEST_ID + "-updated");
assert_equals(target3, element, "should be equal to the updated element.");
}, "changing attribute's value via `Attr` gotten from `Element.attribute`.");
test(function() {
var gBody = document.body;
// setup fixtures.
var TEST_ID = "test12";
var test = document.createElement("div");
test.setAttribute("id", TEST_ID);
gBody.appendChild(test);
// update id
var UPDATED_ID = TEST_ID + "-updated";
test.setAttribute("id", UPDATED_ID);
var e = document.getElementById(UPDATED_ID);
assert_equals(e, test, "should get the element with id.");
var old = document.getElementById(TEST_ID);
assert_equals(old, null, "shouldn't get the element by the old id.");
// remove id.
test.setAttribute("id", "");
var e2 = document.getElementById(UPDATED_ID);
assert_equals(e2, null, "should return null when the passed id is none in document.");
}, "update `id` attribute via element.id");
test(function() {
var gBody = document.body;
var TEST_ID = "test13";
// create fixture
var container = document.createElement("div");
container.setAttribute("id", TEST_ID + "-fixture");
gBody.appendChild(container);
var element1 = document.createElement("div");
element1.setAttribute("id", TEST_ID);
var element2 = document.createElement("div");
element2.setAttribute("id", TEST_ID);
var element3 = document.createElement("div");
element3.setAttribute("id", TEST_ID);
var element4 = document.createElement("div");
element4.setAttribute("id", TEST_ID);
// append element: 2 -> 4 -> 3 -> 1
container.appendChild(element2);
container.appendChild(element4);
container.insertBefore(element3, element4);
container.insertBefore(element1, element2);
var test = document.getElementById(TEST_ID);
assert_equals(test, element1, "should return 1st element");
container.removeChild(element1);
test = document.getElementById(TEST_ID);
assert_equals(test, element2, "should return 2nd element");
container.removeChild(element2);
test = document.getElementById(TEST_ID);
assert_equals(test, element3, "should return 3rd element");
container.removeChild(element3);
test = document.getElementById(TEST_ID);
assert_equals(test, element4, "should return 4th element");
container.removeChild(element4);
}, "where insertion order and tree order don't match");
test(function() {
var gBody = document.body;
var TEST_ID = "test14";
var a = document.createElement("a");
var b = document.createElement("b");
a.appendChild(b);
b.setAttribute("id", TEST_ID);
assert_equals(document.getElementById(TEST_ID), null);
gBody.appendChild(a);
assert_equals(document.getElementById(TEST_ID), b);
}, "Inserting an id by inserting its parent node");
test(function () {
var TEST_ID = "test15"
var outer = document.getElementById("outer");
var middle = document.getElementById("middle");
var inner = document.getElementById("inner");
outer.removeChild(middle);
var new_el = document.createElement("h1");
new_el.setAttribute("id", "heading");
inner.appendChild(new_el);
// the new element is not part of the document since
// "middle" element was removed previously
assert_equals(document.getElementById("heading"), null);
}, "Document.getElementById must not return nodes not present in document");
// TODO:
// id attribute in a namespace
// TODO:
// SVG + MathML elements with id attributes
</script>
</body>
</html>
<!DOCTYPE html>
<title>Node.insertBefore</title>