search

microsoft / verisol

A formal verifier and analysis tool for Solidity Smart Contracts
Other
245 stars 46 forks source link

question: detection of reentrancy and unchecked send vulnerability #264

Open yxliang01 opened 4 years ago

yxliang01 commented 4 years ago

May I know whether it's possible to detect reentrancy and unchecked send vulnerability with this toolchain?

In the test cases, I can see DAO-buggy.sol has an assertion on the balance to avoid getting excessive amount of currency. However, such assertion is specifically for this instance of reentrancy and can't really be generalized.

yxliang01 commented 4 years ago

Hi @shuvendu-lahiri , would you like to answer this question?

shuvendu-lahiri commented 4 years ago

There is no general support for reentrancy assertions in Verisol.

yxliang01 commented 4 years ago

Thank you very much @shuvendu-lahiri for your reply. Would you also like to comment about the possibility of checking unchecked send vulnerabilities with this toolchain?