Web Platform Threats: Automated Detection of Web Security Issues With WPT

Web Platform Threats: Automated Detection of Web Security Issues With WPT

Speakers: Pedro Bernardo, PhD Student, TU Wien; Lorenzo Veronese, Valentino Dalla Valle, Stefano Calzavara, Marco Squarcina, Pedro Adão, Matteo Maffei

Conference: USENIX Security '24

YouTube: https://www.youtube.com/watch?v=hKVOLSoKs-w

Overview

The modern web platform is an incredibly complex ecosystem, built upon ever-evolving specifications implemented by various browsers. This talk, presented by Pedro Bernardo and a collaborative team from TU Wien and the University of Padua, addresses the profound challenges of ensuring security and consistency across this intricate landscape. Titled "Web Platform Threats: Automated Detection of Web Security Issues With WPT," the research introduces a novel, automated approach to identify security vulnerabilities within browser implementations by leveraging the existing Web Platform Tests (WPT) suite in conjunction with formally defined web invariants.

The core problem tackled by this work stems from the inherent difficulties in manually reviewing the web platform's natural language specifications for security flaws and subsequently verifying that browser implementations adhere to these security properties. Manual reviews are not only error-prone and slow but also fundamentally unscalable given the rapid growth and increasing complexity of web features and their interactions. This research proposes a robust alternative: an automated pipeline that instruments major web browsers, collects execution traces during WPT runs, and then verifies these traces against a set of predefined security invariants using an SMT solver.

The significance of this research is underscored by its tangible impact. By applying their methodology, the team successfully identified 10 unique vulnerabilities across popular browsers, leading to 2 CVEs (a complete mixed content policy bypass on Safari and a client-side cookie integrity violation on Firefox) and initiating discussions that resulted in changes to the foundational RFC 6265bis cookie specification. This work demonstrates a practical and scalable method for proactively detecting critical security issues in browser implementations, advocating for a shift from reactive security patching to an automated, invariant-driven verification process integrated into the development lifecycle.

Background

▶ Watch: Introduction: Web platform complexity and security challenges (0:00)

The foundation of the web platform lies in its specifications, managed by organizations like the W3C, WHATWG, and IETF. These specifications dictate how web components should function, aiming to ensure consistency across diverse browsers and devices. However, their informal nature, written in natural language, often introduces ambiguity and can lead to unintended interactions between components, creating fertile ground for security vulnerabilities. Web browsers, tasked with implementing these specifications, are colossal software projects, whose sheer size and complexity make security issues an inevitable reality. The challenge then becomes twofold: how to ensure browsers correctly interpret and implement the specifications, and how to do so consistently across different vendors.

Historically, the primary mechanism for verifying browser adherence to specifications has been the Web Platform Tests (WPT). WPT is an extensive, collaborative compliance testing framework developed and maintained by browser developers and specification writers. With approximately 200,000 subtests, WPT offers comprehensive coverage of the web platform, but its focus is strictly on compliance, not security. This means that while WPT can confirm if a browser behaves according to a functional requirement, it doesn't provide explicit security guarantees.

For security, the industry has largely relied on manual reviews by experts whenever new features are introduced or specifications are updated. While invaluable, this manual approach suffers from critical limitations: it is inherently error-prone, slow, and, most significantly, unscalable. As the web platform continues its exponential growth, the number of potential interactions and attack surfaces expands beyond human capacity for comprehensive analysis. Automated approaches are desperately needed to keep pace.

Previous work by the research team explored the concept of web invariants—security properties of the web that are always expected to hold—in conjunction with formal browser models to identify logical flaws within the specifications themselves. This earlier research laid the groundwork for defining these critical security properties. However, the current work shifts focus from finding flaws in the specifications to finding security issues directly within the implementations of web browsers. This transition required developing a methodology capable of observing and analyzing actual browser behavior against these predefined security invariants, moving beyond theoretical models to practical, automated vulnerability detection in real-world software. The core problem this research addresses is the absence of a scalable, automated method to verify that complex browser implementations uphold fundamental security properties, thereby leaving a significant gap in the web's security posture.

Key Findings

