Professor Zhong Shao spoke at the 5th Annual Global Summit during Shanghai blockchain week about trustworthy blockchain ecosystems. Professor Shao is the co-founder of CertiK, and the Computer Science department chair at Yale University. The following was his speech:

Good morning, ladies and gentlemen! It’s an honor to be invited to this conference.

Dr. Gavin Wood gave a good explanation of trust and truth — he mentioned that “trust” isn’t always the “truth.” Today’s topic will focus on cybersecurity, and the commonality between cybersecurity and blockchain security.

Everyone knows that security is a pressing issue — and of course, this isn’t just a blockchain problem.

Cybersecurity, in itself, is a huge problem. Data shows that the worldwide market share of cybersecurity will be $167 billion by the end of 2019. By 2024, the market share will increase to $300 billion. With $4 billion worth of cryptocurrencies stolen in the first half of 2019, blockchain security is a topic that must be discussed.

Hackers are driven to blockchains since many store currency-related assets. Therefore, any bug in the underlying OS, hypervisor, and storage system can put entire chains at risk.

Whether the issue stems from the implementation of the consensus protocol or the programming language compiler, both off-chain and cross-chain protocols are at risk. In fact, the programming behind cross-chain protocols can be very complex. The code lays in concurrent and distributed patterns — unlike the sequential pattern that most code follows — making it prone to mistakes.

If multiple users are engaging with the blockchain, how can we tell where the problem lies? Potential issues can pose serious threats, especially in heterogeneous blockchains.

When blockchain first became popular, everyone wanted platforms to be fast, effective, and decentralized. However, when optimized with sophisticated methods like sharding and consensus protocols, companies faced many problems that affected the correctness of the code. Coupled with privacy protection and privacy enforcement regulations, creating a blockchain that was fast, effective, and decentralized was no easy task.

Ten days ago, Jerome Powell, the United States Federal Reserve Chairman, said:

“It’s one thing to be able to counterfeit paper currency. It’s another thing to hack into a cyber currency and create, with a computer, however much of it you want.”

Clearly, security is fundamental to any blockchain ecosystem.

Formal Verification is a solution that many think can solve all blockchain security problems. This technology has actually undergone nearly 40 years of evolution, beginning in the 1960’s when Tony Haoare invented the Hoare logic.

The development of Formal Verification is similar to that of machine learning; the technology touched cyclical periods of intense heat and severe winters. In the 1980’s, many people used Formal Verification to verify code and mathematically prove that programs satisfied their purposes. However, even if the code had been verified, people would not believe the program was truly trustworthy because they would not be able to actually check the results of the verification report.

Formal Verification still has many problems. 15 years ago, we introduced the concept of a Certified Software — a software that could formally verify programs by leveraging machine checkable proof engines that help programmers prove that the code is flawless and bug-free. During this period of time, the software had been called “Proof-Carrying Code.” In order to attach a machine-checkable proof when developing a new blockchain system, you would need to call a third party to verify that there are no related problems.

How is it possible for blockchain to move from truth to trust?

Through math.

Because mathematical proofs are uncontroversial facts accepted worldwide, software built through proofs is built to be secure, trustworthy, and durable. That is, once the code is verified, it becomes a pure digital theorem. Developers have the ability to turn a black box into a verified black box that can be trusted completely.

We have been studying CertiKOS for many years at Yale University. Our goal is to scale up Formal Verification and certified software to create larger systems. We noticed that many engineers write programs in nodes, never thinking about proofs for the future. Most have the same idea — my code runs, so now I should debug in order to fully develop it after.

But such situations don’t exist in complex blockchain systems. Since blockchain protocols are complicated, mathematical proofs must be executed to guarantee security.

In order to fundamentally solve complex problems, we must divide the system into a variety of abstraction layers — also known as black boxes. In reality, anything in the universe is built from step by step processes.

There are many different countries, cities, governments, and communities that make up the Earth. And every time we put a bunch of small things together, we can gradually build one big world.

