GossipSub is a new peer-to-peer communication protocol designed to counter attacks from misbehaving peers by controlling what information is sent and to whom, via a score function computed by each peer that captures positive and negative behaviors of its neighbors. The score function depends on several parameters (weights, caps, thresholds) that can be configured by applications using GossipSub. The specification for GossipSub is written in English and its resilience to attacks from misbehaving peers is supported empirically by emulation testing using an implementation in Golang. In this work we take a foundational approach to understanding the resilience of GossipSub to attacks from misbehaving peers. We build the first formal model of GossipSub, using the ACL2s theorem prover. Our model is officially endorsed by the GossipSub developers. It can simulate GossipSub networks of arbitrary size and topology, with arbitrarily configured peers, and can be used to prove and disprove theorems about the protocol. We formalize fundamental security properties stating that the score function is fair, penalizes bad behavior, and rewards good behavior. We prove that the score function is always fair, but can be configured in ways that either penalize good behavior or ignore bad behavior. Using our model, we run GossipSub with the specific configurations for two popular real-world applications: the FileCoin and Eth2.0 blockchains. We show that all properties hold for FileCoin. However, given any Eth2.0 network (of any topology and size) with any number of potentially misbehaving peers, we can synthesize attacks where these peers are able to continuously misbehave by never forwarding topic messages, while maintaining positive scores so that they are never pruned from the network by GossipSub.

翻译：GossipSub是一种新型点对点通信协议，旨在通过控制信息发送内容及对象来抵御恶意节点攻击。该协议依赖每个节点计算的评分函数（捕捉其邻居节点的正向与负向行为），其评分函数取决于多个参数（权重、阈值、上限值），这些参数可由采用GossipSub的应用进行配置。GossipSub的规范以英文描述，其对恶意节点攻击的韧性通过基于Golang实现的仿真测试得到经验性验证。本研究采用基础方法探索GossipSub抵御恶意节点攻击的能力，首次利用ACL2s定理证明器构建了GossipSub的形式化模型。该模型获得GossipSub开发团队的官方认可，能够模拟任意规模和拓扑结构的GossipSub网络及任意配置的节点，可用于证明或证伪协议相关定理。我们形式化定义了基础安全属性：评分函数具有公平性，能够惩罚不良行为并奖励良好行为。我们证明评分函数始终满足公平性，但其配置可能导致惩罚良好行为或忽略不良行为。基于该模型，我们采用两种真实应用场景的特定配置运行GossipSub：FileCoin和Eth2.0区块链。结果显示所有属性在FileCoin场景中均成立。然而，对于任意拓扑结构和规模的Eth2.0网络（包含任意数量的潜在恶意节点），我们能够合成攻击方式：这些节点通过永不转发主题消息持续作恶，同时维持正向评分以避免被GossipSub从网络中剪除。