▶ Watch: Our approach: invariants, instrumentation, trace verification (4:00)

The research yielded significant and impactful findings, demonstrating the efficacy of automated invariant-based verification for browser security. Out of the nine web invariants defined (seven pertaining to cookies and two to mixed content), the pipeline identified violations for five of them. In total, 101 invariant violations were detected across the instrumented browsers running the entire WPT suite. Through careful analysis and distillation, these violations were consolidated into 10 unique vulnerabilities.

The team promptly reported these vulnerabilities to the affected browser vendors, resulting in eight individual reports that were all acknowledged. Crucially, this work led to the assignment of two CVEs:

• A complete mixed content policy bypass via framing on Safari, which represents a critical vulnerability where insecure resources could be loaded within a secure context, undermining fundamental security guarantees.
• A client-side cookie integrity violation on Firefox, indicating a flaw in how Firefox handled cookie attributes, potentially allowing for unauthorized manipulation or leakage of sensitive cookie data.

Beyond the immediate impact of vulnerability disclosure, the research also initiated important discussions with specification writers and maintainers. These discussions were instrumental, leading to changes in RFC 6265bis, the foundational specification for HTTP cookies. This outcome highlights the profound influence of this work, not only in identifying implementation flaws but also in contributing to the refinement and strengthening of core web standards.

The researchers also provided transparency regarding the accuracy of their pipeline. Out of the 101 initial invariant violations, 15 were identified as false positives. These false positives were primarily attributed to three root causes:

1. Missing Events: This occurred when the instrumentation had insufficient visibility into specific browser components or when browser features/bugs prevented event capture.
2. Incorrectly Ordered Events: Non-determinism in JavaScript event listener scheduling, combined with the timestamp granularity of the instrumentation, sometimes led to out-of-order events or timestamp collisions that were difficult to disambiguate in post-processing.
3. Missing Information: Certain events in some browsers lacked critical parameters. For instance, Safari's webRequest API did not provide the resourceType parameter in request objects, which was essential for reasoning about certain invariants, leading to inaccurate conclusions.

Despite these limitations and the presence of false positives, the researchers expressed high confidence in the correctness and output of their pipeline. They emphasize that the observed number of false positives is manageable and that the approach offers a lightweight yet powerful method for detecting security issues. The fact that real-world, high-impact vulnerabilities were discovered and addressed underscores the practical value and reliability of their methodology.

Technical Deep Dive

▶ Watch: Challenges in defining invariants and browser instrumentation (5:00)

The technical core of this research revolves around a sophisticated pipeline designed to automatically detect security issues in browser implementations using web invariants and the Web Platform Tests (WPT) suite. The overall approach can be broken down into several key stages:

1. Defining Web Invariants: The first critical step involves formally defining a set of web invariants, which are security properties expected to hold true across the web platform. The researchers focused on two mechanisms with clear security implications and relatively compact specifications: cookies and mixed content. An illustrative example of a web invariant is the general case for the mixed content policy, stating that "insecure resources fetched from secure pages should be blocked." In total, nine such invariants were defined: seven related to cookies and two to mixed content. This process is challenging, as it requires deep understanding of often ambiguous natural language specifications and discerning the community's expected behavior.

1. Browser Instrumentation: To observe browser behavior, the team developed a multi-layered, cross-browser instrumentation strategy. This is crucial because relevant events can occur at various levels within a browser's architecture. Their instrumentation primarily consists of a cross-browser extension designed to collect events in JSON format.

• JavaScript API Calls: Content scripts are injected into every iframe to proxy and monitor configurable JavaScript API calls, such as accesses to document.cookie and calls to fetch.
• Cookie Jar Changes: The browser's internal cookie jar modifications are tracked using the cookies extension API.
• Network Activity: Network requests, responses, and redirections are monitored via the webRequest extension API.
• External Proxy: To overcome limitations, particularly with Chrome's Manifest V3, which makes some network data transparent to extensions, an external proxy is employed. This proxy collects additional network information, which is then merged back into the execution traces during post-processing to provide a more complete overview.

