Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers

Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers

Speakers: Ankit Kumar, PhD Student, Northeastern University; Max von Hippel, PhD Student, Northeastern University; Panagiotis Manolios, Professor, Northeastern University; Cristina Nita-Rotaru, Professor, Northeastern University

Conference: IEEE S&P

YouTube: https://www.youtube.com/watch?v=Ax__H_0B1E

Overview

This talk presents groundbreaking research into the security and resilience of GossipSub, a widely adopted peer-to-peer (P2P) publish-subscribe protocol. Utilized by high-value applications such as Ethereum and Filecoin, which collectively represent hundreds of billions of dollars in market capitalization, GossipSub is critical infrastructure for decentralized networks. The core focus of the research is to formally analyze GossipSub's complex peer scoring function, a mechanism designed to protect the network from misbehaving nodes.

Led by Ankit Kumar, the research team from Northeastern University demonstrates that, despite its sophisticated design, GossipSub, particularly in its Ethereum implementation, harbors significant vulnerabilities. Through the application of formal methods and an industrial-strength theorem prover, the team uncovered specific conditions under which malicious peers can evade detection and remain active within the network, leading to potential network-wide disruptions. This work is pivotal as it represents the first formal model of GossipSub, moving beyond traditional scenario-based testing to provide a rigorous, provable analysis of its security guarantees.

The findings not only pinpoint critical security flaws but also offer concrete insights into the underlying causes, specifically identifying how certain design choices in Ethereum's GossipSub configuration can be exploited. The team’s discovery has been acknowledged by both GossipSub and Ethereum developers, resulting in the registration of a MIT CVE, underscoring the severity and practical implications of the vulnerabilities. This analysis provides a crucial foundation for strengthening the resilience of P2P protocols fundamental to the integrity and operation of major blockchain ecosystems.

Background

▶ Watch: Introduction to GossipSub and its vulnerabilities (0:00)

GossipSub functions as a scalable and dynamic publish-subscribe protocol, essential for the efficient dissemination of messages across decentralized networks. Its design prioritizes three critical considerations: fast delivery of messages, low bandwidth overhead, and security against misbehaving nodes. To achieve fast dissemination and low overhead, GossipSub employs a hybrid message propagation strategy. Full messages are transmitted over mesh connections, represented by solid blue lines in network diagrams, where the degree of connectivity is carefully controlled. Simultaneously, hashes of messages are gossiped outside these primary mesh connections, using dotted lines, to reduce bandwidth. Interested peers can then request full messages based on these gossiped hashes. The network itself is highly dynamic, with peers constantly joining and leaving, and mesh connections adapting to these changes.

The protocol's security mechanism is built around a sophisticated peer scoring function. This function locally tracks and evaluates the behavior of peers based on a variety of metrics. These metrics are categorized as either positive or negative. Positive metrics, such as "time in mesh" and "number of first message deliveries," indicate beneficial behavior, with higher values being more favorable. Conversely, negative metrics, like the "number of invalid messages sent," signify detrimental behavior, where higher values are worse. Applications leveraging GossipSub, such as Ethereum, can also contribute their own metrics, like "P5," which might influence peer scores to prevent the removal of high-value publishers. Some metrics are topic-dependent, meaning they are specific to a particular message topic, while others are topic-independent.

The scoring function itself is notably complex, combining these diverse metrics through a weighted sum. Positive metrics are multiplied by positive weights, and negative metrics by negative weights. These weighted quantities are then summed, potentially multiplied by per-topic weights, and finally subjected to an overall cap. The intent is that a peer's score, if it falls below zero, should trigger the peer's pruning from the mesh. Conversely, peers with higher-than-average scores are promoted or added to meshes.

Previous analyses of GossipSub have primarily relied on scenario-based testing or unit testing. While valuable, these approaches can be insufficient for a protocol as intricate and dynamic as GossipSub, which operates in open, adversarial environments. The inherent complexity of its scoring function, with numerous interacting parameters and dynamic network conditions, makes it prone to subtle, hard-to-discover vulnerabilities through empirical testing alone. This research addresses this gap by being the first to formally model the GossipSub protocol and rigorously reason about its scoring function using formal properties, revealing critical security problems that might otherwise remain hidden.

Key Findings

▶ Watch: Formal modeling of GossipSub using ACL2s (3:37)

