Mobile operating systems provide developers with various mobile-to-Web bridges to display Web pages inside native applications. A recently introduced component called Custom Tab (CT) provides an outstanding feature to overcome the usability limitations of traditional WebViews: it shares the state with the underlying browser. Similar to traditional WebViews, it can also keep the host application informed about ongoing Web navigations. In this paper, we perform the first systematic security evaluation of the CT component and show how the design of its security model did not consider cross- context state inference attacks when the feature was introduced. Additionally, we show how CTs can be exploited for fine-grained exfiltration of sensitive user browsing data, violation of Web session integrity by circumventing SameSite cookies, and how UI customization of the CT component can lead to phishing and information leakage. To assess the prevalence of CTs in the wild and the practicality of the mitigation strategies we propose, we carry out the first large-scale analysis of CT usage on over 50K Android applications. Our analysis reveals that their usage is widespread, with 83% of applications embedding CTs either directly or as part of a library. We have responsibly disclosed all our findings to Google, which has already taken steps to apply targeted mitigations, assigned three CVEs for the discovered vulnerabilities, and awarded us $10,000 in bounties. Our interaction with Google led to clarifications of the CT security model in the new Chrome Custom Tabs Security FAQ document.

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.

Over the last two decades, a set of standards published by the W3C, IETF and WHATWG was consolidated to form the Web Platform, a full-fledged application platform as opposed to the initial design of the Web as a set of hyperlinked documents. The current state of the standardization of the Web, fragmented into a multitude of documents maintained by different organizations, complicates the process of reasoning about the security of the platform as a whole. This led to the introduction of vulnerabilities originating from unforeseen interactions between different Web components. This situation stems from the fact that Web specification often include informally-defined or implicit assumptions about the security of other features. In this thesis we argue for the need of a rigorous and formal definition of Web security in terms of invariants that are guaranteed to be valid across the Web platform. In particular, in this work, we study the security mechanisms of the modern Web and formalize them in the form of Web invariants. We propose two methodologies for validating Web invariants on a new model of Web specifications (WebSpec) and on browser implementations (Chromium, Firefox, Safari) that allowed us to discover new inconsistencies and propose sound mitigations. We then focus on application security and study the lesser-known Web threat model of the related domain attacker, measuring its impact on the security of the most popular sites on the Web. Finally, we turn our attention to cookies and their long history of vulnerabilities, discussing new violations of their integrity protections and new attacks enabled by related-domain attackers.

Cookies have a long history of vulnerabilities targeting their confidentiality and integrity. To address these issues, new mechanisms have been proposed and implemented in browsers and server-side applications. Notably, improvements to the Secure attribute and cookie prefixes aim to strengthen cookie integrity against network and same-site attackers, whereas SameSite cookies have been touted as the solution to CSRF. On the server, token-based protections are considered an effective defense for CSRF in the synchronizer token pattern variant. In this paper, we question the effectiveness of these protections and study the real-world security implications of cookie integrity issues, showing how security mechanisms previously considered robust can be bypassed, exposing Web applications to session integrity attacks such as session fixation and cross-origin request forgery (CORF). These flaws are not only implementation-specific bugs but are also caused by compositionality issues of security mechanisms or vulnerabilities in the standard. Our research contributed to 12 CVEs, 27 vulnerability disclosures, and updates to the cookie standard. It comprises (i) a thorough cross-browser evaluation of cookie integrity issues, that results in new attacks originating from implementation or specification inconsistencies, and (ii) a security analysis of the top 13 Web frameworks, exposing session integrity vulnerabilities in 9 of them. We discuss our responsible disclosure and propose practical mitigations.

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.

