Ethereum uses formal verification to improve the security of smart contracts

Baozou Comment : At the Ethereum Developer Conference (Devcon2) held in Shanghai this month, formal verification became a hot topic in the community, attracting great attention and heated discussions. As a supplement to the solidity language, it has the potential to strengthen the security of blockchain smart contracts and prevent similar incidents like The DAO from happening. However, there are still some technical difficulties to be overcome, and it is not a panacea for all problems, but its potential has been highly recognized by the developer community.

Translation: Annie_Xu

Recently, a new buzzword has emerged in the blockchain field - formal verification.

This phrase, which refers to the use of mathematical algorithms to verify software programs, has frequently appeared in media reports. But last week's Blockchain Summit in Shanghai gave us some hints that the importance of formal verification should grow as both smart contracts and blockchains face security issues.

Multiple sessions at the Ethereum developer conference Devcon2 showed that the developer community is clearly welcoming this new program that can help Ethereum coders. The concept has increased confidence in the Ethereum protocol and the proof-of-stake blockchain project.

The DAO was the largest smart contract project to date on the decentralized application development platform, and its sudden collapse certainly explains why the concept has gained traction.

Although formal verification may seem complex, it can be simply understood as an application in Ethereum. Coders now basically write smart contracts in the solidity language, which is then compiled into bytecode for the Ethereum Virtual Machine (EVM), distributed to the nodes of the network, and executes the code program.

Formal verification can be seen as an objective way of ensuring that different network elements receive instructions and then execute them as intended on behalf of the user.

Grant Passmore, founder of Aesthetic Integration, saw an opportunity to promote this technology and released Imandra Contracts, a formal verification platform for blockchain and smart contracts, at Devcon2.

Grant Passmore

He suggested at the conference that Ethereum could serve as a “paradise” for formal verification, given the community’s goals and the heavy responsibility placed on the code.

“The Ethereum community is unique. After The DAO, we discovered the necessity of strong computer engineering. It is impossible to make a smart contract look like a web application.”

Another speaker, Cornell's Philip Daian, discussed the methodology more broadly, stating that he believes formal verification can help Ethereum solve major problems.

“This will be an important building block and I’m looking forward to setting standards through ethereum and sharing this experience.”

Training wheels

Financial companies have been emphasizing smart contract languages ​​recently, so integrating Solidity and formal verification has become the hottest topic recently.

Solidity was developed for the Ethereum platform and has been criticized for being untested and difficult to write in. These issues were amplified by the lack of a code base for the language compiler and the collapse of The DAO.

Therefore, Solidity creator Christian Reitweissner admitted that formal verification should be used to help Ethereum coders find vulnerabilities more effectively.

In the future, he said, smart contract developers could use formal verification to determine if there are loopholes in their work. They could also use the tool to determine if the result of adding two averages is better than the result assigned by the compiler.

“It’s possible that this could happen, and formal verification can automatically detect it. You can detect it early and make adjustments to the smart contract.”

Reitweissner said the Solidity team has been exploring how to integrate formal verification, and last October developed a prototype to study how the Why3 toolkit could help achieve this goal, although the product has not yet been made public for all of Solidity.

Proving Ground

The summit also focused on discussing how to use Ethereum to explore how to apply formal verification to the financial industry.

Passmore said that he has been working with financial institutions to explore ways to integrate the system since 2014. Customers have already started some applications, such as dark pools, whose fairness has been criticized by traders.

Passmore said the ethereum community could push for smart contract adoption.

“When we first started working with banking clients, many of them showed great interest in this area, but we were concerned about the correctness of the smart contracts.”

The growth of formal verification also attracted Yoichi Hirai, a formal verification engineer currently working at the Ethereum Foundation; he had been interested in the technology since he was a researcher at cybersecurity leader FireEye.

Hirai said at the meeting that he could not use formal verification without source code or when the task was too complex.

“I found out that Ethereum, the Ethereum Virtual Machine, the Yellow Paper only had 32 pages of introduction, and I thought I could translate it and write a proof of concept for a smart contract.”

Ethereum, on the other hand, can offer what he calls a “smaller form factor” and “solvable problems,” letting developers decide how to efficiently compile Solidity into bytecode.

“I believe there will be more formal verification researchers.”

Not a panacea

However, despite the great interest in the concept, it is important to be cautious about what form formal verification will take. Alex Beregszaszi, a developer working on upgrading the EVM, said he is currently exploring solutions to help developers ensure the functionality of smart contract code.

Passmore also pointed out that it is currently impossible to determine whether the new system has discovered the problems with The DAO because formal verification tools still require human input.

“You can encode The DAO events and then check for vulnerabilities, but first you have to know what the caveats are.”

Both Reitweissner and Passmore acknowledge this limitation and warn developers not to view formal verification as a panacea.

However, Reitweissner believes that as applications are promoted, this methodology will continue to develop, and developers will gradually learn to better identify problems and develop corresponding code libraries to record necessary common problems.

Passmore believes that this way, the Ethereum community can successfully promote the concept, and it will ultimately promote blockchain research and development.

"Even though a lot of people aren't familiar with it yet, we need it. We're still learning, but we have to embrace it, and it's very exciting."