Commit 6660afff authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

SC_DOM_Components website

parent 93ce0b890f00
......@@ -8384,6 +8384,30 @@ abstract =
to show that our formalization complies to the official standard of
the W3C, respectively, the WHATWG.
 
[SC_DOM_Components]
title = A Formalization of Safely Composable Web Components
author = Achim D. Brucker <https://www.brucker.ch>, Michael Herzberg <http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg>
topic = Computer science/Data structures
date = 2020-09-28
notify = adbrucker@0x5f.org, mail@michael-herzberg.de
abstract =
While the (safely composable) DOM with shadow trees provide the
technical basis for defining web components, it does 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 safely composable 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. In comparison to the strict
standard compliance formalization of Web Components in the AFP entry
"DOM_Components", the notion of components in this entry
(based on "SC_DOM" and "Shadow_SC_DOM") provides
much stronger safety guarantees.
[Store_Buffer_Reduction]
title = A Reduction Theorem for Store Buffers
author = Ernie Cohen <mailto:ecohen@amazon.com>, Norbert Schirmer <mailto:norbert.schirmer@web.de>
......
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>A Formalization of Safely Composable Web Components - Archive of Formal Proofs
</title>
<link rel="stylesheet" type="text/css" href="../front.css">
<link rel="icon" href="../images/favicon.ico" type="image/icon">
<link rel="alternate" type="application/rss+xml" title="RSS" href="../rss.xml">
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax = {
tex: {
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
processEscapes: true,
svg: {
fontCache: 'global'
}
};
</script>
<script id="MathJax-script" async src="../components/mathjax/es5/tex-mml-chtml.js"></script>
</head>
<body class="mathjax_ignore">
<table width="100%">
<tbody>
<tr>
<!-- Navigation -->
<td width="20%" align="center" valign="top">
<p>&nbsp;</p>
<a href="https://www.isa-afp.org/">
<img src="../images/isabelle.png" width="100" height="88" border=0>
</a>
<p>&nbsp;</p>
<p>&nbsp;</p>
<table class="nav" width="80%">
<tr>
<td class="nav" width="100%"><a href="../index.html">Home</a></td>
</tr>
<tr>
<td class="nav"><a href="../about.html">About</a></td>
</tr>
<tr>
<td class="nav"><a href="../submitting.html">Submission</a></td>
</tr>
<tr>
<td class="nav"><a href="../updating.html">Updating Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../using.html">Using Entries</a></td>
</tr>
<tr>
<td class="nav"><a href="../search.html">Search</a></td>
</tr>
<tr>
<td class="nav"><a href="../statistics.html">Statistics</a></td>
</tr>
<tr>
<td class="nav"><a href="../topics.html">Index</a></td>
</tr>
<tr>
<td class="nav"><a href="../download.html">Download</a></td>
</tr>
</table>
<p>&nbsp;</p>
<p>&nbsp;</p>
</td>
<!-- Content -->
<td width="80%" valign="top">
<div align="center">
<p>&nbsp;</p>
<h1> <font class="first">A</font>
<font class="first">F</font>ormalization
of
<font class="first">S</font>afely
<font class="first">C</font>omposable
<font class="first">W</font>eb
<font class="first">C</font>omponents
</h1>
<p>&nbsp;</p>
<table width="80%" class="data">
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">A Formalization of Safely Composable Web Components</td>
</tr>
<tr>
<td class="datahead">
Authors:
</td>
<td class="data">
Achim D. Brucker (a /dot/ brucker /at/ exeter /dot/ ac /dot/ uk) and
<a href="http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg">Michael Herzberg</a>
</td>
</tr>
<tr>
<td class="datahead">Submission date:</td>
<td class="data">2020-09-28</td>
</tr>
<tr>
<td class="datahead" valign="top">Abstract:</td>
<td class="abstract mathjax_process">
While the (safely composable) DOM with shadow trees provide the
technical basis for defining web components, it does 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 safely composable 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. In comparison to the strict
standard compliance formalization of Web Components in the AFP entry
"DOM_Components", the notion of components in this entry
(based on "SC_DOM" and "Shadow_SC_DOM") provides
much stronger safety guarantees.</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{SC_DOM_Components-AFP,
author = {Achim D. Brucker and Michael Herzberg},
title = {A Formalization of Safely Composable Web Components},
journal = {Archive of Formal Proofs},
month = sep,
year = 2020,
note = {\url{http://isa-afp.org/entries/SC_DOM_Components.html},
Formal proof development},
ISSN = {2150-914x},
}</pre>
</td>
</tr>
<tr><td class="datahead">License:</td>
<td class="data"><a href="http://isa-afp.org/LICENSE">BSD License</a></td></tr>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Shadow_SC_DOM.html">Shadow_SC_DOM</a> </td></tr>
</tbody>
</table>
<p></p>
<table class="links">
<tbody>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/SC_DOM_Components/outline.pdf">Proof outline</a><br>
<a href="../browser_info/current/AFP/SC_DOM_Components/document.pdf">Proof document</a>
</td>
</tr>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/SC_DOM_Components/index.html">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="../release/afp-SC_DOM_Components-current.tar.gz">Download this entry</a>
</td>
</tr>
<tr><td class="links">Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script src="../jquery.min.js"></script>
<script src="../script.js"></script>
</body>
</html>
\ No newline at end of file
......@@ -173,7 +173,9 @@ the W3C, respectively, the WHATWG.</td>
<tr><td class="datahead">Depends on:</td>
<td class="data"><a href="Core_SC_DOM.html">Core_SC_DOM</a> </td></tr>
<tr><td class="datahead">Used by:</td>
<td class="data"><a href="SC_DOM_Components.html">SC_DOM_Components</a> </td></tr>
</tbody>
......
......@@ -123,6 +123,15 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
Achim D. Brucker
and <a href="http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg">Michael Herzberg</a>
</td>
</tr>
<tr>
<td class="entry">
2020-09-28: <a href="entries/SC_DOM_Components.html">A Formalization of Safely Composable Web Components</a>
<br>
Authors:
Achim D. Brucker
and <a href="http://www.dcs.shef.ac.uk/cgi-bin/makeperson?M.Herzberg">Michael Herzberg</a>
</td>
</tr>
<tr>
<td class="entry">
......
......@@ -87,6 +87,30 @@ 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.</description>
</item>
<item>
<title>A Formalization of Safely Composable Web Components</title>
<link>https://www.isa-afp.org/entries/SC_DOM_Components.html</link>
<guid>https://www.isa-afp.org/entries/SC_DOM_Components.html</guid>
<dc:creator> Achim D. Brucker, Michael Herzberg </dc:creator>
<pubDate>28 Sep 2020 00:00:00 +0000</pubDate>
<description>
While the (safely composable) DOM with shadow trees provide the
technical basis for defining web components, it does 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 safely composable 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. In comparison to the strict
standard compliance formalization of Web Components in the AFP entry
&#34;DOM_Components&#34;, the notion of components in this entry
(based on &#34;SC_DOM&#34; and &#34;Shadow_SC_DOM&#34;) provides
much stronger safety guarantees.</description>
</item>
<item>
<title>The Safely Composable DOM</title>
......@@ -568,27 +592,5 @@ pointwise-bounded family of continuous linear operators from a Banach
space to a normed space is uniformly bounded. Our approach is an
adaptation to Isabelle/HOL of a proof due to A. Sokal.</description>
</item>
<item>
<title>Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems</title>
<link>https://www.isa-afp.org/entries/Attack_Trees.html</link>
<guid>https://www.isa-afp.org/entries/Attack_Trees.html</guid>
<dc:creator> Florian Kammueller </dc:creator>
<pubDate>27 Apr 2020 00:00:00 +0000</pubDate>
<description>
In this article, we present a proof theory for Attack Trees. Attack
Trees are a well established and useful model for the construction of
attacks on systems since they allow a stepwise exploration of high
level attacks in application scenarios. Using the expressiveness of
Higher Order Logic in Isabelle, we develop a generic
theory of Attack Trees with a state-based semantics based on Kripke
structures and CTL. The resulting framework
allows mechanically supported logic analysis of the meta-theory of the
proof calculus of Attack Trees and at the same time the developed
proof theory enables application to case studies. A central
correctness and completeness result proved in Isabelle establishes a
connection between the notion of Attack Tree validity and CTL. The
application is illustrated on the example of a healthcare IoT system
and GDPR compliance verification.</description>
</item>
</channel>
</rss>
This diff is collapsed.
......@@ -282,6 +282,7 @@
<a href="entries/Core_DOM.html">Core_DOM</a> &nbsp;
<a href="entries/Core_SC_DOM.html">Core_SC_DOM</a> &nbsp;
<a href="entries/Shadow_SC_DOM.html">Shadow_SC_DOM</a> &nbsp;
<a href="entries/SC_DOM_Components.html">SC_DOM_Components</a> &nbsp;
<a href="entries/Auto2_Imperative_HOL.html">Auto2_Imperative_HOL</a> &nbsp;
<a href="entries/IMP2_Binary_Heap.html">IMP2_Binary_Heap</a> &nbsp;
<a href="entries/Priority_Search_Trees.html">Priority_Search_Trees</a> &nbsp;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment