Abstract

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 to reuse components. As it stands, however, the ability to create web components is 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 which users and client-side code (JavaScript) interact with. Being in this central position makes the DOM the most central and critical part of a web browser, 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 research, 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 formalization of the Core DOM in Isabelle/HOL into which we introduce shadow roots. 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 .