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网络，支持任意配置的节点，并可用于证明或证伪协议相关定理。我们形式化定义了基本安全属性，要求评分函数具有公平性、惩罚不良行为并奖励良好行为。研究表明，评分函数始终满足公平性，但存在配置方式可能导致惩罚良好行为或忽略不良行为的情况。通过该模型，我们针对两个真实世界应用（FileCoin和Eth2.0区块链）的具体配置运行GossipSub，验证了所有属性在FileCoin中成立。然而，对于任意拓扑和规模的Eth2.0网络，在存在任意数量潜在恶意节点的情况下，我们能够合成攻击场景：这些节点通过始终不转发主题消息实现持续违规，同时维持正评分从而避免被GossipSub从网络中修剪。