Formal Model-Driven Analysis of Resilience of GossipSub to Attacks from Misbehaving Peers
Ankit Kumar, Max von Hippel, Panagiotis Manolios and Cristina Nita-Rotaru.
IEEE Symposium on Security and Privacy (SP) May 2024
Abstract
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.
PDF (365K)