在 ACL2s 中对 GossipSub 的验证

GossipSub 是一种流行的新型点对点网络协议，旨在通过允许节点仅向动态选择的相邻节点子集（网格邻居）转发消息的完整内容，同时与其余节点闲聊其所见消息，从而快速高效地传播消息。节点根据每个邻居的评分，在本地周期性地决定将其哪些邻居接入或剪除出网格。评分使用评分函数计算，该函数依赖于与节点在网络中性能相关的网格特定参数、权重和计数器。由于 GossipSub 网络的性能最终取决于其节点的性能，一个重要问题随之产生：评分计算机制是否能有效剔除网格中表现不佳甚至故意作恶的节点？我们在配套论文中通过使用我们正式的、官方的且可执行的 ACL2s 模型对 GossipSub 进行推理，对该问题给出了否定回答。基于我们的发现，我们合成并模拟了对 GossipSub 的攻击，这些攻击得到了 GossipSub、FileCoin 和 Eth2.0 开发者的确认，并在 MITRE CVE-2022-47547 中公开披露。在本文中，我们详细描述了我们的模型。我们讨论了设计决策、GossipSub 的安全属性、在我们的模型背景下对这些安全属性的推理、攻击生成以及我们在编写模型时学到的经验教训。