As a distributed system, the operation of blockchain is facilitated by multiple nodes. The properties of these nodes could differ in a variety of ways due to their free and open entries or exits, particularly within a non-licensed public blockchain. The nodes need to communicate with each other by sending messages through the network. They will reach a consensus on a task message and execute it unanimously as per the protocol they follow to ensure the normal operation of the blockchain network.

At least two types of potential errors could occur. The first includes node crash, network failure, packet loss, etc. as a result of unstable hardware performance or unsafe operation environment, with the second mostly owing to malevolent or non-complying nodes, which may lead to the deliberate delay or rejection of messages, invalid blocks, and irrelevant messages sent to other nodes. In the worst-case scenario, malevolent nodes might conspire.

As non-licensed networks, blockchains are incapable of eliminating such errors simply by selecting the so-called “qualified” nodes. Therefore, the implementation of the consensus protocol is necessary because its prudent design could effectively ensure the safety of networks, sustaining stable operations in complex environments.

Viewed as a fundamental and core component for the network, the Giskard consensus protocol has always been taken seriously by PlatON. In addition to the prudent design and intensive testings, PlatON has also invited the internationally recognized team from Runtime Verification Inc. to perform formal verification on the Giskard Consensus protocol, which is on par with academic criteria. During the verification, both PlatON and Runtime Verification adhere to the principle of efficiency, cautiousness, and even meticulousness, performing “high pressure” verification on the Giskard consensus protocol. The results have been published in a report titled Verifying Safety of the Giskard Consensus Protocol in Coq as an open-source on Github.

According to the results, the evidence of machine-verification provided by Runtime Verification through formal verification substantiates that the key safety attributes of the protocol, in turn, empowers PlatON to fully implement it even if there exists any misbehavior node. The results of this project collaboration also offer potent reasons for establishing the reliable Giskard consensus protocol as a core component of PlatON’s network infrastructure, demonstrating clearly the fundamental assumptions of the protocol.

“We are pleased to work with the team from PlatON, and to build modeling and formalize the numerous aspects of the Giskard protocol through COQ,” said Gregory Russell, Runtime Verification CEO and professor of computer science at the University of Illinois at Urbana-Champaign. Today, we are confident of ensuring smooth implementation of the protocol, which means that its safety level has measured up to expectations. After careful discussions with the PlatON team, we decided to adopt the most rigorous formal verification method available, which testifies to the strict security of the protocol. The verification modeling we built could also serve as a reliable and rigorous reference for the implementations and changes of the protocol going forward. We look forward to deepening our partnership with PlatON to build a technology ecosystem.”

Nevertheless, there is no end to the pursuit of technological progress. We have faith in the brilliant and vast community wisdom, which is why we are sincerely inviting members of the community to study the formal verification report provided by Runtime Verification. As we make concerted efforts to study every detail of the protocol, its stable and safe operation will reach new highs.

Websites to check out the verification results:

https://github.com/runtimeverification/giskard-verification/blob/master/report/report.pdf

We encourage discussion and exchange of ideas by community members about the contents and results of the report.

About Runtime Verification

Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses runtime verification-based techniques to perform security audits on virtual machines and smart contracts on public blockchains. It is dedicated to using its dynamic software analysis approach to improve the safety, reliability, and correctness of software systems in the blockchain field. Current customers that Runtime Verification serves include PlatON, IOHK (Cardano’s development company), Ethereum, Algorand, Web3 Foundation, Elrond, Casper Labs, Gnosis, MakerDAO, etc.

For the time being, blockchain safety tests are mostly lightweight static analysis tests (testing only the internal logic of source code), while dynamic analysis test (using the data generated as the codes are compiled and executed) increases coverage to find bugs as opposed to static analysis tests. Runtime Verification is a global leader in formal verification and is capable of directly verifying compiled binary codes. Compared to the formal verification of source codes, this prevents missing bugs that are not easily detected due to malfunctions of the compilers.

About PlatON

PlatON is a blockchain-based infrastructure for the future-oriented privacy computation and distributed economy. It aims to facilitate secure, seamless, and open data sharing for the public good with the combination of blockchain and leading cryptographic technologies. Through its Privacy-Preserving Computation (PPC), PlatON breaks down data silos and enables secure data exchange and collaborative computing for both individuals and enterprise users. With its open-source data marketplace, PlatON supports and incentivises individuals and businesses looking to both monetize and utilize 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 decentralized AI, financial services, as well as key management systems.