Formal Verification of Ethereum Smart Contracts

Analyse any contract for critical security vulnerabilities and insecure coding.
One click only. Formal security guarantees. Accepts source and bytecode. Extensible.

-
Enter Contract

Error

JavaScript required

Analysis Results

Decompiled Contract

Security Report

Transaction Reordering

Transactions May Affect Ether Receiver
Matched lines:
info
Transactions May Affects Ether Amount
Matched lines:
info

Recursive Calls

Gas-dependent Reentrancy
Matched lines:
info
Reentrancy With Constant Gas
Matched lines:
info
Reentrant Method Call
Matched lines:
info

Insecure Coding Patterns

Unchecked Transaction Data Length
Matched lines:
info
Unhandled Exception
Matched lines:
info
Use of Origin Instruction
Matched lines:
info
Missing Input Validation
Matched lines:
info

Unexpected Ether Flows

Locked Ether
Matched lines:
info

Use of Untrusted Inputs in Security Operations

Use of Untrusted Input
Matched lines:
info
Block Timestamp
Matched lines:
Block Number
Matched lines:
Block Hash
Matched lines:
Coinbase
Matched lines:
Gas Limit
Matched lines:
Difficulty
Matched lines:
Gas
Matched lines:
Gas Price
Matched lines:
Balance
Matched lines:

Why use Securify?

Securify formally verifies Ethereum contracts for common security issues, such as transaction reordering and missing input validation. Securify is the first smart contract verifier that provides:

How Does Securify Compare to Existing Solutions?

Existing solutions based on executing the contract check only a subset of the possible paths and can therefore miss critical security problems. Further, approaches based on interactive-theorem provers can provide strong guarantees, for all paths, but they cannot be easily automated or easily extended. In contrast, Securify combines the best of both worlds: it analyzes all paths while being fully automated. Further, Securify features a designated domain-specific language for specifying vulnerabilities, which makes it easy to keep Securify up-to-date with current security and other reliability issues.

Are Strong Guarantees Needed?

Yes, because otherwise vulnerable smart contracts may get incorrectly flagged as secure.

Can I get full access now?

Yes, we offer pilot customer access to Securify with the following privileges:

Sign up for the full release of Securify and future updates

Securify Terms of Service

This service by ETH Zurich, Department of Computer Science, Software Reliability Lab, is free of charge. We accept only legal pieces of code. All entries are logged for research and improvement of service. ETH Zurich does not warrant any rights or service levels, nor does it acquire any rights on the code entered. Swiss law is applicable. The place of jurisdiction is Zurich, Switzerland. By sending code to this site, you warrant that all your entries are in your sole responsibility and you do not infringe any laws or third-party rights like copyrights and the like. ETH Zurich and its employees shall not be liable for any entries and for any damages resulting thereof. You agree to indemnify, defend and hold them harmless from any legal or financial demands or arising out of the breach of these terms of use, especially from third-party claims regarding infringement of copyrights and the like.

Sign up for full release

We will inform you about the full release of Securify and future updates.
✓ Thank you for your interest.

Our team

We are a team of security / AI / blockchain experts from ETH Zurich.

Dr. Petar Tsankov


Automated Security

Andrei Dan


Formal Verification

Dr. Arthur Gervais


Blockchain Security

Prof. Dr. Martin Vechev


Tenured Professor of Software Reliability

Feedback

Found an issue with the analysis?
Please let us know:
✓ Thanks for your feedback.

Use of Origin Instruction

The tx.origin instruction walks all the way up the call stack and returns the address of the contract that originated the call. Authorization checks based on the tx.origin can result in dangerious callback attacks.

Safe Example

Unsafe Example


The Safe Example contract on the left is safe with respect to this security guideline as it compares the owner's address to the immediate caller (returned by msg.sender). In contrast, the Unsafe Example on the right compare's the owner address to the one originating the call (returned by tx.origin), which makes the code vulnerable to callback attacks where calls originating from the UserWallet contract are redirected to the send method to drain the wallet.

Transactions May Affect Ether Receiver

A contract is exposed to this vulnerability if a miner (who executes and validates transactions) can reorder the transactions within a block in a way that affects the receiver of ether.

Safe Example

Unsafe Example


The Safe Example contract on the left is not vulnerable to this vulnerability as the receiver of ether is msg.sender, which cannot be modified by previously executed transactions. In contrast, the Unsafe Example on the right sends ether to winner, and this value can be modified by another transaction that modifies the address stored at winner.

Note that these examples are only for illustration purposes. For value transfer, the solidity function transfer() should be used.

Transactions May Affect Ether Amount

A contract is exposed to this vulnerability if a miner (who executes and validates transactions) can reorder the transactions within a block in a way that affects the amount of ether transfered to the receiver.

Safe Example

Unsafe Example


