theme:default, class: invert looks good

theme:gradient, class: blue looks good

theme:king looks good

Overall goal of WebSpec: - Secure browsers through secure specifications - secure specifications through formal analysis

Problems that need to be solved Browsers very complex - new APIs - continuous updates - extensive specifications Manual reviews are error-prone - specifications are extensive - subtle interactions between web components ==> Need for systematic approach - automate discovery of logical flaws - machine-checked security proofs

coq: formal proof management system components: cookies, CORS invariants: ex. "If a response from the server contains a security policy, then the browser enforces that specific policy" toolchain: - compiler translates browser model and Web invariants into SMT-lib formulas - then checked by Z3 automated theorem prover

automatically creates minimal counterexamples/attacks attacks tested on real browsers

If you think modeling different browser components is difficult... you're probaly right

ln 2-4 (∀ - evs): This definition says that for every reachable state where the browser handles a network response, i.e., the state is Reachable (3 - Reachable) and the current event is EvResponse (4 - evs) ln 5 (rp_hd...): if the response contains a Set-Cookie header ln 6 (sc_secure): with a cookie that has the Secure attribute ln 7 (url_protocol): then the protocol used to serve the response is HTTPS

four possible outcomes of the z3 theorem prover SAT: counterexample found -> invariant false UNSAT: proof of no counterexample/invariant true - not formally verified - good confidence anyway - formal proof can be manually produced in Coq UNKNOWN: no conclusion - didn't happen in testing LOOP: no termination after exploring a certain number of steps. - When this number becomes high enough, it gives a good intuition that the invariant is likely to hold

if a vulnerability is found, a couple of things happen first, a minimal attack trace is automatically extracted then the trace is translated back to Coq and verified - due to lack of formal verification sequence diagram created for ease of understanding browser testing framework (Web platform tests WPT) used to test the attack on real browsers

Integrity of `__Host-` Cookies: regards who can set cookies with the `__Host-` prefix Interaction with SOP: about the Same-Origin Policy and Content Security Policy Integrity of server-provided policies: if a server provides a security policy, the browser should enforce it Access control on Trusted Types DOM sinks: Trusted Types is a browser feature that allows developers to restrict the sources of JavaScript code that can be executed on a web page - fix proposed and tested/verified with WebSpec Safe policy inheritance: Documents loaded from a local scheme inherit the policy of the source browsing context. - a planned modification will break this invariant - reported to working group of HTML standard

runtime increases exponentially with trace length lemmas serve as shortcuts to interesting configurations lemmas very effective: days ==> minutes

featherweight firefox: implemented a few js features in Coq - has not been used to automatically detect vulnerabilities. - lack of support for most of the Web features considered in our invariants, e.g., CORS, CSP, service workers Models of the Web: - no proofs, only disproving invariants - not current WebSpi: for verification of web protocols Web Infrastructure Model: comprehensive, but not automated Quark: browser with formally verified kernel

Goal - The primary aim of WebSpec is to enhance browser security by automating the analysis of browser specifications and providing secure, machine-checked proofs. Challenges - Browsers are highly complex and frequently updated, making manual reviews error-prone and insufficient for identifying subtle security issues. - WebSpec addresses the need for a systematic, automated approach to discover logical flaws in browser security mechanisms. Toolchain - WebSpec uses the Coq proof assistant to develop a formal browser model and define web security invariants. - The toolchain translates these models and invariants into SMT-lib formulas, which are then checked by the Z3 theorem prover. Results - WebSpec has successfully identified new and existing logical flaws in current and older web platforms. - The framework generates executable tests to validate these findings across major web browsers and proposes solutions to fix identified security inconsistencies. Performance - While the runtime increases exponentially with the length of traces, the use of lemmas as shortcuts significantly reduces analysis time from days to minutes.