For the uninitiated, blockchain represents pure goodness—the bold, the brave, the new wave of the internet—and all that is true to an extent, still, even to the most grizzled veterans in the space. But the reality is that there’s still a lot of work to be done to ensure that blockchain technology has evolved enough to support broader adoption.

Our co-founder, Professor Ronghui Gu at Columbia University, spoke at the Columbia Alumni Weekend Reinvented event and talked about the security issues in blockchain, how formal verification can help solve those issues, and the work that CertiK is doing towards building trustworthy blockchain systems.

You can check out the full webinar on YouTube, or read on for an adapted written version below.

The Beauty of Blockchain

Blockchains, more specifically, ones that use Turing-complete scripting languages, are an exciting technology because they have the potential to fundamentally rework how we trust and transact with each other.

Traditional transactions, like swapping two assets, require us to trust in third parties such as banks or escrow accounts to execute on the transaction on behalf of the two parties. For example, you have to trust that the bank will only release your assets if the other party has turned in their assets.

With blockchain technology, we no longer need to involve that third party when swapping two digital assets—hence, decentralization. Instead, we only need to trust a small program on top of blockchain, which we call a smart contract, to correctly encode the transaction logic.

People deeply believe in the concept of decentralization, wanting to put their trust in a program rather than a third party to manage systems and execute transactions.

But what if the smart contract is wrong? What if the program that we want to trust has a bug, and it’s actually not trustworthy?

The Dark Side of Blockchain

Smart contracts are similar to other computer programs in that they’re susceptible to bugs, which are essentially a mismatch between the programmer’s intention and the actual implementation of code. Bugs occur often in the blockchain world, with the most infamous one resulting in TheDAO “double-spend” attack that resulted in a major loss of $50M worth of crypto assets.

Similarly, earlier this year (2020), a bug in the dForce DeFi smart contract resulted in a loss of $25M.

Clearly, there’s still much work to be done to secure blockchain technology.

From a study conducted by Forbes, more than $4B in crypto assets have been stolen in the first half of 2019—that’s a lot of money!

So how can we prevent these smart contract bugs—and therefore, financial losses—from occurring?

Testing to Prove Software Correctness

One answer to bring more security to blockchain software may be to run more tests. However, as Edsger Dijkstra puts it, “Program testing can be used to show the presence of bugs, but never to show their absence.”

In other words, with testing we can’t realistically prove that bugs don’t exist.

Suppose you’re a programmer, and your intention (i.e., specification) is to calculate the following:

And then you implement the specification with the following code:

To test this program, you would simply run it with a specific input and compare the actual output with the expected output.

In this example, we run the program where x=0 and the result is equal to 1.

We then run the program where x=1, and the result is equal to 4.

Testing can be simple, but unfortunately, this method only gives you a limited list of test cases and does not guarantee the correctness of programs. What if in the implementation of the program, we made a mistake and decided to (incorrectly) implement our code as such:

Recall that the specification (or programmer’s intention) is:

Unfortunately, this buggy program can still pass tests. In the cases where x=0 and x=1, the results are correct even though the program is wrong:

This is the fundamental limitation of the testing approach.

So what other option do we have?

Formal Verification to More Thoroughly Prove Correctness

Many people, including our co-founders Professor Ronghui Gu and Professor Zhong Shao of Columbia University and Yale University, respectively, would propose formal verification. It’s “the only known way to guarantee that a system is free of programming errors.” (See: [seL4 SOSP’09])

Take the previous example, in which the testing method resulted in a couple false positives.

With formal verification, on the other hand, we use mathematical ways to prove that a program is equivalent to a programmer’s intention or specification. Starting from the code, we can apply mathematical steps to essentially break down and rebuild the code to prove that it’s equivalent to the specification.

A step-by-step example is shown below:

Even for a simple program like this, formal verification proofs require pretty significant effort. Imagine the difficulty in using this method to verify complex systems like modern processors, OS kernels, and distributed blockchain systems; some people believe that formal verification for such systems is even impossible and can’t be done.

