GossipSub is a popular new peer-to-peer network protocol designed to disseminate messages quickly and efficiently by allowing peers to forward the full content of messages only to a dynamically selected subset of their neighboring peers (mesh neighbors) while gossiping about messages they have seen with the rest. Peers decide which of their neighbors to graft or prune from their mesh locally and periodically using a score for each neighbor. Scores are calculated using a score function that depends on mesh-specific parameters, weights and counters relating to a peer's performance in the network. Since a GossipSub network's performance ultimately depends on the performance of its peers, an important question arises: Is the score calculation mechanism effective in weeding out non-performing or even intentionally misbehaving peers from meshes? We answered this question in the negative in our companion paper by reasoning about GossipSub using our formal, official and executable ACL2s model. Based on our findings, we synthesized and simulated attacks against GossipSub which were confirmed by the developers of GossipSub, FileCoin, and Eth2.0, and publicly disclosed in MITRE CVE-2022-47547. In this paper, we present a detailed description of our model. We discuss design decisions, security properties of GossipSub, reasoning about the security properties in context of our model, attack generation and lessons we learnt when writing it.

翻译：GossipSub是一种新兴的流行点对点网络协议，其设计目标是通过允许节点仅将消息的完整内容转发给动态选择的邻居子集（称为网格邻居），同时以闲谈方式向其余邻居传播其已获取的消息，从而实现消息的快速高效分发。节点基于为每个邻居计算的评分，在本地定期决定从网格中接入或剪除哪些邻居。评分计算依赖于一个评分函数，该函数涉及与节点在网络中的表现相关的网格特定参数、权重和计数器。由于GossipSub网络的性能最终取决于其中节点的表现，一个关键问题随之产生：评分计算机制能否有效从网格中剔除表现不佳甚至蓄意作恶的节点？我们在姊妹篇论文中通过形式化、官方且可执行的ACL2s模型对GossipSub进行了推理，并对这一问题给出了否定回答。基于研究发现，我们综合并模拟了对GossipSub的攻击，这些攻击已得到GossipSub、FileCoin及Eth2.0开发者的确认，并在MITRE CVE-2022-47547中公开披露。本文详细描述了我们的模型，探讨了设计决策、GossipSub的安全属性、基于模型的安全属性推理、攻击生成策略以及建模过程中的经验教训。