Bulwark: Holistic and Verified Security Monitoring of Web Protocols
Lorenzo Veronese, Stefano Calzavara, Luca Compagna

TL;DR
Bulwark is an automatic tool that creates formally verified security monitors for web protocols, providing comprehensive protection at both client and server levels to defend against attacks on third-party web services.
Contribution
It introduces a novel method for generating verified security monitors from pi-calculus specifications, enabling holistic web protocol security.
Findings
Successfully detects vulnerabilities in OAuth 2.0 implementations
Effectively monitors PayPal payment system integrations
Provides full visibility of attack surface
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
