论文标题
八卦对差异的弹性弹性的正式驱动分析
Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers
论文作者
论文摘要
Gossipsub是一种新的点对点通信协议，旨在通过控制发送的信息以及通过每个对等计算的分数函数来反对对等的攻击，从而捕获其邻居的正面和负面行为。分数函数取决于可以通过使用gossipsub的应用程序配置的几个参数（权重，帽，阈值）。 Gossipsub的规范是用英语编写的，其对不良同行的攻击的弹性得到了通过使用Golang的实现进行仿真测试的经验支持。 在这项工作中，我们采用一种基本方法来理解八卦对行为不端同龄人攻击的弹性。我们使用ACL2S Theorem Prover构建了Gossipsub的第一个正式模型。我们的模型得到了八卦开发人员的正式认可。它可以使用任意配置的同行模拟任意大小和拓扑的八卦网络，并可以用来证明和反驳有关协议的定理。我们正式化基本的安全属性，指出分数功能是公平的，惩罚不良行为并奖励良好的行为。我们证明得分函数始终是公平的，但是可以以惩罚好行为或忽略不良行为的方式进行配置。使用我们的模型，我们运行八卦，并具有针对两个流行的现实世界应用的特定配置：Filecoin和ETH2.0区块链。我们证明了Filecoin的所有属性。但是，鉴于任何ETH2.0网络（具有任何拓扑和大小）具有任何数量的可能性不佳的同行，我们可以合成攻击，在这些攻击中，这些同伴能够通过永远不会转发主题消息来持续不当行为，同时保持积极的分数，以使他们永远不会被gossipsub从网络中缩小它们。
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.
