BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formal Foundations for Provably Safe Web Components - Michael Herz
 berg\, University of Sheffield
DTSTART:20200303T100000Z
DTEND:20200303T102000Z
UID:TALK140368@talks.cam.ac.uk
CONTACT:Jean Pichon-Pharabod
DESCRIPTION:One of the cornerstones of modern software development that en
 ables the creation of sophisticated software systems is the concept of reu
 sable software components. Especially the fast-paced and business-driven w
 eb ecosystem is in need of a robust and safe way to reuse components. As i
 t stands\, however\, the ability to create web components is spread out\, 
 immature\, and not clearly defined\, leaving much room for misunderstandin
 gs.\n\nTo improve the situation\, we need to look at the core of web brows
 ers:\nthe Document Object Model (DOM). It represents the state of a websit
 e which users and client-side code (JavaScript) interact with. Being in th
 is 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 guar
 antees it provides. A well-established approach for this kind of highly cr
 itical system is to apply formal methods to mathematically prove certain p
 roperties.\n\nIn this research\, we provide a formal analysis of web compo
 nents based on shadow roots\, highlight their short-comings by proving the
 m unsafe in many circumstances\, and propose suggestions to provably impro
 ve 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 impor
 tant DOM API accordingly\, by which we uncover surprising behavior and sho
 rtcomings. Finally\, we propose changes to the DOM standard by altering ou
 r model and proving that the safety of many DOM API methods improves while
  leading to a less ambiguous API.
LOCATION:Computer Lab\, FW26
END:VEVENT
END:VCALENDAR