The cornerstone of this research is the development of an official, open, formal, fully executable, and cross-validated model of GossipSub using ACL2s, an industrial-strength theorem prover. This model, derived from both the protocol's prose specification and its GoLang implementation, has been recognized by GossipSub's own developers as an official specification. Leveraging this robust formal model, the researchers embarked on a deep analysis of the protocol's security properties, leading to several critical findings.

The primary discovery is that GossipSub, specifically as implemented in Ethereum, is vulnerable to attacks from misbehaving peers. These vulnerabilities allow malicious actors to appear honest while undermining network integrity. The researchers identified these flaws by defining and formally testing four fundamental properties that should ideally govern peer behavior and scoring:

1. Property 1: Non-positive Topic Score Implies Non-positive Overall Score. This property states that if a peer consistently exhibits non-positive behavior within a specific topic (i.e., its topic-based score component for that topic is less than or equal to zero), then its overall score should eventually also drop to non-positive. This ensures that persistent poor behavior in any topic leads to demotion.
2. Property 2: Increasing Negative Metrics Implies Overall Score Drops Below Zero. This property posits that if a peer's negative metrics (e.g., invalid messages) continuously increase over time, its overall score should eventually fall below zero, leading to its removal from the mesh.
3. Property 3: Increasing Positive Metrics Implies Overall Score Increases Above Zero. Conversely, this property states that if a peer's positive metrics (e.g., time in mesh) consistently increase, its overall score should eventually rise above zero, leading to promotion or retention in meshes.
4. Property 4: Identical Metrics Achieve Identical Scores. This is a more trivial property, stating that if two peers exhibit identical behavior (i.e., have identical metric values), they should receive identical scores. This property is inherently satisfied due to the referential transparency of ACL2s as a functional programming language.

Crucially, the team found counter-examples for the first two properties within the Ethereum GossipSub implementation. This means that in Ethereum, it is possible for a peer to have a non-positive topic score (Property 1) or continuously increasing negative metrics (Property 2), yet still maintain an overall score above zero, thus evading detection and pruning. This directly contradicts the intended security guarantees of the scoring function.

In contrast, the Filecoin implementation of GossipSub was found to satisfy all four properties, demonstrating a more resilient configuration. The root cause of Ethereum's vulnerability was identified as a cap applied to the sum of the topic-based components of the score. This cap prevents significant drops in individual topic scores from being fully reflected in the overall score if the aggregated topic-based score remains above the cap threshold. Filecoin, by disabling this specific cap, ensures that even minor misbehaviors are sufficient to bring the overall score below zero, thereby maintaining the intended security posture.

These findings have been confirmed by GossipSub and Ethereum developers, leading to the registration of a MIT CVE (though the specific CVE number was not mentioned in the talk), highlighting the critical nature of these vulnerabilities for the security of major blockchain networks.

Technical Deep Dive

▶ Watch: Key vulnerabilities discovered and confirmed by developers (4:19)

The technical foundation of this research lies in the meticulous formal modeling of GossipSub using ACL2s. ACL2s (A Computational Logic for Applicative Common Lisp) is an industrial-strength theorem prover and a functional programming language built on first-order logic. Its capabilities allow for the creation of executable models that can be rigorously reasoned about and subjected to formal verification. The choice of ACL2s was critical because it provides the precision and expressiveness necessary to model a protocol as complex as GossipSub, capturing its dynamic behavior and intricate scoring logic with high fidelity.

The modeling process involved a dual approach: drawing from the prose specification of GossipSub to understand its high-level design and rules, and simultaneously analyzing the actual GoLang code used in implementations. This allowed the researchers to create an executable model that not only conformed to the theoretical specification but also accurately reflected the behavior of real-world deployments. Conformance tests were performed to ensure that the ACL2s model precisely matched the actual GossipSub protocol, a rigor that led to its recognition as an official specification by the protocol's developers.

ACL2s's ability to perform large-scale simulations was instrumental. The model allowed for fine-grained control over network topology, application parameters, events, and messages. For instance, simulations were conducted on models of real-life Ethereum testnets, based on prior work by Kayat et al., involving thousands of nodes and processing up to 100,000 events. This capability enabled the team to observe the protocol's behavior under various attack scenarios and identify states where the formal properties were violated.

Let's delve deeper into the formal properties and their violations:

The peer scoring function is central to GossipSub's security. It's a complex formula involving:

• Positive metrics: time in mesh, first message deliveries
• Negative metrics: invalid messages, duplicate messages, graft/prune threshold violations
• Application-specific metrics: e.g., P5 from Ethereum.

