Runtime Verification completes another successful engagement with PlatON Networks
Runtime Verification is pleased to announce the successful completion of its engagement with PlatON Networks. This engagement focused on verifying the safety property of PlatON’s Giskard Consensus Protocol using the Coq proof assistant. The Giskard consensus protocol is used to validate transactions and computations in the PlatON network.
Runtime Verification was tasked with describing a model of Giskard in Coq in order to demonstrate how several key safety properties of the protocol are encoded and formally proved. We happily encourage all persons, inside and outside the PlatON community, to read the technical report, the Coq code, as well as the companion Specification of the Giskard Consensus Protocol. The Giskard consensus protocol is central to PlatON Network's distributed networking infrastructure for blockchain-based transactions. Due to the large number of possible scenarios in a distributed system and the possibility of adversarial behavior of network nodes, traditional ways of ensuring consensus protocol safety using only testing is insufficient. The formal verification effort by Runtime Verification provides machine-checked proofs of key safety properties of Giskard across all protocol executions, even in the presence of adversarial nodes. The proofs provide important evidence of the trustworthiness of Giskard as a core component of PlatON Networks' infrastructure, and clarify the basic assumptions of Giskard.
This work is important because it establishes trustworthiness in a key component of PlatON's infrastructure (a component which is very difficult to analyze using only testing and similar methods) and as a secondary benefit, Runtime Verification has clarified the specification and assumptions of the Giskard protocol; the revised specification can serve as a guide for the implementation and validation of Giskard.
Grigore Rosu, the CEO of Runtime Verification and a professor of computer science at the University of Illinois at Urbana-Champaign said: “It was a great pleasure and honor to work with the PlatON team on modeling and formally verifying important aspects of the Giskard protocol in Coq. Not only that we now have higher confidence in the correct operation of the protocol and its implementation, but also, and equally importantly, we have together identified and agreed upon all the assumptions under which the protocol has the desired safety properties. Under the supervision of the PlatON team, we proved those properties using the most rigorous formal verification methods known. The resulting Giskard model can also serve as a trusted, rigorous documentation for future implementations and variations of the protocol. We look forward to the next steps of our collaboration with PlatON!”
James Qu, CTO of PlatON, said the following about the engagement: "It was a great experience to work with RV engineers and scientists on the Griskard proof. I was very impressed by the team's ability to tackle complicated concurrent scenarios and edge cases. I am happy to have RV as part of PlatON's grand plan. Moving forward, there are plenty of opportunities to engage again, namely around protocol modeling and formal verification of smart contracts.”
About PlatON Networks
PlatON Networks is a technology company located in Hong Kong, China and Singapore that has the mission to bring the next-generation Internet Protocol to the world.
About Runtime Verification
Runtime Verification is a technology company located in Urbana, Illinois, USA, where it provides software testing and verification services and products to companies across the blockchain space.