In March, Michael passed successful his PhD viva. Now, his PhD thesis is available online herzberg:formal-web-components:2020?. The thesis investigates one of the cornerstones of modern software development that enables the creation of sophisticated software systems: the concept of reusable software components for web applications.

The abstract of the thesis entitled “Formal Foundations for Provably Safe Web Components” reads in its entirety:

One of the cornerstones of modern software development that enables the creation of sophisticated software systems is the concept of reusable software components. E 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. vv Parts of the PhD thesis herzberg:formal-web-components:2020? have been published in international conferences [1], [2]. Moreover, the formalization is available in the Archive of Formal Proofs:

• The standard compliant formalization is contained in the following three entries:
  • A Formal Model of the Document Object Model [3]
  • A Formalization of Web Components [4]
  • A Formal Model of the Document Object Model with Shadow Roots [5]
• The improved version of the DOM that is safely composable is formalized in the following three entries:
  • The Safely Composable DOM [6]
  • A Formal Model of the Safely Composable Document Object Model with Shadow Roots [7]
  • A Formalization of Safely Composable Web Components [8]

References