Bodei, C., Ceragioli, L., Degano, P., Focardi, R., Galletta, L., Luccio, F., Tempesta, M., & Veronese, L. (2021). FWS: Analyzing, Maintaining and Transcompiling Firewalls. Journal of Computer Security, 29(1), 77–134.
DOI: 10.3233/jcs-200017 Metadata
Abstract: 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.

Squarcina, M., Tempesta, M., Veronese, L., Calzavara, S., & Maffei, M. (2021). Can I Take Your Subdomain? Exploring Same-Site Attacks in the Modern Web. In 30th USENIX Security Symposium (pp. 2917–2934). 30th USENIX Security Symposium, USENIX Security 2021, August 11-13, 2021.
Metadata ⯈Fulltext (preprint)
Abstract: 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.

Veronese, L., Calzavara, S., & Compagna, L. (2020). Bulwark: Holistic and Verified Security Monitoring of Web Protocols. In Computer Security – ESORICS 2020 (pp. 23–41). Springer.
DOI: 10.1007/978-3-030-58951-6_2 Metadata ⯈Fulltext (preprint)
Abstract: 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.

Tempesta, M., Bodei, C., Degano, P., Forcardi, R., Galletta, L., & Veronese, L. (2018). Firewall Management With FireWall Synthesizer. In keiner (p. 1). ITASEC.
Metadata ⯈Fulltext (preprint)
Abstract: 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

Bodei, C., Degano, P., Galletta, L., Focardi, R., Tempesta, M., & Veronese, L. (2018). Language-Independent Synthesis of Firewall Policies. In 2018 IEEE European Symposium on Security and Privacy (EuroS&P). Institute of Electrical and Electronics Engineers ( IEEE ), Austria. IEEE.
DOI: 10.1109/eurosp.2018.00015 Metadata ⯈Fulltext (preprint)
Abstract: 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.