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.
