Local mirror of the Archive of Formal Proof (AFP) entry "Core_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.

77 lines
4.3 KiB

  1. To cite the use of this formal theory, please use
  2. Achim D. Brucker and Michael Herzberg. The Safely Composable DOM. In Archive of
  3. Formal Proofs, 2020. http://www.isa-afp.org/entries/Core_SC_DOM.html,
  4. Formal proof development
  5. A BibTeX entry for LaTeX users is
  6. @Article{ brucker.ea:afp-core-sc-dom:2020,
  7. author = {Achim D. Brucker and Michael Herzberg},
  8. title = {The Safely Composable {DOM}},
  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/Core_SC_DOM.html}, Formal proof development},
  14. issn = {2150-914x},
  15. abstract = { In this AFP entry, we formalize the core of the Safely Composable Document Object Model (SC DOM).
  16. The SC DOM improve the standard DOM by strengthening the tree boundaries set by shadow roots: in the
  17. SC DOM, the shadow root is a sub-class of the document class (instead of a base class).
  18. This modifications also results in changes to some API methods (e.g., getOwnerDocument) to return the
  19. nearest shadow root rather than the document root. As a result, many API methods that, when called on
  20. a node inside a shadow tree, would previously ``break out'' and return or modify nodes that are
  21. possibly outside the shadow tree, now stay within its boundaries. This change in behavior makes
  22. programs that operate on shadow trees more predictable for the developer and allows them to make more
  23. assumptions about other code accessing the DOM. },
  24. public = {yes},
  25. classification= {formal},
  26. categories = {websecurity},
  27. pdf = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-core-sc-dom-2020.pdf},
  28. filelabel = {Outline},
  29. file = {http://www.brucker.ch/bibliography/download/2020/brucker.ea-afp-core-sc-dom-outline-2020.pdf},
  30. areas = {formal methods, security, software engineering},
  31. url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-afp-core-sc-dom-2020}
  32. }
  33. An overview of the formalization is given in:
  34. Achim D. Brucker and Michael Herzberg. A Formal Semantics of the Core DOM
  35. in Isabelle/HOL. In The 2018 Web Conference Companion (WWW). Pages 741-749,
  36. ACM Press, 2018. doi:10.1145/3184558.3185980
  37. A BibTeX entry for LaTeX users is
  38. @InProceedings{ brucker.ea:core-dom:2018,
  39. abstract = {At its core, the Document Object Model (DOM) defines a tree-like
  40. data structure for representing documents in general and HTML
  41. documents in particular. It forms the heart of any rendering engine
  42. of modern web browsers. Formalizing the key concepts of the DOM is
  43. a pre-requisite for the formal reasoning over client-side JavaScript
  44. programs as well as for the analysis of security concepts in modern
  45. web browsers. In this paper, we present a formalization of the core DOM,
  46. with focus on the node-tree and the operations defined on node-trees,
  47. in Isabelle/HOL. We use the formalization to verify the functional
  48. correctness of the most important functions defined in the DOM standard.
  49. Moreover, our formalization is (1) extensible, i.e., can be extended without
  50. the need of re-proving already proven properties and (2) executable, i.e.,
  51. we can generate executable code from our specification.},
  52. address = {New York, NY, USA},
  53. author = {Achim D. Brucker and Michael Herzberg},
  54. booktitle= {The 2018 Web Conference Companion (WWW)},
  55. conf_date= {April 23-27, 2018},
  56. doi = {10.1145/3184558.3185980},
  57. editor = {Pierre{-}Antoine Champin and Fabien L. Gandon and Mounia Lalmas and Panagiotis G. Ipeirotis},
  58. isbn = {978-1-4503-5640-4/18/04},
  59. keywords = {Document Object Model, DOM, Formal Semantics, Isabelle/HOL},
  60. location = {Lyon, France},
  61. pages = {741--749},
  62. pdf = {https://www.brucker.ch/bibliography/download/2018/brucker.ea-core-dom-2018.pdf},
  63. publisher= {ACM Press},
  64. title = {A Formal Semantics of the Core {DOM} in {Isabelle/HOL}},
  65. url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-core-dom-2018},
  66. year = {2018},
  67. }