1. Trace Collection and Coverage: A significant challenge in automated vulnerability detection is ensuring sufficient code coverage. The researchers addressed this by running their instrumented browsers across the entire WPT test suite. With approximately 200,000 subtests, WPT provides an extensive and diverse set of scenarios, allowing the pipeline to capture a wide range of browser behaviors relevant to the defined invariants. Each WPT run generates an execution trace, which is a sequence of events collected by the instrumentation.

Consider an example trace for a test running on a secure page that sets a secure cookie:

• document.cookie = "a=b; Secure": This would generate a js-set-cookie event, parameterized by the assigned string.
• If the cookie is successfully set in the browser's internal cookie jar, a cookie-jar-set event follows. This event provides detailed information about how the browser parsed the assignment, including the value of attributes like Secure, Domain, Path, and Name.
• Later, document.cookie is accessed to verify the cookie: This triggers a js-get-cookie event, showing that the cookie "a=b" was indeed returned.

This sequence of events, along with their parameters, forms the execution trace.

1. Invariant Verification: Once execution traces are collected, they are lifted into an SMT (Satisfiability Modulo Theories) format. Concurrently, the web invariants, initially defined as security properties, are encoded as implications in first-order logic. An SMT solver is then used to verify these traces against the encoded invariants. The solver attempts to find instances where the trace (representing actual browser behavior) violates an invariant (representing expected secure behavior). Any such violation signals a potential security vulnerability.

