Formal Foundations for Provably Safe Web Components

One of the cornerstones of modern software development that enables the creation of
sophisticated software systems is the concept of reusable software components. Especially
the fast-paced and business-driven web ecosystem is in need of a robust and safe way of
reusing components. As it stands, however, the concepts and functions needed to create
web components are spread out, immature, and not clearly defined, leaving much room
for misunderstandings.
To improve the situation, we need to look at the core of web browsers: the Document
Object Model (DOM). It represents the state of a website with which users and client-side
code (JavaScript) interact. Being in this central position makes the DOM the most
central and critical part of a web browser with respect to safety and security, so we
need to understand exactly what it does and which guarantees it provides. A well-
established approach for this kind of highly critical system is to apply formal methods to
mathematically prove certain properties.
In this thesis, we provide a formal analysis of web components based on shadow roots,
highlight their short-comings by proving them unsafe in many circumstances, and propose
suggestions to provably improve their safety. In more detail, we build a formalisation
of the Core DOM in Isabelle/HOL into which we introduce shadow roots. Then, we
extract novel properties and invariants that improve the often implicit assumptions
of the standard. We show that the model complies to the standard by symbolically
evaluating all relevant test cases from the official compliance suite successfully on our
model. We introduce novel definitions of web components and their safety and classify
the most important DOM API accordingly, by which we uncover surprising behavior and
shortcomings. Finally, we propose changes to the DOM standard by altering our model
and proving that the safety of many DOM API methods improves while leading to a less
ambiguous API.