WebSpec, a formal framework for browser security analysis, reveals new cookie attack

January 8, 2022 TH Author

Folks at Technische Universität Wien in Austria have devised a formal security framework called WebSpec to analyze browser security.

And they’ve used it to identify multiple logical flaws affecting web browsers, revealing a new cookie-based attack and an unresolved Content Security Policy contradiction.

These logical flaws are not necessarily security vulnerabilities, but they can be. They’re inconsistencies between Web platform specifications and the way these specs actually get implemented within web browsers.

WebSpec was developed by Lorenzo Veronese, Benjamin Farinier, Mauro Tempesta, Marco Squarcina, Matteo Maffei in an effort to bring rigor to web security through automated, verifiable rule checking rather than manual evaluation.

Browsers, as they explain in an academic paper, “WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms,” have become tremendously complex and continue to become more so as additional components get added to the web platform.

New web platform components undergo compliance testing, the researchers say, but their specifications get reviewed manually by technical experts to understand how new technologies interact with legacy APIs and individual browser implementations.

“Unfortunately, manual reviews tend to overlook logical flaws, eventually leading to critical security vulnerabilities,” the computer scientists explain, pointing to how eight years after the introduction of the HttpOnly flag in Internet Explorer 6 – as a way to keep cookies confidential from client-side scripts – researchers discovered the flag could be bypassed by scripts accessing the response headers of an AJAX request using the getResponseHeader function.

WebSpec uses the Coq theorem proving language to subject the interplay of browsers and their specified behavior to formal testing. It makes browser security a matter of machine-checkable Satisfiability Modulo Theories (SMT) proofs [PDF].

To test for inconsistencies between web specs and browsers, the researchers defined ten “invariants,” each of which describes “a property of the Web platform that is expected to hold across its updates and independently on how its components can possibly interact with each other.”

These invariants or rules represent testable conditions that should hold true, such as “Cookies with the Secure attribute can only be set (using the Set-Cookie header) over secure channels,” as defined in RFC 6265, Section 4.1.2.5.

Of the ten invariants evaluated, three failed.

“In particular, we show how WebSpec is able to discover a new attack on the __Host- prefix for cookies as well as a new inconsistency between the inheritance rules for the Content Security Policy and a planned change in the HTML standard,” the paper explains.

HTTP cookies prefixed with “__Host-” are supposed to only be set by the host domain or scripts included on pages on that domain. WebSpec, however, found an attack to break the related invariant test.

“A script running on a page can modify at runtime the effective domain used for SOP [Same-Origin Policy] checks through the document.domain API,” the paper explains, noting that the mismatch between access control policies in the Document Object Model and the cookie jar lets a script running in an iframe access the document.cookie property on a parent page if both pages set document.domain to the same value.

The researchers note that while the current web platform remains vulnerable to this attack, eventually it won’t be: The document.domain property has been deprecated, meaning future browser updates will omit support, some day.

The authors also used WebSpec to discover an inconsistency with the way Blob objects – objects containing data that can be read as text, binary, or streams using built-in object methods – inherit their Content Security Policy.

Lorenzo Veronese, a doctoral student at TU Wien, raised the issue last July to the working group of the HTML standard, but the different behaviors described in the CSP spec and the policy container explainer have yet to be reconciled.

Antonio Sartori, a Google software engineer, has developed a fix but it has yet to be integrated into the HTML standard.

In any event, the availability of WebSpec as a tool to formally evaluate browser behavior should make life a bit easier for those struggling to maintain sprawling browser codebases. ®