These metrics are multiplied by various positive and negative weights, summed up, potentially adjusted by per-topic weights, and finally subjected to an overall cap. This multi-layered calculation is designed to dynamically adjust a peer's score based on its observed conduct, promoting good actors and demoting bad ones.

The first two properties were found to have counter-examples in Ethereum's configuration:

1. Property 1: If after some point in time the component of score in a particular topic is continuously less than or equal to zero, then after some point in time the overall score must also drop to less than or equal to zero.

• The formalized ACL2s version of this property declares universally quantified variables for peers (p), topics (top), and topic-based counter values (PTC). It essentially states that if a peer p has non-positive topic score for top (derived from PTC), then p's overall score should be non-positive.
• Counter-example in Ethereum: The research found specific PTC values where a non-positive topic score did not imply a non-positive overall score. During simulations, the network state for Ethereum GossipSub was observed to enter a loop, repeatedly returning to this problematic state, thus disproving the temporal version of this property as well. This means a peer could continuously misbehave in a specific topic without ever being fully penalized.
• Reason for Filecoin's resilience: Filecoin's configuration ensures that the maximum positive score is consistently dominated by minimum penalties due to misbehaviors. Any significant misbehavior is sufficient to bring the overall score below zero, thereby satisfying Property 1.

1. Property 2: If after some point in time the negative metrics of a peer start increasing, then after some point in time it is the case that the overall score for that peer drops and eventually it has to go below zero.

• This property is fundamental for ensuring that consistently malicious behavior, as indicated by rising negative metrics, leads to expulsion.
• Counter-example in Ethereum: This property does not hold for Ethereum. The critical flaw lies in a cap applied to the sum of the topic-based components of the score. If a peer's negative metrics increase, causing its topic-based scores to decrease, but the total sum of these topic-based scores (before being added to other components) remains higher than this cap, then the drop itself is not reflected in the overall score. The cap effectively "absorbs" the negative impact, preventing the overall score from decreasing sufficiently to trigger demotion.
• Reason for Filecoin's resilience: Filecoin disables this specific cap. Consequently, any decrease in topic-based scores due to misbehavior directly impacts the overall score, ensuring that Property 2 is satisfied and malicious peers are appropriately penalized.

The identification of these counter-examples, particularly the role of the scoring function's cap, provides a precise, technical explanation for why Ethereum's GossipSub implementation is vulnerable. It highlights how seemingly minor configuration parameters within a complex scoring algorithm can have profound security implications, allowing misbehaving peers to persist undetected within the network.

Demo / Proof of Concept

▶ Watch: Counter-examples for Ethereum, Filecoin passes properties (6:38)

The research team moved beyond theoretical counter-examples to demonstrate the practical exploitability of these vulnerabilities through the development of attack gadgets. These gadgets are simplified, modular constructions designed to make it easier to understand and build concrete attacks based on the identified flaws in the GossipSub scoring function. They serve as a proof of concept for how a misbehaving peer can leverage the scoring function's weaknesses to evade detection.

An example provided is the AG1 attack gadget. In this scenario, Peer A is attacking Peer V within a single topic. The attack involves Peer A consistently dropping messages in a specific "green" topic that Peer V is subscribed to. According to the expected behavior of GossipSub's security mechanism, Peer V should detect this misbehavior from Peer A, register a negative score against it, and eventually prune A from its mesh connections for that topic. However, using the AG1 gadget, Peer A is configured to exploit the identified vulnerabilities (specifically, the cap on the topic-based score sum in Ethereum). As a result, Peer V is unable to detect this misbehavior from A and is also unable to prune A from its own mesh. Peer A effectively appears as an honest participant despite actively disrupting message delivery.

These attack gadgets are not limited to isolated incidents. The researchers demonstrated that they can be combined to form more sophisticated and impactful attacks, including:

• Eclipse attacks: Where a malicious peer or set of peers isolates a victim peer from the rest of the network, controlling all its incoming and outgoing connections.
• Network partition attacks: Where large segments of the network are effectively cut off from each other, leading to significant disruption in message propagation and consensus.

The team constructed, simulated, and verified these attacks using their robust ACL2s model in the context of Ethereum. This comprehensive validation process confirms that the theoretical vulnerabilities translate into practical exploitation scenarios, enabling misbehaving peers to appear honest and cause widespread disruption. The ability to simulate these complex attacks on real-world Ethereum testnet topologies, processing 100,000 events, underscores the practical relevance and severity of the findings. The overall conclusion is that these attacks can be scaled to create network-wide disruptions, posing a substantial threat to applications like Ethereum that rely on GossipSub for their underlying P2P communication.

