Posted on by Achim D. Brucker, licensed under CC BY-ND 4.0.

Formal Foundations for Provably Safe Web Components

In March, Michael passed successful his PhD viva. Now, his PhD thesis is available online [???]. 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 [???] have been published in international conferences [1, 2]. Moreover, the formalization is available in the Archive of Formal Proofs:

References

1. Brucker, A. D. and Herzberg, M. “A Formal Semantics of the Core DOM in Isabelle/HOLThe 2018 web conference companion (www) (2018): 741–749. doi:10.1145/3184558.3185980, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018

2. Brucker, A. D. and Herzberg, M. “A Formally Verified Model of Web ComponentsFormal aspects of component software (facs) (2020): doi:10.1007/978-3-030-40914-2_3, URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019

3. Brucker, A. D. and Herzberg, M. “The Core DOMArchive of Formal Proofs (2018): URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-dom-2018

4. Brucker, A. D. and Herzberg, M. “A Formalization of Web ComponentsArchive of Formal Proofs (2020): URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-dom-components-2020

5. Brucker, A. D. and Herzberg, M. “Shadow Dom: A Formal Model of the Document Object Model with Shadow RootsArchive of Formal Proofs (2020): URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-shadow-dom-2020

6. Brucker, A. D. and Herzberg, M. “The Safely Composable DOMArchive of Formal Proofs (2020): URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-sc-dom-2020

7. Brucker, A. D. and Herzberg, M. “Shadow Sc Dom: A Formal Model of the Safelty Composable Document Object Model with Shadow RootsArchive of Formal Proofs (2020): URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-shadow-sc-dom-2020

8. Brucker, A. D. and Herzberg, M. “A Formalization of Safely Composable Web ComponentsArchive of Formal Proofs (2020): URL: http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-sc-dom-components-2020