Client-side security mechanisms implemented by Web browsers, such as cookie security attributes and the Mixed Content policy, are of paramount importance to protect Web applications. Unfortunately, the design and implementation of such mechanisms are complicated and error-prone, potentially exposing Web applications to security vulnerabilities. In this paper, we present a practical framework to formally and automatically detect security flaws in client-side security mechanisms. In particular, we leverage Web Platform Tests (WPT), a popular cross-browser test suite, to automatically collect browser execution traces and match them against Web invariants, i.e., intended security properties of Web mechanisms expressed in first-order logic. We demonstrate the effectiveness of our approach by validating 9 invariants against the WPT test suite, discovering violations with clear security implications in 104 tests for Firefox, Chromium and Safari. We disclosed the root causes of these violations to browser vendors and standard bodies, which resulted in 8 individual reports and one CVE on Safari

The complexity of browsers has steadily increased over the years, driven by the continuous introduction and update of Web platform components, such as novel Web APIs and security mechanisms. Their specifications are manually reviewed by experts to identify potential security issues. However, this process has proved to be error-prone due to the extensiveness of modern browser specifications and the interplay between new and existing Web platform components. To tackle this problem, we developed WebSpec, the first formal security framework for the analysis of browser security mechanisms, which enables both the automatic discovery of logical flaws and the development of machine-checked security proofs. WebSpec, in particular, includes a comprehensive semantic model of the browser in the Coq proof assistant, a formalization in this model of ten Web security invariants, and a toolchain turning the Coq model and the Web invariants into SMT-lib formulas to enable model checking with the Z3 theorem prover. If a violation is found, the toolchain automatically generates executable tests corresponding to the discovered attack trace, which is validated across major browsers. We showcase the effectiveness of WebSpec by discovering two new logical flaws caused by the interaction of different browser mechanisms and by identifying three previously discovered logical flaws in the current Web platform, as well as five in old versions. Finally, we show how WebSpec can aid the verification of our proposed changes to amend the reported inconsistencies affecting the current Web platform.

In this paper, we analyze the security of programming languages and their execution environments (compilers and interpreters) with respect to Spectre attacks. The analysis shows that only 16 out of 42 execution environments have mitigations against at least one Spectre variant, i.e., 26 have no mitigations against any Spectre variant. Using our novel tool Speconnector, we develop Spectre proof-of-concept attacks in 8 programming languages and on code generated by 11 execution environments that were previously not known to be affected. Our results highlight some programming languages that are used to implement security-critical code, but remain entirely unprotected, even three years after the discovery of Spectre.

Spectre attacks exploit one of the most effective CPU optimization techniques: speculative execution. Instructions executed speculatively can leave traces in microarchitectural structures that attackers can later recover using side-channels, enabling attackers to read arbitrary data. The adoption of speculative execution is widespread across today's CPU architectures, which means billions of devices are susceptible to Spectre attacks. As a result, CPU manufacturers have suggested using serializing instructions that effectively disable speculative execution for a given code segment as mitigation. However, to apply this technique while providing a good balance between security and performance, these vulnerable code snippets, called Spectre gadgets, must be first located. In this thesis, we contribute to the state-of-the-art in Spectre gadget detection. We implement SpecTacle, a tool that extracts potentially vulnerable control flow paths and performs static taint analysis to detect gadgets in such paths while producing a low number of false negatives without sacrificing execution time. Additionally, these potential gadgets are validated through symbolic execution. Finally, we show SpecTacle's efficacy through litmus tests and successfully apply it to a real-world example. In addition to the detection of Spectre-PHT gadgets, we adapt our tool to support the detection of gadgets that leak data through an AVX-based side-channel, not supported by any other state-of-the-art tool. These gadgets are used by NetSpectre, a Spectre variant that enables remote Spectre attacks. Finally, we propose an approach to statically detecting Spectre gadgets in JIT-compiled code, which until now has only been done dynamically, and validate this approach through a proof-of-concept.