Defensive Implications

▶ Watch: Detailed analysis of Property 1 and its counter-example (7:00)

The findings of this research carry significant defensive implications for developers and operators of systems utilizing GossipSub, particularly Ethereum. The primary takeaway is the urgent need to re-evaluate and potentially revise the peer scoring function's parameters and logic, specifically addressing the identified flaw with the topic-based score cap in Ethereum.

1. Revising the Scoring Function Parameters: The most direct defensive action for Ethereum is to adjust or disable the cap on the sum of topic-based scores, mirroring Filecoin's more resilient configuration. This would ensure that negative behavior, even if localized to specific topics, consistently contributes to a peer's overall score reduction, leading to timely demotion and pruning. Careful analysis and tuning of all weights and thresholds within the scoring function are also crucial to prevent similar bypasses.

1. Adopting Formal Verification for Critical Protocols: This work strongly advocates for the broader adoption of formal verification methods for critical P2P protocols like GossipSub. Traditional testing methods proved insufficient to uncover these subtle vulnerabilities. Formal modeling with tools like ACL2s provides a rigorous, mathematical guarantee of security properties, significantly reducing the risk of undiscovered flaws in complex systems. Future protocol designs and updates should integrate formal analysis from the outset.

1. Continuous Monitoring and Anomaly Detection: Even with an improved scoring function, network operators should implement robust continuous monitoring and anomaly detection systems. While the scoring function acts as a first line of defense, sophisticated attackers might still attempt novel evasion techniques. Monitoring tools can track peer scores, message propagation rates, and other network health indicators to identify unusual patterns that might signal an ongoing attack.

1. Layered Security Approach: GossipSub is one layer of a decentralized network's security. Defenders should consider a layered security approach, where other mechanisms (e.g., reputation systems, identity verification, economic incentives/disincentives) complement the P2P layer's security. This provides redundancy and resilience against potential failures in any single security component.

1. Community Awareness and Best Practices: The findings should prompt a broader review across the entire ecosystem of applications using GossipSub. Other projects integrating GossipSub should analyze their specific configurations, especially regarding scoring function parameters and caps, to ensure they are not similarly vulnerable. Sharing best practices and security advisories within the decentralized community is vital for collective defense.

1. Understanding Attack Vectors: The attack gadgets and the demonstration of eclipse and network partition attacks provide valuable insights into potential attack vectors. Defenders can use this information to design specific countermeasures, such as improving peer discovery mechanisms to resist eclipse attacks or enhancing network topology analysis to detect partition attempts early.

By addressing these defensive implications, the resilience of GossipSub-dependent networks, particularly Ethereum, can be significantly enhanced, protecting them from sophisticated, hard-to-detect attacks by misbehaving peers.

Key Takeaways

• GossipSub, a critical P2P protocol used by Ethereum and Filecoin, contains subtle vulnerabilities in its peer scoring function, particularly in Ethereum's implementation.
• Formal methods, specifically using the ACL2s theorem prover, were instrumental in creating an executable model of GossipSub and uncovering these vulnerabilities, demonstrating their superiority over traditional testing for complex protocols.
• Two fundamental security properties related to peer demotion (non-positive topic score implying non-positive overall score, and increasing negative metrics leading to score drop below zero) were found to be violated in Ethereum's GossipSub.
• The root cause of Ethereum's vulnerability is a cap applied to the sum of topic-based scores, which prevents misbehavior from being fully reflected in a peer's overall score. Filecoin's implementation, by disabling this cap, is more resilient.
• Attack gadgets, such as the AG1 attack, demonstrate the practical exploitability of these flaws, allowing misbehaving peers to drop messages and evade detection, potentially leading to eclipse and network partition attacks.
• Defenders in the Ethereum ecosystem must revise the scoring function's parameters, consider adopting formal verification for critical components, and implement robust monitoring to mitigate these identified risks.

About the Speaker(s)

The research presented was a collaborative effort from Northeastern University. Ankit Kumar is a PhD student who presented this work, showcasing his expertise in formal methods and protocol analysis. He collaborated with Max von Hippel, also a PhD student, highlighting the team's strength in this specialized field. Their work was guided by their PhD advisers, Panagiotis Manolios and Cristina Nita-Rotaru, both esteemed professors at Northeastern University. Their collective expertise spans areas such as formal methods, theorem proving, distributed systems, P2P protocols, and network security, underscoring the rigorous academic foundation of this significant contribution to blockchain and P2P security.