The Ethereum community is still reeling from the DAO attack two months ago.
The attack exposed the vulnerabilities of smart contracts when they are not constructed correctly. It also reminded all of us that security should be the number one priority.
Researchers from Microsoft, Harvard University, and Inra, a French national research institute, took the time to analyze the language and verifying process of smart contracts. The group published their results in a technical paper.
The paper established that there’s still more work to be done when it comes to writing smart contracts. It was found that many favor the Solidity source over the Ethereum Virtual Machine (EVM) bytecode. During their research, 396 out of 112,802 contracts were identified on etherscan.io using EVM bytecode.
“[W]e are able to translate and typecheck 46 out of the 396 contracts we collected on https://etherscan.io. Out of these, only a handful are valid in the Eth effect. This is a clear sign that a large scale analysis of published contract is likely to uncover widespread vulnerabilities; we leave such analysis to future work,” the report states.
To allow proper translation and verification between both programming languages, the paper presents the framework of F*, a “functional programming language aimed at program verification.”
This solution will provide individual tools for decompiling EVM bytecode (renamed EVM*) and analyzing Solidity (Solidity*). These tools offer three different methods of verification:
- Given a Solidity program, we can use Solidity* to translate it to F* and verify at the source level functional correctness specifications such as contract invariants, as well as safety with respect to runtime errors.
- Given an EVM bytecode, we can use EVM* to decompile it and analyze low-level properties, such as bounds on the amount of gas consumed by calls.
- Given a Solidity program and allegedly functionally equivalent EVM bytecode, we can verify their equivalence by translating each into F*. Thus, we can check the correctness of the output of the Solidity compiler on a case-by-case basis using relational reasoning.
This shows their dedication to provide the safest and authentic technology.