Firewalls are essential for managing and protecting computer networks. They permit specifying which packets are allowed to enter a network, and also how these packets are modified by IP address translation and port redirection. Configuring a firewall is notoriously hard, and one of the reasons is that it requires using low level, hard to interpret, configuration languages. Equally difficult are policy maintenance and refactoring, as well as porting a configuration from one firewall system to another. To address these issues we introduce a pipeline that assists system administrators in checking if: (i) the intended security policy is actually implemented by a configuration; (ii) two configurations are equivalent; (iii) updates have the desired effect on the firewall behavior; (iv) there are useless or redundant rules; additionally, an administrator can (5) transcompile a configuration into an equivalent one in a different language; and (vi) maintain a configuration using a generic, declarative language that can be compiled into different target languages. The pipeline is based on IFCL, an intermediate firewall language equipped with a formal semantics, and it is implemented in an open source tool called FWS. In particular, the first stage decompiles real firewall configurations for iptables, ipfw, pf and (a subset of) Cisco IOS into IFCL. The second one transforms an IFCL configuration into a logical predicate and uses the Z3 solver to synthesize an abstract specification that succinctly represents the firewall behavior. System administrators can use FWS to analyze the firewall by posing SQL-like queries, and update the configuration to meet the desired security requirements. Finally, the last stage allows for maintaining a configuration by acting directly on its abstract specification and then compiling it to the chosen target language. Tests on real firewall configurations show that FWS can be fruitfully used in real-world scenarios.

Related-domain attackers control a sibling domain of their target web application, e.g., as the result of a subdomain takeover. Despite their additional power over traditional web attackers, related-domain attackers received only limited attention by the research community. In this paper we define and quantify for the first time the threats that related-domain attackers pose to web application security. In particular, we first clarify the capabilities that related-domain attackers can acquire through different attack vectors, showing that different instances of the related-domain attacker concept are worth attention. We then study how these capabilities can be abused to compromise web application security by focusing on different angles, including: cookies, CSP, CORS, postMessage and domain relaxation. By building on this framework, we report on a large-scale security measurement on the top 50k domains from the Tranco list that led to the discovery of vulnerabilities in 887, sites, where we quantified the threats posed by related-domain attackers to popular web applications.

Modern web applications often rely on third-party services to provide their functionality to users. The secure integration of these services is a non-trivial task, as shown by the large number of attacks against Single Sign On and Cashier-as-a-Service protocols. In this paper we present Bulwark, a new automatic tool which generates formally verified security monitors from applied pi-calculus specifications of web protocols. The security monitors generated by Bulwark offer holistic protection, since they can be readily deployed both at the client side and at the server side, thus ensuring full visibility of the attack surface against web protocols. We evaluate the effectiveness of Bulwark by testing it against a pool of vulnerable web applications that use the OAuth 2.0 protocol or integrate the PayPal payment system.

Firewalls are notoriously hard to configure and maintain. Policies are written in low-level, system-specific languages where rules are inspected and enforced along non-trivialcontrol flow paths. Moreover, firewalls are tightly related to Network Address Translation(NAT) since filters need to be specified taking into account the possible translations ofpacket addresses, further complicating the task of network administrators. To simplifythis job, we proposeFireWall Synthesizer(FWS), a tool that decompiles real firewallconfigurations from different systems into an abstract specification. This representationhighlights the meaning of a configuration, i.e., the allowed connections with possible addresstranslations. We show the usage of FWS in analyzing and maintaining a configuration ona simple (yet realistic) scenario and we discuss how the tool scales on real-world policies

Configuring and maintaining a firewall configura-tion is notoriously hard. Policies are written in low-level,platform-specific languages where firewall rules are inspectedand enforced along non trivial control flow paths. Furtherdifficulties arise from Network Address Translation (NAT),since filters must be implemented with addresses translationsin mind. In this work, we study the problem ofdecompilinga real firewall configuration into an abstract specification.This abstract version throws the low-level details away byexposing the meaning of the configuration, i.e., the allowedconnections with possible address translations. The generatedspecification makes it easier for system administrators to checkif:(i)the intended security policy is actually implemented;(ii)two configurations are equivalent;(iii)updates have thedesired effect on the firewall behavior. The peculiarity of ourapproach is that is independent of the specific target firewallsystem and language. This independence is obtained througha generic intermediate language that provides the typicalfeatures of real configuration languages and that separatesthe specification of the rulesets, determining the destiny ofpackets, from the specification of the platform-dependent stepsneeded to elaborate packets. We present a tool that decompilesreal firewall configurations from different systems into thisintermediate language and uses the Z3 solver to synthesizethe abstract specification that succinctly represents the firewallbehavior and the NAT. Tests on real configurations show thatthe tool is effective: it synthesizes complex policies in a matterof minutes and, and it answers to specific queries in just a fewseconds. The tool can also point out policy differences beforeand after configuration updates in a simple, tabular form.