CertiK : Formal Verification Platform for Smart Contracts and Blockchain Ecosystems
1 PREFACE
i) What is CertiK ?
Founded in Silicon Valley & NYC, CertiK is a formal verification framework for building fully trustworthy smart contracts and blockchain ecosystems.It is a formal verification framework to mathematically prove that smart contracts and blockchain ecosystems are bug-free and hacker-resistant. To scale the verification, CertiK developed a layer-based approach to decompose such an otherwise prohibitive proof task into smaller ones. These smaller proof obligations can be encoded in the CertiK transactions and will then be proved and validated by the participants in a decentralized style. Thus, the CertiK ledgers work as certificates to exhibit the end-to-end correctness and security of the verified smart contracts and verified blockchain ecosystems, making them entirely trustworthy.Thus, the CertiK platform’s blockchain is intended to work as certificates to exhibit the end-to-end correctness and security of the verified smart contracts, libraries of decentralized applications (DApp), and the implementations of the blockchain itself. That is also why these are called certified blockchain ecosystems.
Below is the video containing introduction to CertiK
ii) Why CertiK needs to be there ?
A)Blockchain is a rapidly growing space :
a)Blockchain Market Cap : $14 billion (12/2016) → $300 billion (12/2017)
b)Number of Ethereum Smart contracts: 0.1 million (6/2016)→ 1 million (12/2017)
Note : Blockchain Ecosystems are based on trust.
B)Blockchain is Vulnerable!
a)Blockchain Implementations are error-prone.Ethereum Virtual Machine Implementation: 703 open issues, 2186 closed issues (1/15/2018).
b)Smart contracts are open-sourced to hackers and immutable once deployed TheDAO: 1 bug, $50 million lost, fixed by hard fork.
c)Huge attack benefits $630 million has been lost to hackers in 12/2017.
Recently , we saw the bancor issue which led to millions of lost in funds. CertiK could have helped in preventing this . Here is the explanatory article which explains how Certik could have helped .
As the space is growing , more and more hackers are trying to targeting the space leading to more reservations among general mass about blockchain space. This will only increase as the space grows.We need something in this space which can help in minimizing such attacks and CertiK is here for this.
Recently , there was also a bug in ICON smart contract . Though it didn’t lead to any financial loss but if CertiK was there , It could have warned ICON about this . A partnership between ICON and CertiK is also monumental in this direction.Here is how CertiK could have helped.
C) Build Trustworthy Blockchain Ecosystem
2) TEAM
i) Great Minds Behind CertiK
As they say ,a great idea needs a great team to make it a success and CertiK does justice on this front. Looking at the team leaders , you will be full of confidence that this guys can really do justice to such a great project .
ii) Achievements So far
As the team is super awesome , their achievements so far are in sync with their talent. Some of the achievements are listed below:
a) When it comes to research , conference papers in top journals can be a good way of looking into the research . The Certik team has 6 top-tier conference papers. POPL’15, PLDI’16a, PLDI’16b, OSDI’16, APLAS’17, PLDI’18. This only confirms the level of research the team has done.
b) Selected as research highlights by CACM
c)Widely considered as a “breakthrough” . Well it ,indeed, is.
3) INVESTORS AND PARTNERSHIPS
i) Investors And Partners
Top Blockchain funds have invested in Certik .The list is long one.
4)MARKET ANALYSIS AND TECHNOLOGY
i) Technology
There are many ways to improve the reliability and security of system software, but none of them can fully address these challenges introduced by blockchains. Testing is currently the most widely used approach to enhance the trust of systems. Program testing can be used to show the presence of bugs, but never to show their absence. It is obvious that using testing alone cannot eliminate the zero-day vulnerability issues. Formal verification is an alternative approach that aims to mathematically prove that the system is correct with respect to specifications. However, it is still difficult to formally verify practical and complex systems. Traditional verification techniques like the model checking are limited to ensuring functional correctness and suffer from the state explosion problem when dealing with concurrent/decentralized programs.
To address these challenges, one will have to answer the following questions:
1.What to prove?
2.How to scale the proof development?
3.How to let others trust the proofs?
It is believed that the answers to the above questions are rooted in the blockchain itself. This belief has guided the Foundation to develop a one-stop solution, named the CertiK Platform, which provides a powerful set of Certified Kits for building fully trustworthy blockchain ecosystems
- Smart labeling. The CertiK Platform has designed a novel approach to specify DApps/systems using labels. These labels are expressive enough to formally state the desired properties and are compatible with the existing programming languages (e.g., Solidity). By utilizing deep learning techniques with manually established labeled code base for training, the CertiK Platform intends to introduce a framework, named smart labeling, to understand decentralized programs not only at the syntax level but also at the semantics level and then adding proper labels to the source code automatically.
- Layer-based decomposition. The CertiK team is among the first to achieve modular verification by realizing a novel concept, named layered deep specifications . This technique uncovers the insights of layered design patterns and makes it possible to decompose a complex proof task into smaller ones and verify each of them at their proper abstraction level.
- Pluggable proof engine. These decomposed proof obligations are much easier to untangle and can even be solved by some automatic verifiers (e.g., SMT solvers ). To enable extensibility, the CertiK Platform is intended to provide an open protocol such that more advanced solving algorithms can be freely plugged into this system.
- Machine-checkable proof objects. The CertiK Platform constructs mechanized proof objects (or counterexamples) such that these proofs can be quickly checked by anyone using their own machine. These proof objects can be viewed as the “certificates” to the verified programs.
- Certified DApp libraries. In order to improve the code quality and reliability of the entire blockchain community, the CertiK Platform offers a series of certified libraries and plug-ins to the integrated development environment (IDE) for building more trustworthy DApps. The use of these tools will cost a small amounts of CTK as virtual crypto “fuel”, but will provide more assurance during the development time.
- Customized certification services. For DApps/systems (e.g., digital wallets) with high reliability requirements, the CertiK Platform intends to provide customized certification services. In this case, verification experts will help specify/verify the programs and generate a detailed, comprehensive report.
The CertiK ecosystem contains 5 different components with each assigned a specific role.
- Customers : will be code developers or automatic programs that send codes to the system. The sent codes are called “Proof objects” and must be sent along with CertiK tokens (CTK) as a reward.
- Bounty hunters : their tasks are to allocate computing resources to the system as well as to receive proof objects and to broadcast the works within the system. They are entitled to be rewarded with CTK tokens sent by the customers. To be qualified in this role, a certain party must possess a high number of CTK tokens as required by the system.
- Checkers : their responsibilities are to record transactions or verify proof objects submitted by bounty hunters. Bounty hunters will receive the tokens when the checkers confirm the proof objects. Upon confirmation, the checkers will be rewarded with some CTKs.
- Sages : will be connectors of proof engine to CertiK system. The proof engine is an algorithm deployed to find bugs in smart contracts. Sages will be rewarded based on performance of their engines. The bounty hunters will be users of proof engines
- Users : this is suitable for developers who can link library of CertiK to IDE in order to create DApp. Users must pay expenses in CTKs. Users can subscribe to all CertiK Platform’s certified libraries and IDE plug-ins to build their own DApps/systems with some CTKs
These five roles will help to maintain the stability and sustainability of the CertiK ecosystem and can also lead to a natural growth in the importance and value of the CTK token.
CertiK makes use of its native CTK token which is used as a digital fuel across the platform. CTK is a non-refundable functional utility ‘fuel’ which will be used as the unit of exchange between participants on the CertiK Platform. CTK is also used in economic incentives which encourage participants to both contribute and maintain the ecosystem on the CertiK Platform. CTK acts as an integral part of the CertiK Platform, and provides a common unit of exchange that reward users and helps to keep the platform sustainable.
ii) Market Analysis
In the past two years, due to the extreme popular of Bitcoin, the blockchain technology and DApps have become more and more popular. The price skyrocket of virtual currencies derives the exponential growth of the number of smart contracts and other DApps. There are more than one million contracts deployed on Ethereum on January 2018 while this number was only about 0.12 million a year and half ago . Many people believe that blockchain will fundamentally change every aspect of our lives. The development infrastructure is improved daily, and it can be expected that this exponential growth of deployed smart contract will continue in the future. Based on the current growth rate, the total amount of such DApps will probably reach 10 million in the new one to two years. Market size estimation. Most of the existing smart contracts and DApps are dealing with virtual currencies, making their reliability and security highly sensitive. There is a high demand for verification services. Existing smart contract verification service providers charge several thousand to one million dollars for a single service, although their techniques cannot adequately address the challenges mentioned in Sec. 1. It is evident that this kind of verification service is highly profitable and has a high barrier to entry. If only takes one hundred thousand dollars as the average charge for a service, the market for such verification services alone can be as large as one trillion dollars (i.e., 10M × $100K). In addition, the techniques used in the CertiK Platform can cover a broader market than existing service providers thanks to our certified DApp libraries and the IDE plug-ins that provide real-time and interactive verification feedback. These services can reduce the development costs by shortening the development cycle and replacing some of the testing infrastructure. According to our collected data, the testing development and maintenance take about 40% of the total development cost and, a DApp with a good quality service typically takes around one million dollars to build. In this sense, if the CertiK Platform certified libraries and plug-ins replace 20% of the testing infrastructure, it will be a trillion dollar market (i.e., 20% × 40% × 10M × $1M).
iii)CertiK’s competitor
Potential competitors
- Quantstamp proposes a verification protocol for smart contracts written in Solidity. It utilizes the traditional model checking techniques and requires an intensive amount of human effort for reviewing the source code and writing the specification manually. This limits the scalability of their approach.
- Zeppelin is a testing/verification service provider that takes a significant percentage of the existing market. But most of their current verification services are done manually.
- Runtime Verification is a traditional formal verification company and now provide verification services for smart contracts. Similar to the CertiK team, they also have a strong academic background and have proposed one semantics of the EVM, named KEVM. But their work still remains at the research stage.
5) ROADMAP AND CONCLUSION
i) Roadmap
ii) Conclusion
Security in the blockchain space is still a major issue . There are many cases of vulnerability in the smart contracts. The space needs to be safe for bringing more people into it . The investors need a safe environment so that they can feel safe about investing their money . So this space certainly needs a project like CertiK . The importance of CertiK becomes much more as the blockchain keeps on rapidly growing.
I would say i feel this is my one of the top picks for 2018 .
Below is the video containing CertiK Verification Service Demo
6) MORE RESOURCES TO LEARN ABOUT CERTIK
Website : https://CertiK.org
Telegram : https://t.me/certikorg
Medium : https://medium.com/certik
Twitter : https://www.twitter.com/certikorg
Reddit : https://www.reddit.com/r/Certik/
Certik description by Coin Crunch Guys :
https://www.youtube.com/watch?v=qP6mV9iBrbw&t=5s