Formal Foundations for Provably Safe Web Components

Add to your list(s) Download to your calendar using vCal

• Michael Herzberg, University of Sheffield
• Tuesday 03 March 2020, 10:00-10:20
• Computer Lab, FW26.

If you have a question about this talk, please contact Jean Pichon-Pharabod.

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 .

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Lab, FW26
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.