Collected research

WebSpec

Lorenzo Veronese, Benjamin Farinier, Mauro Tempesta, Marco Squarcina and Matteo Maffei · arXiv

WebSpec models browser behavior in Coq, compiles security invariants into constrained Horn clauses, and checks generated attack traces with machine-checked proofs. It exposes flaws involving Host cookies and domain relaxation, CSP inheritance for blob URLs, and interactions among browser defenses.

Record

Researcher

Lorenzo Veronese, Benjamin Farinier, Mauro Tempesta, Marco Squarcina and Matteo Maffei

Published by

arXiv

Format

Whitepaper

Topic

Other

In the archive

• Collected in the 2022 research round

Tags

• formal-analysis
• cookie
• same-origin-policy
• csp
• tooling
• owasp-a01-2021
• owasp-a05-2021
• owasp-a07-2021

This page is the archive's own catalogue record. The research is the work of Lorenzo Veronese, Benjamin Farinier, Mauro Tempesta, Marco Squarcina and Matteo Maffei, first published at the original source. Preserved copies are kept so the citation survives its host; this one was last captured on 10 September 2026.