Watch Your Language: Our First Vyper Audit
A lot of companies are working on Ethereum smart contracts, yet writing secure contracts remains a difficult task. You still have to avoid common pitfalls, compiler issues, and constantly check your code for recently discovered risks. A recurrent source of vulnerabilities comes from the early state of the programming languages available. Most developers are using Solidity, which is infamous for its numerous unsafe behaviors. Now Vyper, a Python-like language, aims to provide a safer language. And since community interest in Vyper is growing, we had to review Vyper contracts on a recent audit with Computable.
Overall, Vyper is a promising language that:
- Includes built-in security checks,
- Increases code readability, and
- Makes code review simpler.
However, Vyper’s age is showing; our review confirmed that this young language will benefit from more testing and tools. For instance, we found a bug in the compiler, which indicates a lack of in-depth testing. Also, Vyper does not yet benefit from the third-party tool integrations that Solidity does, but we’re on the case: We recently added Vyper support to crytic-compile, allowing Manticore and Echidna to work on the Vyper contracts, and the Slither integration is in progress. For now, you can check out the details of our Vyper audit and our recommendations below.
The Good
Integer checks are built-in
Vyper comes with built-in integer overflow checks, and will revert if one is detected. Since integer overflows are frequently at the root of vulnerabilities, overflow protection by default is definitely a good step towards safer contracts. And with this protection, you don’t need to use libraries like SafeMath anymore.
The main caveat here, though, is the higher gas cost. For example, the compiler will add two SLOAD for the following code:
Figure 1: Integer overflow check.
Figure 2: evm_cfg_builder result for the Figure 1 example.
Nevertheless, overflow protection by default is still the best strategy. In the future, Vyper could reduce the gas cost through optimizations (e.g., removing two SLOADs from the example above), or by adding unsafe types in the language for developers with specific needs.
Unsafe functionality is restricted
Vyper comes with a lot of restrictions compared to Solidity, including:
- No inheritance
- No recursive code
- No infinite length loop
- No dynamically sized array
- No assembly code
- Inability to import logic from another file
- Inability to create one contract from another
Although these restrictions might seem excessive, most contracts can be implemented while still following these rules.
Solidity allows multiple inheritance, which is frequently overused by developers. We saw many codebases with an overly complex inheritance graph, which made the code review much harder than it should be. In fact, contracts are so difficult to track with multiple inheritance, we had to build a dedicated printer to output the inheritance graph in Slither. Preventing multiple inheritance will force developers to create better designs.
Solidity also allows assembly code, which is frequently used to compensate for inadequate compiler optimizations. When it’s impossible to write these optimizations at the developer level, there’s more pressure on the Vyper compiler team to write good compiler optimizations. This is not a bad thing—optimization should rely on the compiler, not the developers.
Overall, one-third of Slither’s detectors are not needed when using Vyper, thanks to Vyper’s many language restrictions. Vyper-specific detectors can be written, but the simplicity of the language tends to make it safer than Solidity by design.
The Not-So-Good
Vyper has not been tested or reviewed enough
Vyper’s Readme warns its users:
As a result, the compiler is likely to have bugs, and the language’s syntax and semantics might change. Vyper’s users must be careful, follow its development closely, and review the generated EVM bytecode.
For example, until 0.1.0b12, public functions were callable from the contract itself, which created a security risk due to the way Vyper handles msg.sender and msg.value. Since 0.1.0b12, all public functions are the equivalent of external functions in Solidity, removing the risk of this vulnerability.
The compiler bug we found shows that the compiler would benefit from more testing (see details below). It would not be a surprise to see previous solc bugs present in Vyper. For example, the following bugs were either recently fixed or are still present:
- Lack of overflow checking for unary operations
- Lack of type checking on events
- Incorrect zero-padding when returning small arrays
Some restrictions are cumbersome
While many of Vyper’s restrictions are good steps toward safer code, some may create problems.
For instance, the total absence of inheritance makes it more difficult to test the code. The creation of mock contracts, or the addition of properties for testing with Echidna, require copying and pasting the code—an error-prone process. Although multiple inheritance is frequently abused by developers, it won’t hurt to allow simple inheritance to facilitate testing.
Like the lack of inheritance, the absence of contract creation is also inconvenient— it increases the complexity of mock contracts, unit tests, and automated testing.
Finally, each contract has to be written in a separate file and import has a partial support. If contract A calls contract B, A needs to know B’s interface. It is then the developer’s responsibility to copy and paste the latest interface version. If B is updated, but its interface in A is not, A will be buggy and error-prone in handling the contract’s dependencies. To prevent these types of vulnerabilities, we built slither-dependencies, a tool that will check the correct interfaces in the codebase.
Our Solutions
Compiler bug: Function collision
Vyper follows the function dispatcher standard used by Solidity: To call a function, the first four bytes of the keccack of the function signature will be used as an identifier. A so-called dispatcher takes care to match the identifier with the correct code to execute. In Figure 3, the dispatcher checks for two different function id:
0x0e8927fbc (pushed at 0x94): increase()0x61bc221a (pushed at 0xcb): counter()
Figure 3: Dispatcher of the example in Figure 1.
This strategy has a shortcoming: Four bytes is small, and collisions are possible. For example, both gsf() and tgeo() will lead to an id of 0x67e43e43. Figure 4 shows the dispatcher generated with vyper 0.1.0b10:
Figure 4: Function id collision.
As a result, calling tgeo() will execute gsf() code, and tgeo() will never be executable. This issue creates the perfect conditions for backdoored contracts. We reported this bug to the Vyper team and it was fixed in July. Their initial fix did not consider the corner case of a collision with the fallback function, but this is also properly fixed now.
Finally, we implemented a detector in Slither that will catch this bug. Use Slither if you are concerned about interacting with Vyper contracts.
Crytic tools integration
Vyper is now natively supported by most of our tools (including Manticore, Echidna and evm-cfg-builder) as of crytic-compile 0.1.3.
Manticore
Manticore is a symbolic execution framework that lets you prove assertions in your code. It works at the EVM level, which is necessary to avoid potential compiler bugs. For example, the following token has a bug that will give free tokens to anyone requesting fewer than 10 tokens:
Figure 5: Vyper buggy token.
The following Manticore script will detect this issue:
Figure 6: Manticore example working with Vyper.
The script will generate a transaction showing inputs leading to the bug:
Function call:buy(1) -> STOP (*)
Developers can then integrate the script to their CI to detect the bug, and prove its absence once it has been fixed.
Check out Computable Manticore scripts for more examples.
Echidna
Echidna is a property-testing fuzzer: It tries different combinations of inputs until it succeeds in breaking a given property. Like Manticore, it works at the EVM level. In the following example, Echidna tries a combination of calls until the echidna_test function returns false:
Figure 7: Echidna example.
When running Echidna on the example in Figure 7, the result is:
Figure 8: Echidna running on Vyper code.
Similar to Manticore, Echidna can be integrated with CI to detect bugs during development. Keep an eye on crytic.io for an easy solution for using Echidna.
Slither
We are working to support Vyper in our static analyzer. Slither is already capable of:
- Detecting if code is vulnerable to the collision id compiler bug we discovered.
- Detecting if there is an incorrect external contract definition (via
slither-dependencies).
Once the Vyper support is complete, Vyper contracts will benefit from our intermediate representation (SlithIR), and have access to all the vulnerability detectors and code analyses already present in our framework.
Conclusion
Vyper is a good step towards a better smart contract language. We loved its simplicity and its focus on security. However, the language is a bit too young to recommend for production. If you want to use Vyper, we highly recommend using Manticore and Echidna to check the EVM code, and to follow along Slither’s development.
Already loving Vyper and want to secure your code? Contact us!
*** This is a Security Bloggers Network syndicated blog from Trail of Bits Blog authored by josselinfeist. Read the original post at: https://blog.trailofbits.com/2019/10/24/watch-your-language-our-first-vyper-audit/
