The majority of blockchain-based systems aim to autonomously
manage financial assets and artifacts of significant monetary
value. Consequently, ensuring their proper operation and
resilience against adversarial behavior are major concerns. In
short, making sure these systems are secure is of paramount
importance.
Consensus protocols
Fundamental to all blockchain-based systems is the correctness of
its underlying consensus protocol. A consensus protocol includes
both:
a mechanism for decentralized selection of one or more block
proposers of a round in the protocol, and
a mechanism for achieving decentralized consensus on a single
block to be appended to the chain.
The problem
Designing and implementing blockchain systems, and consensus
protocols in particular, are intrinsically challenging tasks. As
the protocol evolves, additional interactions are introduced,
making the task of ensuring correctness even more challenging.
Ad-hoc protocol designs, based on informal descriptions, result in
buggy and vulnerable implementations. Another complication is the
gap between protocol designand actual implementation.
Our approach
Our approach to protocol verification is centered around formal
methods. First, we build formal specifications of the protocol’s
design and its properties with the latter representing the
requirements the design is expected to satisfy. Second, we
mathematically verify the protocol’s design meets its expected
requirements.
Moreover, using the K framework, the specification is formal AND
executable. Executable specifications enable running simulations
and animating systems, a useful tool for prototyping and debugging
different designs during the development process, and serve as a
reference implementation for model-based test generation. Finally,
the executable specification is immediately available to
reachability, model checking and theorem proving tools which can
facilitate different forms of formal analysis.
Interested in reviewing the work we’ve done to date? Please visit
the links below.
