The GossipSub Story
Ethereum's nodes stay in sync by gossiping. Blocks, attestations, sync messages — all of it flows over a publish-subscribe protocol called GossipSub, the workhorse of the libp2p networking stack. I spent a good chunk of my PhD trying to break it — formally, with a theorem prover — and this is the story of what fell out.
It started with a model. My collaborators and I wrote down GossipSub's core logic precisely enough to ask adversarial questions of it: what can a misbehaving peer actually do to an honest one? The answer was uncomfortable. We found attacks in which malicious peers could censor a victim — quietly cutting them off from the conversation while everything looked fine on the surface.
We disclosed what we found to the Ethereum 2.0 client teams in 2022. Adrian Manning from the Lighthouse team responded in detail, acknowledging the censoring attack and describing the scoring-parameter mitigations on their side. Over at Protocol Labs, Vyzo carried our findings to the Eth2 developers, and Yiannis Psaras read the paper and called it “very valuable work.” The disclosure is now recorded as CVE-2022-47547.
The full analysis became our IEEE Symposium on Security and Privacy 2024 paper, “Formal Model-Driven Analysis of Resilience of GossipSub to Sybil Attacks” (with Max von Hippel, Cristina Nita-Rotaru, and Pete Manolios). I also gave a talk about it at IPFS Camp 2022 — the recording is on YouTube.
Finding attacks was only half the story. The other half was proving defenses. We mechanized GossipSub's security argument in the ACL2s theorem prover — machine-checked proofs that the protocol resists the attacks we modeled. That work, “Verification of GossipSub in ACL2s,” won the best student paper award at the ACL2 Workshop 2023.
The Ethereum Foundation noticed. In 2024, the EF's Ecosystem Support Program funded our follow-up project, “Refinement-Based Analysis of P2P Protocols for Ethereum,” through its Academic Grants Round — extending the formal modeling from GossipSub to Ethereum's consensus-layer application logic.
All of it — the attacks, the proofs, the refinement methodology — eventually became my PhD dissertation on refinement-based reasoning of peer-to-peer protocols. These days I work on automated reasoning at AWS, and the latest chapter of the gossip saga is “Lean Gossip,” appearing at DEBS 2026.
Not bad for a protocol whose entire job is small talk.