Top Mathematics discussions
NishMath
Igor Konnov@Protocols Made Fun
//
Model checking is increasingly recognized as a valuable tool in the design of distributed protocols, offering both technical improvements and measurable benefits. Independent researcher Igor Konnov highlights the importance of embracing various methods like testing, property-based testing, simulation, fuzzing, and model checking to enhance correctness and security in critical systems. The focus on model checking stems from its potential to uncover bugs that have economic impact and demonstrate system properties, ultimately leading to better protocol design and implementation. Real value is added when a technical improvement of a protocol is seen, preferably in a measurable way.
Recently, Konnov published two technical papers demonstrating the application of model checkers in verifying fault-tolerant distributed algorithms. These works include the ChonkyBFT consensus protocol for ZKsync and an exploration of automatic model checking of the Ethereum specification, supported by the Ethereum Foundation. The experience gained from these projects highlights the practical advantages of model checking, especially in identifying potential issues and improving overall system reliability. The ZKsync governance protocol was also the topic of a talk at the DeFi Security Summit 2024.
Specifically, the application of Quint and Apalache model checkers to the ZKsync governance protocol revealed several benefits, including the identification of code fragments that could be improved and the refinement of freezability logic. The process also demonstrated that legal documents could be translated into state invariants, which were used to specify the protocol. This resulted in the creation of over 50 invariants, all tested with randomized simulation and symbolic model checking, showcasing the ability of model checking to contribute to the verification process, even with bounded model checking and randomized symbolic execution.
References :
Recently, Konnov published two technical papers demonstrating the application of model checkers in verifying fault-tolerant distributed algorithms. These works include the ChonkyBFT consensus protocol for ZKsync and an exploration of automatic model checking of the Ethereum specification, supported by the Ethereum Foundation. The experience gained from these projects highlights the practical advantages of model checking, especially in identifying potential issues and improving overall system reliability. The ZKsync governance protocol was also the topic of a talk at the DeFi Security Summit 2024.
Specifically, the application of Quint and Apalache model checkers to the ZKsync governance protocol revealed several benefits, including the identification of code fragments that could be improved and the refinement of freezability logic. The process also demonstrated that legal documents could be translated into state invariants, which were used to specify the protocol. This resulted in the creation of over 50 invariants, all tested with randomized simulation and symbolic model checking, showcasing the ability of model checking to contribute to the verification process, even with bounded model checking and randomized symbolic execution.
Share:
References :
- Protocols Made Fun: This paper delves into the verification of the ZkSync governance protocol using model checkers, including quint and apalache.
- Protocols Made Fun: A discussion on model checking in distributed protocols.
Classification:
- HashTags:
- Target: Protocol
- Product: Formal Methods
- Feature: Model checking
- Type: Research
- Severity: Interesting