truster POC updated #3
Conversation
igorganich
force-pushed
the
truster_pr
branch
from
96f705e to
1e19f47
Compare
igorganich
force-pushed
the
truster_pr
branch
from
a7188e3 to
6effe9c
Compare
igorganich
force-pushed
the
truster_pr
branch
from
5ef7771 to
20d5ce4
Compare
igorganich
force-pushed
the
truster_pr
branch
from
20d5ce4 to
4547b30
Compare
| Then the opposite check will look like this: | ||
| ```solidity | ||
| function _isSolved() private { | ||
| ... | ||
| assert(token.balanceOf(address(pool)) != 0 || token.balanceOf(recovery) != TOKENS_IN_POOL); | ||
| } |
| **0xaaaa0003** is the pool address. **0xab19e0c0** is the **flashLoan** function selector: | ||
| ```javascript | ||
| $ cast 4b 0xab19e0c0 | ||
| flashLoan(uint256,address,address,bytes) | ||
| ``` |
There was a problem hiding this comment.
cool thanks for adopting the cast 4b method
test/truster/README.md
Outdated
| Fortunately, Halmos provides a special cheat-code for such cases: svm.createCalldata(). All we need to generate valid calldata is the contract type passed as a parameter to this cheat-code. One of the most obvious ways to use it in our attacker is this piece of code: | ||
| ```solidity | ||
| contract SymbolicAttacker is Test, SymTest { | ||
| function attack() public { |
There was a problem hiding this comment.
| function attack() public { | |
| function attack() public { |
test/truster/README.md
Outdated
| /* | ||
| ** It is expected to receive a symbolic address as a parameter | ||
| ** This function should return some concrete address and corresponding data. | ||
| ** In the case of symbolic execution, the brute force over addresses | ||
| ** is happening here! | ||
| */ | ||
| function get_concrete_from_symbolic (address /*symbolic*/ addr) public view | ||
| returns (address ret, bytes memory data) | ||
| { | ||
| for (uint256 i = 0; i < addresses_list_size; i++) { | ||
| if (addresses[i] == addr) { | ||
| string memory name = names_by_addr[addr]; | ||
| return (addresses[i], svm.createCalldata(name)); | ||
| } | ||
| } | ||
| revert(); // Ignore cases when addr is not some concrete known address | ||
| } | ||
| } |
There was a problem hiding this comment.
clever technique!
I would explain this slightly differently:
- if addr is a concrete value, this returns (addr, symbolic calldata for addr)
- if addr is symbolic, execution will split for each feasible case and it will return (addr0, symbolic calldata for addr0), (addr1, symbolic calldata for addr1), ..., and so on (one pair per path)
- if addr is symbolic but has only 1 feasible value (e.g. with vm.assume(addr == ...)), then it should behave like the concrete case
There was a problem hiding this comment.
Yes, it would be much cleaner
test/truster/README.md
Outdated
| } | ||
| ``` | ||
|
|
||
| We will not dwell on the implementation details of this contract. I will only say that this is a contract in which you can store address->contract name pairs. And also with its help you can conveniently brute force addresses symbolically. It is easier to show how to use it in practice. First, let's prepare Global Storage in Truster_Halmos.t.sol: |
There was a problem hiding this comment.
nit: can we rename the file TrusterHalmos.t.sol? let's drop the underscore, it's cleaner
test/truster/README.md
Outdated
| // We can hardcode this address for convenience | ||
| GlobalStorage glob = GlobalStorage(address(0xaaaa0002)); | ||
|
|
||
| function attack() public { |
There was a problem hiding this comment.
| function attack() public { | |
| function attack() public { |
| ... | ||
| contract SymbolicAttacker is Test, SymTest { | ||
| // We can hardcode this address for convenience | ||
| GlobalStorage glob = GlobalStorage(address(0xaaaa0002)); |
There was a problem hiding this comment.
can we pass it as a constructor parameter? hardcoding it seems brittle (for instance if we move things around a bit and addresses change, it would require debugging what's going on)
There was a problem hiding this comment.
Of course, we normally expect to pass such contracts through the constructor. However, I did this specifically to emphasize that we can use this GlobalStorage from anywhere in the application. Imagine that we needed it in a contract generated by some factory contract. If we pass them through the constructor - we will have to rewrite each of these contracts by adding GlobalStorage passing logic. I thought it was less convenient than just hardcoding it where it was needed. And logging in at the very beginning immediately gives us the address of this contract.
What do you think?
There was a problem hiding this comment.
This discussion will definitely end as soon as "native" storage appears in Halmos :). For example, Clang Static Analyzer also uses symbolic code execution and there is a possibility to use such storage to collect the necessary information https://clang.llvm.org/doxygen/ProgramStateTrait_8h.html#a6d1893bb8c18543337b6c363c1319fcf. How about an idea for improvement?
No description provided.