Using Securify for Safer Smart Contracts
Let’s face it. Writing smart contracts is tough. There are multiple perspectives to worry about while developing smart contracts: that all codes are up for public scrutiny, that the requirement for transactions to maintain atomicity could result in reentrant behaviors, that randomness is extremely difficult to reliably achieve in a distributed network, etc. And more than once we have seen high profile smart contract exploits which resulted in huge losses [1][2][3][4][5], with the scarier idea being “who/what are we empowering with these lost funds”.
To develop safer smart contracts, efforts from multiple parties are ongoing — developer education with best practice guidelines and “capture the flag” challenges such as Ethernaut or Capture the Ether, better toolsets (e.g. Remix with static analysis) and/or languages (Vyper) to prevent accidental mistakes, security scanners, and others. More comprehensive reviews could involve audits by third parties using manual reviews or formal verification, however, may not be accessible for everyone, especially for teams who are bootstrapping or hobbyist programmers. For the aspiring smart contract developer, an immediately accessible toolkit for smart contracts reviews are security scanners, such as Securify by ChainSecurity (https://securify.chainsecurity.com/) or SmartCheck by SmartDec (https://tool.smartdec.net/). These are easy-to-use online smart contract scanners which most app developers could use, the main difference between the two being that Securify analyses security violations of contracts on a bytecode level through semantic inference, whereas SmartCheck parses the contract language for lexical and syntax analysis. For the purpose of this writeup, we will first focus on our experience with Securify, both the web-based security scanner and the Securify backend (https://github.com/eth-sri/securify).
Before we start, I would like to say that online scanners work base on heuristics, and is not capable of detecting vulnerabilities beyond its predefined list which an experienced audit team could offer, therefore they should not be considered a replacement for an extensive audit work where necessary. Always be mindful that the more money your smart contract deals with, the higher the risk when something is amiss.
Also, do note that for heuristic analysers, the expectation is to overreport than to underreport potential security violations, so some false positives will be expected which then the smart contract developer should work towards identifying if an attack vector does exist.
Starting with a naively implemented contract wallet — which holds a keccak256 hashed value that acts as the password to allow retrieval of Ethers from this contract:
Right off the bat, we can see that this wallet is potentially vulnerable to front-running, and commitHash (for a short window of time at least) could be initialised by another party instead of the deploying party. Let’s pass it through Securify to see what it picks up:
Securify Web (https://securify.chainsecurity.com/)
With Securify web, a simple copy-paste of the above code suffices. Click “Scan Now”, wait for a bit, and results will be returned.
A total of 5 issues were reported, with 2 warnings.
The issues were reported in a rather intuitive manner right on the potentially vulnerable line of code, with further elaboration and examples provided if the “info” button is clicked.
Looking at the issues:
“Transaction Order Affects Ether Amount” — This possibly is an over-approximation, as here we are sending out the full balance held by the contract without any pre-calculation of amount to be sent, therefore the contract will either send “full amount” or “nothing”. Though what could happen is in a same block, given two valid transactions, the first transaction will draw full amount whereas the second transaction will get nothing.
Here I was also expecting Transaction Ordering Dependency: Receiver to appear, as should the contract be holding a substantial amount of value, it could become worthwhile listening for a transaction to this address with the plaintext data, then front-running with a transaction of my own of a higher gas price.
UPDATE: After chatting with the Securify team, I understood that TOD: Receiver isn’t considered as the sender address remains static as it is described by msg.sender. This would be an issue only if the address is variable within the smart contract, therefore may be changed prior to the withdrawal transaction. What is considered as the front running issue is then TOD: Amount, as the amount held by the smart contract could be withdrawn by another party, leaving the rightful owner with 0.
“Unrestricted write to storage” — Nice that Securify caught this one, where it alerts the contract developer that anyone would write to storage, which is indeed correct. While the contract does check to only allow writes when the storage variable hash has not been given a value, there would be a short window of time where an attacker could render the contract useless by inserting another value not intended by the original user. A better way might be to place this code under a constructor function instead.
“Missing Input Validation” — This is rather self-explanatory, and while not super important in the context of this contract, is something which contract developers should watch out for, especially for different data types. Things like checking if the address being passed to the contract is not accidentally 0x0 to prevent lost funds [6] (assuming we are expecting legitimate transactions, instead of sending tokens to a burn address — which could be done in a separate function without this check).
Both the “Unrestricted Ether Flow” and “Unsafe Call to Untrusted Contract” are fair warnings, as the contract could be communicating unintendedly with contracts or accounts (e.g. ethers transferred to another party instead of the contract owner), so it is worthwhile for the contract developer to take a step back and see if this is indeed the intended design.
Securify Local (https://github.com/eth-sri/securify)
Since Securify has a web front end, why should one use a local instance of Securify? For one, it is possible to extend Securify with additional security patterns for specific contract logic (something I am exploring, perhaps worth a separate writeup), especially if there are business domain restrictions which cannot be captured by a generic expression. Also, from my couple of weeks playing with Securify Web there are instances where it runs slow or times out, and to be fair it *is* a public service, therefore having a local instance is helpful.
I deployed Securify local with my Ubuntu instance with docker installed, so we just need to build the Securify docker image and point Securify to our directory which we would like to analyse.
And upon completion of analysis:
A total of 5 violations (issues) and 4 warnings are detected. The reported violations and warnings are less verbose here (unlike the web version which provides elaboration and example), and the violations are consistent with the ones reported by Securify Web. On the other hand, Securify Local seems to provide additional warnings for us to look into: LockedEther, DAOConstantGas, TODReceiver, and UnhandledException.
I reckon these are labeled as warning since they are partial matches however does not fully match to both the violation patterns and safety patterns as stipulated within Securify — For example, the case of LockedEther — The contract does allow ethers to be received, however as the transfer sends from address(this).balance which could potentially be 0, Securify therefore picks this up neither as a violation or safe pattern. These warnings act as flags for the contract developer to have another look, to ensure these aren’t actual violations.
Just to be thorough, the full list of patterns which Securify Local would report are:
- LockedEther — Reports the possibility where ethers sent to this contract would not be retrievable, hence “locked” within the contract.
- DAO — Reports the possibility of reentrancy attacks (similar to the DAO case), and more precisely this pattern checks if all gas is forwarded. Could be avoided by using the transfer() or send() operations which forwards only 2300 gas stipend.
- DAOConstantGas — Reports the possibility where changes to state after executing an ether transfer may be vulnerable to a reentrancy attack. An example, a variable holding the remaining ethers held being updated only after sending Ethers. In most cases should be avoided using transfer() or send(), but a better practice is to utilise Checks-Effects-Interactions pattern[7].
- TODReceiver — Reports the possibility where the receiver of a transfer may be changed due to transaction ordering with a block. An example, if the intended recipient address is stored as a storage variable and a transfer is to execute based off this address, there is a chance the address may be changed or overwritten if there exists such a transaction prior to the transfer.
- TODAmount — Reports the possibility where the amount of a transfer may be changed due to transaction ordering within a block. Similar to TODReceiver, but in this case, the amount being transferred may change. An example, during a crowdsale where the token multiplier * ethers received = tokens to send, where the token multipler is a variable which could be changed prior to the actual sending occurs.
- UnhandledException — Reports the possibility of whereupon using call() or send(), the return value is not being handled. For example, if a send() operation takes place where the receiving contract runs a fallback function which results in an out of gas error, the send() operation would not revert, but instead return false. Unlike transfer(), which acts like require(send()) and would revert the entire transaction.
- UnrestrictedEtherFlow — Reports the possibility where issues may arise when the contract allows ether to be received indiscriminately, especially to prevent the possibility where Ethers may be locked up due to a missing transfer operation[8].
- UnrestrictedWrite — Reports the possibility where a storage variable may be indiscriminately overwritten by any other party, as there are no ownership restrictions to it.
Interestingly, if we look through Securify’s Github (https://github.com/eth-sri/securify/tree/master/src/main/java/ch/securify/patterns), there seem to be a couple more patterns, many which are commented — Possibly work in progress, or still being refined.
Be mindful that Securify does not execute numerical analysis and therefore there are no overflow/underflow checks, though this is planned for future releases (as addressed under section “Limitation” of the Securify academic paper) [9].
Concluding Remarks
My experience with Securify so far is good (except the occasional “Bad Gateway” on Securify Web, though I’d just move on to using my local instance then). What is really commendable is that ChainSecurity decided to open source the project under a fairly permissive Apache 2.0 license, and making Securify free for public use, especially when smart contract security audits could be prohibitively expensive for some individuals.
That said — Heuristic analysers could only find what had happened as experienced, and new patterns will need to be explicitly covered or otherwise may be missed. Where a more extensive audit is necessary, formal verification with manual audits could proof to be more robust, and worth looking into.
[1] https://blog.zeppelin.solutions/on-the-parity-wallet-multisig-hack-405a8c12e8f7
[2] https://medium.com/cybermiles/i-accidentally-killed-it-and-evaporated-300-million-6b975dc1f76b
[3] http://hackingdistributed.com/2016/07/13/reentrancy-woes/
[5] https://nvd.nist.gov/vuln/detail/CVE-2018-10376
[6] https://github.com/ethereum/mist/issues/1583
[7] https://fravoll.github.io/solidity-patterns/checks_effects_interactions.html
[8] https://www.parity.io/security-alert-2/
[9] https://files.sri.inf.ethz.ch/website/papers/ccs18-securify.pdf
