ChainSecurity Audit and Verification Service Identifies Vulnerabilities and Certifies the Functional Correctness of Smart Contracts on the Blockchain

In a Nutshell: As blockchain technology evolves to decentralize P2P transactions, smart contracts have emerged as its irreversible guarantors. Smart contracts can enforce those transactions without third-party verification, but not all of them perform as intended or are trustworthy. That’s why Zurich-based ChainSecurity offers personalized audit services and an automated verification platform to ensure the validity of smart contracts. ChainSecurity certification assures users that smart contracts are functionally correct and process transactions in a secure manner.

Although Bitcoin and Ethereum’s Ether token both reside on decentralized blockchains, the Ethereum platform has a broader scope. It not only supports cryptocurrency transactions but also encodes and enforces exchanges of tangible goods and services.

It accomplishes that through smart contracts that are, essentially, programs for managing an exchange under a set of mutually agreed upon terms. If either party violates the terms of a smart contract, the code itself automatically enforces its obligations, performing refunds, for example, without the need for a costly central authority — or lawyers.

The Ethereum platform, which launched six years after Bitcoin in 2015, was one of the first blockchains built to support smart contracts. And Ethereum has emerged as the blockchain world’s smart contract standard.

Because Ethereum validates the contracts on its blockchain, they are as immutable as all other information on its network. But beyond that, users still have to consider the validity of smart contracts themselves. And if the complex code behind them isn’t reliable, bad things could happen.

That’s why ChainSecurity verifies the validity and security of those contracts. And it works with more than 75 major enterprise and blockchain clients to protect more than $1 billion in smart contract assets.

“We ensure that smart contracts work correctly — that the source code of a smart contract matches its intended specification,” Chief Security Officer Petar Tsankov said. “With our ChainSecurity audits — and automated platforms —we formalize the business logic of smart contracts into precise formal specifications and verify that these are correctly implemented in the code.”

And it’s not just a dollars-and-cents issue. According to Tsankov, about $1.4 billion will be lost to blockchain attacks in 2019. But launching a smart contract is a bit like launching a rocket — there’s no turning back once the code goes live.

“The whole point of the blockchain is that smart contracts are set in stone — you can’t change them,” Tsankov said. “That’s why it’s critically important to ensure the correctness of the code is formally verified beforehand. Reputations are at stake — and reputational loss is sometimes even more damaging than the effect of actual funds going missing.”

Turnkey Audit Services Address Coding Discrepancies

Founded in 2017, ChainSecurity is a spin-off of the Secure, Reliable, and Intelligent Systems (SRI) Lab at ETH Zurich. Tsankov is part of a team of about 15 professionals who have expertise in blockchain and smart contract security and privacy.

ChainSecurity’s consultative audit process begins with clients providing a specification for the intended smart contract application. “They describe the functional requirements and what the intended behavior is,” Tsankov said. They also provide the source code of the application.

The ChainSecurity process ensures that the smart contract is valid and reports any issues.

“First, we make sure we understand the specification,” Tsankov said. “For highly critical smart contracts, we’re asked to prove that the code is correct by mathematically formalizing its functional specification — in other words, by unambiguously defining what correctness means with respect to the specification.”

Then comes the process of comparing the formalized spec with the code itself.

“We establish that the specification and the code match,” Tsankov said. “And if they don’t, we report any discrepancies privately to the client. After the issues are corrected, we release a public report certifying that all the issues have been resolved.”

Two technologies contribute to ChainSecurity’s process. First, Securify identifies any known smart contract security vulnerabilities, and then VerX, released in April 2019, goes beyond security vulnerabilities by formally verifying smart contracts with respect to their custom functional specifications.

VerX Automated Verifier Certifies the Functional Requirements of Smart Contracts

In a blog entry, Tsankov wrote that VerX allows auditors and developers to “precisely specify the functional requirements they would like to verify” and to prove smart contracts conform to those provided requirements. That process is essential to establishing a “formal guarantee” of a contract.

“For example, a contract might stipulate that only I can modify my token balance,” Tsankov said. “To formally verify this requirement, you must prove that it will hold for the entire lifetime of the smart contract.”

That means if a fraudulent transaction request is sent, it can’t be executed because the contract stipulates that no one else can change that balance.

However, if there’s no formal guarantee, the code may seem correct, “but you don’t have a mathematical proof that a given event will never occur,” Tsankov said.

In addition to functioning as the backbone of the ChainSecurity audit process, VerX and Securify also comprise a unified platform the company offers directly to developers and enterprises.

In both scenarios, the platform certifies what a contract does as opposed to merely identifying bugs. Common specifications can be reused across contracts, and contracts can be efficiently recertified when code updates correct issues arising during the verification process.

Driving the Mainstream Adoption of Blockchain by Solving Security Issues

By securing and verifying the coding complexities in Ethereum smart contracts, ChainSecurity also helps drive mainstream adoption of blockchain.

“When we certify for the users that the currencies and platforms are secure, we help build trust in blockchain technology as a whole,” Tsankov said.

In fact, in early 2019, ChainSecurity prevented a potentially catastrophic vulnerability from being released into the core Ethereum blockchain. When the company announced it was postponing the Constantinople upgrade, the Ethereum Foundation credited ChainSecurity with identifying code patterns that would have made some smart contracts residing on the network vulnerable to attack following the update.

“About 12 hours before this planned Ethereum upgrade, we had a call with the entire Ethereum team that resulted in an immediate halt,” Tsankov said. “It was a very intense moment, but we prevented a global security issue not just on an application layer but also on the blockchain layer.”

Meanwhile, ChainSecurity is working with other blockchain security providers to standardize terms and procedures for describing different levels of security.

“Standardization is well established in traditional IT security, but in blockchain, it doesn’t exist,” Tsankov said. “There’s an audit, and that’s it. But is it a good audit? Nobody knows.”

Working with industry peers on standards to be released by early 2020 means a new level of assurance in a space that’s still in its relatively early stages of development.

“I would say that’s the most exciting thing — bringing more maturity to the security domain of decentralized applications,” Tsankov said.