We believe that software, or any complex systems, should be built step by step, similar to this example mentioned. We used DeepSpec, a technology that allowed us to break down a complicated operating system into 65 layers, to prove that each layer in the system was correct (CertiKOS). This is the first concurrent operating system in the world that is hacker-resistant, and it’s what our team has been working on for a few years now.

While we were doing technology accumulation, we didn’t know that these technologies could generate new applications. When the application of blockchain arose, we realized that this is a killer app, which could perfectly coexist with the DeepSpec technology.

Our intent is to apply Formal Verification methods to all aspects of the blockchain field. CertiK pays attention to many aspects of the blockchain — and not only focuses on security verification of smart contracts and chains, but also the use of Formal Verification technology to build the CertiK Chain. Each line of code built on the CertiK Chain will be verified from the bottom up to ensure accuracy. The tools on the chain will be used to help other teams and other public chains to secure their platforms end-to-end.

About a year and a half ago, Dr. Ronghui Gu, assistant professor at Columbia University, and I jointly established CertiK. Many of our team members are here in the audience today — Dr. Zhaozhong Ni, our Vice President of Engineering, Kai Yan, our Chief Economist, and Bojin Chen, Head of Growth in Beijing.

In addition to the verification-as-a-service used to improve the security of smart contracts, CertiK uses unique machine checkable proof objects to verify code correctness.

Some people will tell you their code is verified — but how can you tell whether they’re telling the truth?

In light of this situation, CertiK provides proofs for you to check yourself. There are many other technologies, such as layer-based technology, smart labels, pluggable proof engines, and certified dApp libraries that have all been applied to this technology.

The entire business plan is designed according to the best practices of the space. And of course, we also offer penetration testing and customized Formal Verification. The details of our services can be found on the company’s official website, certik.io.

What is the mission of the CertiK Chain? We believe that we can build a fully trustworthy blockchain ecosystem with our end-to-end verified system software. We believe that the most important aspect of blockchain is security. If the foundation is built on code that isn’t secure — everything created on top is useless.

What services can the CertiK Chain provide? For software developers, we provide an open, fully trustworthy development ring; for end users, we provide a verified security device; for the community, we make everyone have the peace of mind that their assets are secure and their dApps will not be attacked.

Nodes on the CertiK Chain run on top of our verified OS technology — the CertiKOS. We used the CertiKOS to boot Linux, which is used to guide the implementation of the blockchain consensus, including the contract execution environment. Specifically, CertiKOS will enable Linux to run the full node and validator of the CertiK chain, as well as run the verified VM. We also use DeepSEA, the functional programming language for writing secure smart contracts, to help developers write and generate proofs. Along with machine-verifiable certificates, developers can trust that there are no execution-related errors in the smart contracts written on the CertiK Chain. Our team working on the OS illustrates how you can create a very complex system step by step with Formal Verification.

Traditionally, operating systems run on X86, ARM, RISCV, and other platforms. However, most platforms today use SOC — Heterogeneous SOC. For decentralized heterogeneous blockchain platforms, it is likely that the node is running on Amazon EC2 or Alibaba Cloud. So how can you make CertiKOS run the things mentioned above?

First, we built a generic OS kernel with common components in accordance with architecture and platform abstraction. This practice generally required a machine in the middle to ensure that the code met certain expectations while it ran on the machine. In fact, each system had more than one machine underneath it for these specific cases. There are often many device controllers which allow the code to run on different machines.

How did we verify such code, and how is it scalable?

Verifying such code required sharing resources, such as CPU and Memory, on different machines.

This is similar to the ‘Abstract Layer’ concept — the world can be divided into hundreds of abstract layers with a new black box created at each layer for verification. In this way, a wide variety of complex systems, including decentralized systems, can be verified with a common interface.

And that is how we verified an operating system.

The CertiKOS can be used as a guidance system for distributed blockchain ecosystems to come, and CertiK is proud to lead the blockchain security ecosystem with cutting-edge technology.

Thank you!