PlatON Completes Another Successful Engagement with Runtime Verification
PlatON Network is pleased to announce the successful completion of its engagement with Runtime Verification. 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 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 Network
PlatON is a next-generation computing architecture that aims to facilitate secure, seamless, and open data sharing for the public good. Through Privacy-Preserving Computation (PPC), PlatON breaks down data silos and enables secure data exchange and collaborative computing for enterprise users. With its open-source data marketplace, PlatON supports and incentivises individuals and businesses looking to both monetise and utilise data resources. PlatON addresses limitations in scalability and security by way of Verifiable Computation and privacy-preserving encryption capabilities, currently enabling real-world usability across a variety of global industries, including advertising, healthcare data management, IoT and decentralised AI, financial services, as well as key management systems.
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.
