Interface Deviations
elizabethdinella opened this issue · 4 comments
Hello, thank you for the great work and making your tool publicly available.
I am running in exploit mode with the assertion checker:
./main.native -input examples/Brave3d.sol -mode exploit -exploit_timeout 20000 assert
[CHECKER] Assertion Violation
- all funcs : 31
- reachable : 4
* [STEP] Generating Paths ... took 6e-06s
- #paths : 4
[INFO] Violate CEI: false
[INFO] msg.sender = this possible: false
Model Uploading ...
Generating Exploits ...
=== Interface Deviations ===
- transfer's interface deviated from : transfer(address to, uint value) returns (bool success)
- transferFrom's interface deviated from : transferFrom(address from, address to, uint value) returns (bool success)
- balance's declaration deviated from : mapping(address => uint) balance
=== Report ===
=== Statistics ===
# Iter : 0
- last disproven iter : 0
- last disproven time : 0.
# Max explored depth : 0
# Max disproven depth : 0
# Formulas : 0
# Timeout-formulas : 0
# Queries : 0
# Disproven : 0
- assertion violation : 0
Time Elapsed (Real) : 0.178885936737
Time Elapsed (CPU) : 0.025542
My Brave3d contract has much more than 4 external functions (~10). Why are only 4 paths found?
I also see a list of "Interface Deviations." Can you explain the meaning of this?
Thanks!
[Q1] My Brave3d contract has much more than 4 external functions (~10). Why are only 4 paths found?
=> Could you share your contract for letting me figuring out problems more accurately, .e.g., after chaining variables names or simplifying contract so that it can reproduce the problem above?
[Q2] I also see a list of "Interface Deviations." Can you explain the meaning of this?
=> Those messages are reported if some functions in your contract do not obey some syntactic features of ERC-20 standard
(https://ethereum.org/en/developers/docs/standards/tokens/erc-20/). Those results are irrelevant to the main verification/analysis algorithm. It is mainly for debugging purposes.
You can ignore those messages, if your contract is irrelevant to ERC-20 standard or you do not use erc20
checker in the exploit mode. I will update the code so that it does not show unnecessary logging messages to avoid confusions.
Sure, here is the file. It is a Solidity file, but Github would not let me upload with the .sol
extension
Thanks for sharing the code.
Please note that if the name of the main contract is unspecified via -main
option, our tool will assume that the last contract as a main contract, as mentioned in the readme page.
So please try the following command after doing git pull
(I fixed an error introduced during the refactoring):
./main.native -input a.sol -mode exploit -exploit_timeout 20000 assert -main Brave3d
Hi, it works! Thank you very much.