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.

Session management is a fundamental component of web applications: despite the apparent simplicity, correctly implementing web sessions is extremely tricky, as witnessed by the large number of existing attacks. This motivated the design of formal methods to rigorously reason about web session security which, however, are not supported at present by suitable automated verification techniques. In this paper we introduce the first security type system that enforces session security on a core model of web applications, focusing in particular on server-side code. We showcase the expressiveness of our type system by analyzing the session management logic of HotCRP, Moodle, and phpMyAdmin, unveiling novel security flaws that have been acknowledged by software developers.

Designing and maintaining firewall configurations is hardalso for expert system administrators. Indeed, policies are made of alarge number of rules and are written in low-level configuration languagesthat are specific to the firewall system in use. To simplify the work ofsystem administrators, some authors of the present paper proposed inprevious work a transcompilation pipeline and a tool that(i)extractsthe meaning of a real configuration by representing it into a tabular form;(ii)refactorsa configuration by removing redundant rules;(iii)portsthepolicy from a firewall system to another. Here, we extend this pipelineby proposing a new characterization that models rulesets and firewallsas functions from packets to transformations. Transformations specifywhich packets are accepted by the firewall and how they are translated.Using this functional characterization we propose two new algorithmsthat simplify the treatment of the pipeline

We present WPSE, a browser-side security monitor for web protocols designed to ensure compliance with the intended protocol flow, as well as confidentiality and integrity properties of messages. We formally prove that WPSE is expressive enough to protect web applications from a wide range of protocol implementation bugs and web attacks. We discuss concrete examples of attacks which can be prevented by WPSE on OAuth 2.0 and SAML 2.0, including a novel attack on the Google implementation of SAML 2.0 which we discovered by formalizing the protocol specification in WPSE. Moreover, we use WPSE to carry out an extensive experimental evaluation of OAuth 2.0 in the wild. Out of 90 tested websites, we identify security flaws in 55 websites (61.1%), including new critical vulnerabilities introduced by tracking libraries such as Facebook Pixel, all of which fixable by WPSE. Finally, we show that WPSE works flawlessly on 83 websites (92.2%), with the 7 compatibility issues being caused by custom implementations deviating from the OAuth 2.0 specification, one of which introducing a critical vulnerability.

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

Cryptography is complex and variegate and re-quires to combine different algorithms and mechanisms in non-trivial ways. This complexity is often source of vulnerabilities.Secure key management is one of the most critical aspects,since leaking a cryptographic key vanishes any advantage ofusing cryptography. In this paper we analyze Java keystores,the standard way to manage and securely store keys in Javaapplications. We consider seven keystore implementations fromOracle JDK and Bouncy Castle, a widespread cryptographiclibrary. We describe, in detail, how the various keystores enforceconfidentiality and integrity of the stored keys through password-based cryptography and we show that many of the implementa-tions do not adhere to state-of-the-art cryptographic standards.We investigate the resistance to offline attacks and we show that,for non-compliant keystores, brute-forcing can be up to threeorders of magnitude faster with respect to the most compliantkeystore. Additionally, when an attacker can tamper with thekeystore file, some implementations are vulnerable to denial ofservice attacks or, in the worst case, arbitrary code execution.Finally we discuss the fixes implemented by Oracle and BouncyCastle developers following our responsible disclosure.

Porting a policy from a firewall system to another is a difficult and error prone task. Indeed, network administrators have to know in detail the policy meaning, as well as the internals of the firewall systems and of their languages. Equally difficult is policy maintenance and refactoring, e.g., removing useless or redundant rules. In this paper, we present a transcompiling pipeline that automatically tackles both problems: it can be used to port a policy into an equivalent one, when the target firewall language is different from the source one; when the two languages coincide, transcompiling supports policy maintenance and refactoring. Our transcompiler and its correctness are based on a formal intermediate firewall language that we endow with a formal semantics.

We survey the most common attacks against web sessions, i.e.,attacks which target honest web browser users establishing an au-thenticated session with a trusted web application. We then reviewexisting security solutions which prevent or mitigate the differentattacks, by evaluating them along four different axes: protection,usability, compatibility and ease of deployment. Based on this sur-vey, we identify five guidelines that, to different extents, have beentaken into account by the designers of the different proposals wereviewed. We believe that these guidelines can be helpful for thedevelopment of innovative solutions approaching web security ina more systematic and comprehensive way

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.

In this article, we survey the most common attacks against web sessions, that is, attacks that target honest web browser users establishing an authenticated session with a trusted web application. We then review existing security solutions that prevent or mitigate the different attacks by evaluating them along four different axes: protection, usability, compatibility, and ease of deployment. We also assess several defensive solutions that aim at providing robust safeguards against multiple attacks. Based on this survey, we identify five guidelines that, to different extents, have been taken into account by the designers of the different proposals we reviewed. We believe that these guidelines can be helpful for the development of innovative solutions approaching web security in a more systematic and comprehensive way.