Hello everyone, I’m Ronghui Gu, an assistant professor at Columbia University Computer Science Department and co-founder at CertiK.
Lots of my friends ask me: Why Bitcoin has a price, why Ethereum has a price, and why blockchain is so popular? Many of you probably receive such questions as well. I believe that the answer of these questions roots in a single word — Trust.
Blockchain ecosystems are built based on trust. Some people call it a “consensus”, some people call it a “belief”. However, the codes written to implement such blockchain ecosystem are not trustworthy due to program bugs.
In the past few years, we have seen many hackers utilizing these bugs: More than hundreds of millions of dollars worth of cryptocurrencies have been stolen. How can we avoid such program bugs? Are there any solutions? Can we rely on testing and white hat techniques?
The answer is probably no.
Edsger Dijkstra mentioned: “Program testing can be used to show the presence of bugs, but never their absence.” White hacker testing methods are for sure useful and needed, but they cannot complete all the tasks. Then what else can we do?
Now some people — including me — will stand out and claim that the Formal Verification is the cure.
According to NSF SFM 2016 Report, Formal methods is the only reliable way to achieve security and privacy in computer systems. We should notice that the NSF report use the term “only”. Through Formal Verification, we use mathematical ways to prove that the code indeed satisfies the specification, which rigorously reflects the design of the developers.
However, here is the question: The Formal Verification concept has been out for a decade long, why there are still many bugs, and why we cannot simply use this technique to save the world?
The reason is: In most cases, those proofs are difficult to conduct.
In 2015, Prof. Zhong Shao, the computer science department chair of Yale University, and I, observed that the bottleneck of this technique is not about the proof technique, but about how to write those specifications. We then introduced a concept called DeepSpec. This concept is basically a way to write compositional specification so that we can decompose a very complex proof of obligations into many smaller and easier-to-solve ones. The magic part is that then you can compose all the proofs back and deliver end to end guarantee. This concept was then widely studied and advocated by a broader community including researchers from Yale, Columbia, MIT, Princeton and UPenn. Three workshops and two summer schools has already been held.
In 2016, we applied this technique to build CertiKOS, the first fully verified concurrent OS kernel in the world. It has already been deployed in critical security fields here in the US.
In 2017, we started to apply this technique in the blockchain domain.
As shown above, we have an example of protecting Smart Contracts via DeepSpec: Here is a very complicated Smart Contract, say, a stable token contract from one of our clients. Based on this contract, we write specifications as labels/notations of the source code. Some of those specifications can also be generated automatically. Next, we decompose the proof obligations into many smaller ones at different abstraction levels. Then, we conduct the proofs locally and compose all the proofs together to deliver a certificate showing that this smart contract is correct in respect to the specifications.
We have one more example about how CertiK detect BeautyChain bugs in their smart contracts. The labels are served as partial specifications of these pieces of smart contracts. When the verification fails, the bugs — the differences between codes and specifications — are detected. The labels also show the counterexamples of the program. Once the bug is fixed and the smart contract passes the verification, it is guaranteed that this smart contract indeed satisfies the specification without any exceptions. Such guarantee of bug’s absence is a major difference from program testing and white hat techniques.
As I mentioned before, some specifications can be generated semi-automatically. Based on that, we also developed an AutoScan platform that scans the security issues for the most popular and running smart contracts in the blockchain systems. This platform was released months ago. During a recent scan which took us several hours, we detected many security bugs in those popular smart contracts that are running right now.
Since May 2018, we have started the collaboration with NEO to build the Formal Verification platform which is customized for NEO ecosystems. This project has already been initialized and we will be releasing demos and products this year.
Here is a summary of our current business. We have launched our verification service for about half a year and have so far conducted more than 160 audits and helped secure more than $1.2 Billion worth of cryptocurrencies. What’s more, we have verified more than 88,000 lines of codes and helped verify & audit some complicated system codes.
Today, if you want to list your token on these major exchanges or launchpads, you need to get security certificates of your code from their collaborated security providers. Our services and techniques have already been adopted by many big players in blockchain domain — We are the only security provider for many top exchanges across the globe such as Binance, OKEx, Huobi and well-known platforms such as NEO, OnTology, Etherscan, ICON, Quarkchain, QTum. We have also provided services for many clients including TrueUSD, crypto.com, Quarkchain, Celer, IoTex. They are very good projects and we are helping them to secure their smart contracts. To request a code audit/security solution from CertiK, please contact bd@certik.io.
Now I would like to talk about a new research project called DeepSEA Blockchain.
Previously, we discussed how to detect bugs and prove the correctness of existing code. Now the questions are: Can we build the bug-free code from scratch? Can we build trustworthy smart contracts from the very beginning?
To answer those questions, we introduced DeepSEA functional and high-level programming language that is difficult for developers to make mistakes. We will provide a certified compiler from DeepSEA high-level languages to many platforms including Hyperledger, EVM, and NEO VEM with the guarantee that the compilation phase won’t introduce any new bugs. This means that if you can do the proofs at a source code level, the guarantee can be propagated all the way down to the byte-code level. Meanwhile, we can also generate the formal specifications from the DeepSEA source code into the Coq Proof assistant. Then you can do proofs in Coq manually or use our library to do the proofs semi-automatically.
DeepSEA Blockchain project is a framework to build cross-platform trustworthy smart contracts in the blockchain ecosystem. It is a joint work between CertiK, Yale University and Columbia University. We have received grant support from IBM through Columbia-IBM research center, Ethereum Foundation, Qtum Foundation and many other platforms. We hope that we can also receive grant support from NEO Foundation and development support from NEO community. All those supports can help us introduce this framework into the next level.
That’s all for today. Thank you.
About CertiK
CertiK is a blockchain and smart contract verification platform founded by top Formal Verification experts from Yale and Columbia University. Incubated by Binance Labs, Certik has strategic partnerships with the world’s leading crypto exchanges such as Binance, OKEx, and Huobi, as well as protocols such as NEO, ICON, and QuarkChain.
CertiK’s formal verification method works differently than traditional testing approaches: rather than working manually, CertiK mathematically proves blockchain ecosystem and smart contracts are hacker-resistant and bug-free at scale. CertiK has secured over $4B in asset value, auditing several projects across all major protocols, including BNB, Terra, Crypto.com, and TUSD.
To request the audit/verification of your smart contracts, please email audit@certik.io or visit certik.io to submit the request.
Twitter: https://twitter.com/CertiKCommunity
Reddit: https://www.reddit.com/r/CertiKOrg/
Telegram: https://t.me/certikorg
LinkedIn: https://www.linkedin.com/company/certik
