The word blockchain has experienced several ups and downs in recent years, from cutting-edge technological concepts, hot words on the market, to symbols of excessive consumption. Many people believe that blockchain is a tool to solve the pain points of many industries, and has the potential to become a catalyst for the birth of the next generation of "super business carriers".
However, the fabled epic change has not yet come, it has been put under the spotlight. Those who are interested will profit from it, and those who seek profit will pay blindly. Falling into the vortex of public opinion too early will harm and test the technology in the growth stage.
The actual situation today is that there are very few landing applications, there is still a distance between technology and industry connection, and the noise of speculators has overshadowed the "backbone voice" that really cares about technology and the industry. Odaily joins hands with the top new business media 36Kr, top technology leaders and academic elites to discuss how to embrace regulation, promote the industry to get rid of the dross and extract the essence, hand over traffic and voice to those who do things seriously, and use strength to let the blockchain land.
On September 5th, at the blockchain POD conference hosted by Odaily and co-organized by 36Kr Group Strategy, Vilhelm Sjöberg, chief scientist of CertiK, delivered a speech entitled "Towards building fully trustworthy smart contracts and blockchain ecosystem".
secondary title
The following is the transcript of the speech by Vilhelm Sjöberg, Chief Scientist of CertiK:
Hi everyone, I am the Chief Scientist of CertiK and have done a lot of research work on blockchain. Blockchain is a database, and there are many important research topics in terms of technology and trust. Programs are prone to errors in execution, why do they keep making mistakes in execution? How to make the program more reliable? Of course, it's not that people are bad at programming, but because smart contracts are a very special and important part of the blockchain. On the blockchain, once a smart contract is deployed, it cannot be updated. If the deployed smart contract itself has a loophole, hackers may find and exploit this loophole to steal assets. These problems are what we need to avoid.
In order to ensure the safety of the program, some will be manually reviewed, but the time cost is relatively high, and it may cause other problems. Of course, there are also automated tests for auditing, but it won't help you find all the problems. So for blockchain, these solutions are still not good enough.
CertiK uses mathematical methods to prove programs, that is, provides security services for smart contracts and blockchain applications through formal verification.Our concurrent operating system kernel, CertiKOS, can be fully formally proven, and the key technology behind it is "deep specification".
For complex systems, CertiK utilizes deep specification techniques to achieve safety certification.We will layer complex systems, and we will understand what each abstract layer writes, what it does, and what operations it performs, so as to prove whether it meets our correct specifications. If you write some abstraction layer, we can put it together and verify it. Abstraction layers can be linked to each other so that proofs can be integrated. This is the main work we do: to achieve complete distributed smart contract verification through layering and integration.
The kernel of our operating program CertiKOS is divided into several layers and it is possible to verify a large and complex program because we are dealing with one complex function at a time.
This picture shows that we deployed the operating system CertiKOS on the Landshark machine.
We have also cooperated with many experts in the academic circle, and they help us develop such a project. In 2015, Professor Gu Ronghui and Professor Shao Zhong proposed the concept of "deep specification" and verified it. In 2016, we were already selling this ready-to-use product and service to businesses. In 2017, we expanded CertiK to verify smart contracts. So we can also carry out some academic research, and we can carry out formal verification for blockchain.
Next, let me introduce in detail an ongoing research project we have conducted - DeepSEA, which is a programming language for verifying smart contracts.
Before that, let’s talk about what formal verification is to help you understand.Formal verification includes many different techniques for verification, including shallow verification and deep verification.
Shallow-level verification refers to some common verifications, such as the very common integer overflow problem of smart contracts.For relatively shallow verification, we designed the first generation of high-performance smart contract automatic detection engine CertiK AutoScanEngine (CASE), which can help you automatically scan smart contracts and locate vulnerabilities. Distributed verification is completed by refining the contract into different modules. Users can upload the contract to our verification engine to see which one is correct when calling a certain method, or how to deal with it when an error occurs. The whole process achieves maximum machine verification, with very little dependence on manpower.
Next, I want to talk about deep verification.For example, we need to verify any attribute of value, we have to think about how to prove it. There are some local properties, which may apply to a certain architecture, or to a certain method. But in-depth verification, it can be applied to the entire ecosystem of all smart contracts. As described in our white paper, we are able to integrate and combine different chains, including some payment systems, on-chain, off-chain, etc., aiming to provide security for the entire blockchain ecosystem.
Sometimes we not only rely entirely on machines, but also rely on some human intervention. For example, for complex systems, manuals need to write specifications.In CertiK, each system can be divided into different layers. So such a project can help us create a deep verification and specification system. For this purpose, we developed our own language DeepSEA. If you just want to write a contract, you can write it in a personalized language. But for some high-trust contracts, we may not have such a high degree of trust in other aspects. We can of course write it in the language of the EVM, but it's not very trustworthy code. So we launched CertiK's language DeepSEA, which was originally developed to write CertiK, and now it can also be mapped to Ethereum contracts. In addition to being able to generate specifications, it is also possible to use our proven compiler.
There is a contract on the blockchain to make sure that everything we do is correct. So I think it's also a very good demonstration of some of the procedures that we're doing validation at a deep level. If we go deep, there are some steps we need to do to help us verify that our contract is in a correct and good state. So we can write down this concept, and finally through such a series of steps, we can ensure the correctness of the contract.
We have other projects that you can also see online. There are some payment-related projects that we can expand. There are also projects related to smart contracts, compilers, and EVM models. In the following areas listed below, we will help you. If you are interested, you can join us as a partner and keep in touch with us. Thank you all!