Formally Verifying Complex Systems with Deep Specification

To address the challenge of formally verifying complex systems, Professor Ronghui Gu and his colleagues hypothesize that the bottleneck of formal verification is not in the proof technique itself; but rather, the issue is in the way we write specifications for formal verification.

They developed a new technique called Deep Specification (nicknamed “DeepSpec”), which allows users to write conversational specifications, and make proofs & verification modular. This way you decompose what would otherwise be a prohibitively cumbersome process into many smaller and easier-to-solve pieces of code, reducing the proof of burden and making the formal verification of complex systems possible.

Using Deep Specification, Ronghui Gu and his colleagues built CertiKOS, the world’s first fully-verified, multiprocessor OS kernel and has been proven to be bug-free and hacker-resistant!

As you can see, this line of work has been talked about in many top-tier technology conferences and is widely recognized as a real breakthrough in formal verification.

Note: The technique was named “Deep Specification” in 2015, a time when deep learning was still popular. This technology was later studied and advocated by the NSF Expedition Project and the broader community. To learn more about this technology, you can research the works of DeepSpec: the science of deep specification.

Securing Smart Contracts with DeepSpec

So how would Deep Specification help solve security issues that exist in blockchain? With the combination of DeepSpec techniques and CertiK’s proprietary technologies, we can do quite a lot to ensure that smart contracts are correct and that there are no instances in which the output of programs differ from intended specifications.

Suppose we have a pretty complex smart contract that has many interdependencies. The visual representation of formally verifying a smart contract is seen below:

The first step is to annotate the source program by adding labels to serve as specification to the smart contract.

Next, we decompose the specification of the smart contract into many small components at various abstraction layers. You can verify each component at the layer it belongs to.

After that, we can further compose all the verified components into a guaranteed, verified smart contract—and then we’re done!

The beauty of this is that you do not need to trust CertiK or the proof technology because it will generate machine-checkable proof objects, also called machine-checkable certificates. You can run this program and check the proofs on your own machine. Smart contracts that are verified by CertiK are called certified smart contracts.

For a demonstration of the CertiK Formal Verification Engine, check out the video at 13:41.

The Genesis and Rise of CertiK

In 2018, CertiK was founded in New York City with the mission to use this DeepSpec technique to make blockchain systems truly trustworthy. We aim to use mathematical ways to protect the crypto world under all conditions!

Fun fact: our logo is a shield (signifying protection and security) with a “for all” mathematical symbol:

Since the launch of CertiK’s verification services in 2018, the company has already had more than 150 enterprise clients, covering a range of industries and types of projects, including cryptocurrency exchanges, stablecoins, public chains, DeFi (which has been very recently popular), smart contracts, wallets, block producers, sports, and gaming apps.

CertiK has verified more than $6B crypto assets since mid-2018. And so far, none of the projects verified by CertiK have been hacked by attackers.

All these achievements aside, blockchain cybersecurity remains a major issue. Since CertiK launched, the number of stolen tokens has only increased significantly.

So what’s the problem? Why hasn’t there been a way to fix these security issues?

The Maturation of the Market and Security Needs

Firstly, even with CertiK’s positive track record, the clients we’ve helped and the crypto assets we’ve secured are just small portions of the total market—and that total market is only growing exponentially. If we’re being realistic, there’s no feasible way we can verify every single project out there.

Secondly, smart contracts are just a single layer within the blockchain technology stack. You also have the compiler, virtual machine, consensus protocol and layer, and nodes (i.e., block producers) to worry about. Any vulnerability in the stack can compromise the entire system and can lead to a loss in tokens.

Blockchain is constantly evolving; its current stage of evolution being paralleled to the internet era of when we relied on ISPs for our email addresses. As we see more companies and projects join the blockchain space and the total market value grow, we’ll likely see more unique and complex use cases that require more robust security needs.

