Solar

Solar

We present Solar, a new analysis tool for automatically detecting standard violation errors in smart contracts. Given the Ethereum Virtual Machine bytecode of a smart contract and a user specified constraint or invariant derived from a technical standard such as ERC-20, Solar symbolically executes the contract, explores all possible execution paths, and checks whether it is possible to initiate a sequence of malicious transactions cause the contract to violate the specified constraint or invariant.

HowTo

Use docker

docker run --rm -it --ulimit stack=100000000:100000000 leeleo3x/solar bash

From Source

Install dependencies:

pip install pyelftools ply pysha3 functools32 
pip3 install web3

Install boolector:

https://boolector.github.io/

Set Env Variable:

export PYTHONPATH=/PATH/TO/Solar

To run the system:

cd Solar/Solar
INFURA_ID=INFURA_ID python solar.py PATH_TO_CONRACT_JSON PATH_TO_ANALYZER [--verbose] [--constraints]

You need to provide infura project id if the contract calls external contracts.

Example:

python solar.py erc20/0x78b7fada55a64dd895d8c8c35779dd8b67fa8a05.json analyzers/total_supply.py 'mint(address,uint256)' --verbose
python solar.py erc20/0x7dc4f41294697a7903c4027f6ac528c5d14cd7eb.json analyzers/approve.py 'approve' --verbose --constraints

Analyzers:

• total_supply.py: Total supply invariant.
• approve.py: Approve and transferFrom constraints (ERC-20).
• transfer.py: Transfer constraints (ERC-20).
• owner.py: Approve and transferFrom constraints (ERC-721).

Results:

Results will be shown in folder mcore_*.