The challenges in this deep dive are substantial. Defining web invariants is an open research problem, requiring expert knowledge and careful interpretation of ambiguous specifications. Browser instrumentation is complex, requiring multi-layered approaches to capture events from different browser components, and must contend with inconsistencies in extension APIs (e.g., Chrome's Manifest V3 vs. Firefox/Safari). Furthermore, issues like event ordering non-determinism and timestamp granularity can introduce noise and false positives, necessitating robust post-processing and disambiguation. Despite these hurdles, the systematic integration of WPT for coverage, multi-layered instrumentation, and formal invariant verification through SMT solvers provides a powerful and scalable framework for automated browser security analysis.

Demo / Proof of Concept

▶ Watch: Monitoring JavaScript APIs, cookie jar, and network activity (6:40)

While the talk did not feature a live, interactive demonstration of the full vulnerability detection pipeline, the speakers provided a clear conceptual walkthrough of how their system functions and produces valuable output. This walkthrough served as a compelling proof of concept for the core mechanism of trace collection and event representation, which is fundamental to their invariant verification process.

The conceptual demonstration focused on a simplified, yet illustrative, Web Platform Test scenario:

1. A test runs on a secure page.
2. It attempts to set a cookie with the name "a", value "b", and the Secure attribute (e.g., document.cookie = "a=b; Secure").
3. The test then asserts whether the cookie was successfully set by attempting to retrieve it (e.g., by calling document.cookie and checking for "a=b").

Through this example, the speakers illustrated the execution trace generated by their instrumented browser:

• js-set-cookie event: This event is triggered when the document.cookie assignment occurs. The trace records the exact string assigned, for instance, string: "a=b; Secure".
• cookie-jar-set event: If the browser successfully processes and stores the cookie in its internal cookie jar, this event is recorded. Crucially, it provides parsed information about the cookie's attributes, such as secure: true, domain: "example.com", path: "/", name: "a", and value: "b". This event provides insight into how the browser interprets the cookie assignment. If the cookie were not set (e.g., due to an invalid attribute or insecure context), this event would be absent.
• js-get-cookie event: When document.cookie is accessed to retrieve cookies, this event is logged. The trace shows the cookies that were actually returned by the browser, in this case, cookie: "a=b".

This detailed example effectively showcased how the pipeline captures granular, multi-layered information about browser operations, from JavaScript API interactions to internal cookie jar state changes. By presenting these concrete event types and their associated parameters, the speakers provided a tangible understanding of the data that fuels their invariant verification engine. This conceptual demonstration, though not a live demo, was sufficient to illustrate the pipeline's capability to generate comprehensive behavioral traces necessary for detecting invariant violations and ultimately, security vulnerabilities.

Defensive Implications

▶ Watch: Example: how a test generates an execution trace (7:00)

The findings and methodology presented in this talk carry significant implications for various stakeholders in the web ecosystem, particularly for browser vendors and the broader security community.

For browser vendors, the research offers a compelling case for integrating automated invariant verification directly into their existing development and compliance testing pipelines. The proposed approach is described as "lightweight" and capable of detecting security issues "during development, so before they actually reach production." This proactive security posture is invaluable, as it allows flaws to be identified and remediated much earlier, reducing the cost of fixes and preventing vulnerabilities from impacting end-users. A key defensive recommendation for vendors is to improve support for instrumentation and introspection mechanisms within their browsers. Better, more consistent, and more comprehensive APIs for monitoring internal browser states and events would significantly mitigate the current limitations, such as missing event information or visibility gaps, thereby reducing false positives and increasing the precision and coverage of such security analysis tools.

For the web security community and specification writers, the talk highlights a critical unmet need: the lack of a universally agreed-upon set of web invariants. The speakers explicitly state that "all of this only makes sense if we actually have an agree on a set of web invariants that we want to verify and enforce and we still don't have this as a community and this should be a priority." Establishing a canonical set of security invariants would provide a common ground for evaluating browser security, fostering consistency across implementations, and enabling more effective automated verification efforts. This would require collaborative efforts between security researchers, browser engineers, and standards bodies (W3C, WHATWG, IETF) to formalize security properties that are currently often implicitly understood or informally described.

For web developers, while this research focuses on browser implementation flaws rather than application-level vulnerabilities, it provides a crucial reminder of the inherent complexity and potential fragility of the underlying web platform. Even when following best practices, developers can be exposed to risks due to browser-specific bugs or misinterpretations of specifications, particularly concerning sensitive mechanisms like cookies and mixed content. Developers should stay informed about browser updates, security patches, and any changes to fundamental web standards (like RFC 6265bis for cookies), understanding that the security landscape is dynamic and requires continuous vigilance.

In essence, the defensive implications advocate for a paradigm shift: from primarily reactive security (patching vulnerabilities after discovery in the wild) to a more proactive, automated, and formally-driven approach. By embedding invariant verification into the browser development lifecycle and fostering community-wide agreement on critical security properties, the web platform can significantly enhance its overall resilience against emerging threats.

Key Takeaways

• Automated Invariant Verification is Effective: The research successfully demonstrates that combining web invariants with automated analysis of browser behavior on the Web Platform Tests (WPT) suite is a highly effective method for detecting security vulnerabilities in browser implementations.
• Web Invariants are Crucial Security Definitions: Formalizing "web invariants" (security properties expected to always hold) provides a clear and unambiguous basis for verifying the security posture of complex web components like cookies and mixed content.
• Real-World Impact and CVEs: The methodology led to the discovery of 10 unique vulnerabilities, resulting in 2 CVEs (a Safari mixed content bypass and a Firefox cookie integrity violation) and influencing changes to the RFC 6265bis cookie specification, underscoring the practical significance of the work.
• Scalability for Complex Platforms: Leveraging the extensive WPT suite (200,000 subtests) effectively addresses the challenge of achieving broad coverage for automated analysis, overcoming the limitations of manual security reviews.
• Need for Better Browser Instrumentation: Current limitations in browser instrumentation and introspection mechanisms (e.g., Manifest V3 data transparency, missing API parameters) hinder full visibility and contribute to false positives, highlighting an area for vendor improvement.
• Community Prioritization for Invariant Definition: A critical next step for the web security community is to collectively define and agree upon a standardized set of web invariants to enable more consistent and effective automated security verification across the platform.

About the Speaker(s)

The talk was presented by Pedro Bernardo, a PhD student at TU Wien, who also shares first authorship on the research paper. He introduced the work as a collaborative effort, highlighting his co-first author Lorenzo Veronese. The extensive team contributing to this joint work also includes Valentino Dalla Valle, Stefano Calzavara, Marco Squarcina, Pedro Adão, and Matteo Maffei. This group represents a collaboration primarily between TU Wien (Technische Universität Wien) and the University of Padua, institutions known for their strong research in security and formal methods. Their collective expertise spans areas of web security, browser internals, and formal verification, which is evident in the sophisticated methodology presented in their research.