Local mirror of the Archive of Formal Proof (AFP) entry "Shadow_SC_DOM".
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

89 lines
5.3 KiB

  1. To cite the use of this formal theory, please use
  2. Achim D. Brucker and Michael Herzberg. A Formal Model of the Safely Composable Document Object Model
  3. with Shadow Roots. In Archive of Formal Proofs, 2020. http://www.isa-afp.org/entries/Shadow_SC_DOM.html,
  4. Formal proof development
  5. A BibTeX entry for LaTeX users is
  6. @Article{ brucker.ea:afp-shadow-sc-dom:2020,
  7. author = {Achim D. Brucker and Michael Herzberg},
  8. title = {A Formal Model of the Safely Composable Document Object Model with Shadow Roots},
  9. journal = {Archive of Formal Proofs},
  10. month = sep,
  11. year = 2020,
  12. date = {2020-09-28},
  13. note = {\url{http://www.isa-afp.org/entries/Shadow_SC_DOM.html}, Formal proof development},
  14. issn = {2150-914x},
  15. abstract = { In this AFP entry, we extend our formalization of the safely composable DOM with \emph{Shadow
  16. Roots}. Shadow roots are a recent proposal of the web community to support a component-based
  17. development approach for client-side web applications.
  18. Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be
  19. backward compatible, such extensions often result in complex specification that may contain unwanted
  20. subtleties that can be detected by a formalization.
  21. Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our
  22. formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can
  23. be extended without the need of re-proving already proven properties and executable, i.e., we can
  24. generate executable code from our specification. We exploit the executability to show that our
  25. formalization complies to the official standard of the W3C, respectively, the WHATWG. },
  26. public = {yes},
  27. classification= {formal},
  28. categories = {websecurity},
  29. pdf = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-shadow-sc-dom-2020.pdf},
  30. filelabel = {Outline},
  31. file = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-shadow-sc-dom-outline-2020.pdf},
  32. areas = {formal methods, security, software engineering},
  33. url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-shadow-sc-dom-2020}
  34. }
  35. An overview of the formalization is given in:
  36. Achim D. Brucker and Michael Herzberg. A Formally Verified Model of
  37. Web Components. In Formal Aspects of Component Software (FACS).
  38. Lecture Notes in Computer Science (12018), Springer-Verlag, 2020.
  39. http://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019
  40. A BibTeX entry for LaTeX users is
  41. @InCollection{ brucker.ea:web-components:2019,
  42. abstract = {The trend towards ever more complex client-side web applications is unstoppable. Compared to
  43. traditional software development, client-side web development lacks a well-established component
  44. model, i.e., a method for easily and safely reusing already developed functionality. To address this
  45. issue, the web community started to adopt shadow trees as part of the Document Object Model (DOM):
  46. shadow trees allow developers to "partition" a DOM instance into parts that should be safely
  47. separated, e.g., code modifying one part should not, unintentionally, affect other parts of the DOM.
  48. While shadow trees provide the technical basis for defining web components, the DOM standard neither
  49. defines the concept of web components nor specifies the safety properties that web components should
  50. guarantee. Consequently, the standard also does not discuss how or even if the methods for modifying
  51. the DOM respect component boundaries. In this paper, we present a formally verified model of web
  52. components and define safety properties which ensure that different web components can only interact
  53. with each other using well-defined interfaces. Moreover, our verification of the application
  54. programming interface (API) of the DOM revealed numerous invariants that implementations of the DOM
  55. API need to preserve to ensure the integrity of components.},
  56. keywords = {Web Component, Shadow Tree, DOM, Isabelle/HOL},
  57. location = {Amsterdam, The Netherlands},
  58. author = {Achim D. Brucker and Michael Herzberg},
  59. booktitle = {Formal Aspects of Component Software (FACS)},
  60. language = {USenglish},
  61. publisher = pub-springer,
  62. address = pub-springer:adr,
  63. series = s-lncs,
  64. number = 12018,
  65. isbn = {3-540-25109-X},
  66. doi = {10.1007/978-3-030-40914-2_3},
  67. editor = {Sung-Shik Jongmans and Farhad Arbab},
  68. pdf = {http://www.brucker.ch/bibliography/download/2019/brucker.ea-web-components-2019.pdf},
  69. title = {A Formally Verified Model of Web Components},
  70. classification= {conference},
  71. areas = {formal methods, software},
  72. year = 2020,
  73. public = {yes},
  74. url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-web-components-2019}
  75. }