The Safe Example contract on the left is not vulnerable to this vulnerability as the amount of ether transfered is price, which is a constant that cannot be modified by previously executed transactions. In contrast, the amount of ether transfered by the contract Unsafe Example can be modified via calls to method setPrice.

Note that these examples are only for illustration purposes. For value transfer, the solidity function transfer() should be used.

Gas-dependent Reentrancy

Gas-dependent reentrancy is a major vulnerability that became famous due to the DAO attack. A contract is exposed to gas-dependent reentrancy if: (1) the amount of transferred ether depends on state that gets updated only after the transfer is made and (2) the amount of gas handed to the caller depends on amount of available gas. The Call instruction for ether transfer grants control over the transaction execution to the ether receiver while handing all available gas, and this allows the receiver to call the contract again (before its state is updated) to receive the same amount of ether again. An attacker can repeat this process until the contract's balance is drained.

Safe Example

Unsafe Example


Reentrancy is not possible in the Safe Example shown on the left because the contract sets the balance variable to 0 before the transfer is made, therefore blocking potential reentrant calls. The Unsafe Example contract on the right however is vulnerable to reentrancy, because the balance variable is modified only after the transfer is made.

Note that these examples are only for illustration purposes. For value transfer, the solidity function transfer(amount) should be used as it gives a only a minimal amount of gas to the caller.

Reentrancy with Constant Gas

A contract is exposed to reentrancy with constant gas if: (1) the amount of transferred ether depends on state that gets updated only after the transfer is made and (2) the amount of gas handed to the caller is constant. The transfer(amount) and send(amount) instruction for ether transfer grants control over the transaction execution to the ether receiver, and this allows the receiver to call the contract again (before its state is updated) to receive the same amount of ether again. An attacker can repeat this process until the contract's balance is drained.

Safe Example

Unsafe Example


Reentrancy is not possible in the Safe Example shown on the left because the contract sets the balance variable to 0 before the transfer is made, therefore blocking potential reentrant calls. The Unsafe Example contract on the right however is vulnerable to reentrancy, because the balance variable is modified only after the transfer is made.

Missing Input Validation

Unexpected method arguments may result in insecure contract behaviors. To avoid this, contracts must check whether all transaction arguments meet their desired preconditions.

Safe Example

Unsafe Example


The Safe Example contract on the left correctly throws an exception if the amount of ether requested to be transfered exceeds the balance of the transaction sender. In contrast, the Unsafe Example contract does not check the amount, which may result in transferring more ether than the transaction sender actually has. Note that the balance stored in the map balance would underflow since for unsigned integers we have 0 - 1 = 2**256 - 1.

Transaction Data Length Validation

Contracts that do not validate the length of the provided transaction data may allow attackers to drain their balance. By default, Call instruction that is given address that is shorter than 20 bytes gets padded with zeros. Moreover, transaction data is also padded with zeros. Attackers can leverage this behavior to effectively increasing the payout value substantially. Securify detects Call instructions that take as input an address that depends on CallDataLoad and checks whether the transaction data size is checked.

Safe Example

Unsafe Example


The Safe Example contract correctly checks the length of the data passed to method sendMoney. The Unsafe Example contract does not perform this check.

Unhandled Exception

A call/send instruction returns a non-zero value if an exception occurs during the execution of the instruction (e.g., out-of-gas). A contract must check the return value of these instructions and throw an exception:

Safe Example

Unsafe Example


The Safe Example contract on the left correctly checks the return value of the call instruction and throws an exception using the statement throw. The Unsafe Example contract on the right ignores the return value. Consequently, the balance of the transaction sender is zeroed out even if the transfer of ether via the call instruction fails.

Locked Money

The locked Ether bug occurs in contracts that never transfer Ether and do not have a Suicide instruction (which transfers the contract's owner all the contract's Ether). Securify detects such contracts by checking whether all instructions are different than the Suicide instruction and whether all Call instructions transfer zero ether.

Safe Example

Unsafe Example

Use of Untrusted Inputs in Security Operations

The unsafe inputs security bug occurs in contracts where inputs to a cryptographic hash function can be manipulated by the miner or user. That is, when the inputs depend on block information or transaction input. Our pattern detects this bug by selecting SHA3 (and SHA256, RIPEMD160) instructions and checking whether the inputs to the SHA3 depend on block information. The inputs to the SHA3 are the values in the memory starting from the first SHA3's argument and up to the location found at the sum of the first and second arguments (exclusive).

Safe Example (for limited value)

Unsafe Example

Transactions may affect Ether receiver
info
Transactions may affect Ether amount
info
Recursive Calls
info
Missing Input Validation
info
Transaction Data Length Validation
info
Unhandled Exception
info
Locked Money
info
Use of Untrusted Input
info
We are currently in beta.