The Solution: CertiK’s Tech Stack

True to our desire to protect the crypto world for all, we recognized a need for an end-to-end solution to this problem, to provide security at every level of the tech stack so that there is nothing left unprotected. We’ve already started work on building out our CertiK Tech Stack, a set of products and techniques that we’ve built at Columbia University and CertiK which includes:

• DeepSEA toolchain
• CertiK native blockchain
• NoOps: CertiKOS for blockchain

DeepSEA Toolchain

With the DeepSEA toolchain, it’ll help prevent bugs during the development phase; you may not even need to run any formal verification or testing to prove program correctness because its correctness is inherent in the programming language itself.

DeepSEA is the first programming language for writing trustworthy smart contracts that reduces insecure features at the programming language level and is encrypted with a strong checker to help reduce bugs during development. It even has a verification engine, which means you can write specifications and run formal verification while developing software. You won’t need to wait until deployment to verify your program. It’s currently available as a v0.9 release on our Github.

The toolchain also has a verified compiler to guarantee that the compilation phase won’t introduce bugs. This is a very large, joint project between Columbia University, Yale University, and CertiK; and is backed by Columbia-IBM Blockchain Center, Columbia Data Science Institute, and other Columbia institutes. It also has support from other organizations such as Ethereum Foundation and Qtum Foundation.

Our goal is for this toolchain to provide trustworthy smart contracts and help build reliable blockchain ecosystems across Hyperledger, Ethereum, and our very own CertiK Chain.

CertiK Native Blockchain

At the blockchain system level, we’ve developed the CertiK Native Blockchain. This is the first security-focused public blockchain that was first introduced in 2018, with the first testnet launched in November 2019 and the full testnet in March 2020.

CertiK Chain provides the CertiK Virtual Machine (also referred to as the CVM), which guarantees that smart contracts are executed correctly. So if you have a DeepSEA smart contract that’s been verified by our verification engine and then compiled by our DeepSEA compiler, then the bytecode of the smart contract is correct. Even with a correct program, you also need to make sure that the virtual machine will correctly execute the bytecode; CVM will make sure that this last step is trustworthy.

The CertiK Chain can also serve as a security enclave for other blockchain platforms. Imagine that a smart contract running on another blockchain is certified; that machine-checkable certificate or proof can be stored on CertiK Chain, and you can check whether the smart contract you want to invoke is correct or not, and is secure or not.

NoOps: CertiKOS for Blockchain

The last piece we offer at the bottom layer of this stack is what we call NoOps. You can think of it as CertiKOS, but for blockchain systems. Recall that CertiKOS is the world’s first fully-verified, multiprocessor OS kernel that’s bug-free and hacker-resistant.

WIth NoOps, we’ll deploy CertiKOS in the blockchain world to help secure all the nodes and block producers. It provides the highest grade of protection for these nodes, ensuring that most will not be hacked and can continuously produce blocks in a good manner.

If you’d like to read more about NoOps, check out our recent product announcement and our detailed product overview.

What’s Next for CertiK

Our overall goal for CertiK is lofty; we want to provide end-to-end cybersecurity solutions for the blockchain world by delivering valuable products to fix or support each of the components in the ecosystem. All these components are built at the labs in Columbia University and at CertiK.

Right now, our team consists of more than 30 researchers and engineers, and more than 20 individuals in BD and Marketing. CertiK was founded and headquartered in New York City, with offices in Seattle, Beijing, and Seoul; and we plan to establish new offices around the world in the near future.

Many of us on the team are actually Columbia University alumni, who joined CertiK after their undergrad, masters, and even PhD programs. We also have other team members from Yale University and other reputable universities, as well as high tech companies.

At CertiK, we believe that our end-to-end solutions, formal verification technique, deep specification technique, and products will be critical towards building trustworthy blockchain systems.

If you’re looking for your next role in blockchain and are eager to join a team of high-performing achievers, make sure to check out our job openings!