Pakala: yet another EVM symbolic execution tool
Tested on Ubuntu 20.04,python 3.8.10
there were several dependencies issues on Ubuntu 22 with Python 3.10 so downgraded version is recommended for proper run
Pakala is a tool to search for exploitable bugs in Ethereum smart contracts.
Pakala is a symbolic execution engine for the Ethereum Virtual Machine.
The intended public for the tool are security researchers interested by Ethereum / the EVM.
It basically looks for ways to get money out of the contract, into an address the attacker controls. That’s the most obvious kind of vulnerability that people would seek to exploit.
What does it looks for?
Right now, there are only two built-in analyses:
call suicide() to an user-controlled address.
send() more ethers than the attacker sent.
Pakala can stack an arbitrary number of calls to the contract, to allow for state-changing calls first, and then withdrawals.
Z3 abstraction layer
It uses Z3, but through Claripy, which is an abstraction layer that exposes a nice interface, and does caching and black magic.
I also added a SHA3 layer on top of it, which does what’s needed to support cryptographic hashes properly, without this detail leaking anywhere in the code
Two layers: finding executions and stacking them
The first one executes a contract and tries to find a list of “outcomes”. An outcome is a valid execution of the contract that led to a state change (storage written, or money sent), associated to the precondition that needs to be satisfied for this specific execution to trigger.
The second layer is able to tell whether an outcome is doing something bad, corresponding to a vulnerability.
It can also stack multiple outcomes on top of each other, to simulate a sequence of multiple calls to the contract. That means it’s able to detect vulnerabilities that need more than one transaction (typically, changing the owner, then calling an “ownerOnly” function).
This approach allows it to only execute the contract once, and then focus on stacking the outcomes, which is pretty efficient. However, that means there is no support for calling external contracts. It will never be able to find reentrancy bugs either.
You can use it as a reverse engineering tool: by simply listing the outcomes it is possible to get a good understanding of what the contract is doing.
root@CryptoXploit:~# apt update
root@CryptoXploit:~# apt install python3-pip
root@CryptoXploit:~/Pakala# pip3 install –upgrade pip
root@CryptoXploit:~# pip3 install pakala
you will be required web3 API to pull latest address status, transactions etc so for that reason go to https://alchemy.com/ and free signup for API
setup the Ethereum API as mainnet and then go to https://dashboard.alchemy.com/
click VIEW KEYS
copy the HTTPS link
root@CryptoXploit:~/Pakala# WEB3_PROVIDER_URI=’https://eth-mainnet.g.alchemy.com/v2/nr3lejsEx_jGZhkTc2-V4dLW5yvtBDle’
root@CryptoXploit:~# pakala 0xeBE6c7a839A660a0F04BdF6816e2eA182F5d542C –force-balance=”1 ether”
