Similar projects and alternatives to reentrancy-attacks based on common topics and language
OpenZeppelin Contracts is a library for secure smart contract development.
Bamboo see https://github.com/cornellblockchain/bamboo (by pirapira)
Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.
Practical tutorials of Certora Prover (by Certora)
Example Certora verification for a simple multi-contract system
Smart Contract security audit reports (by TechRate)
Ultimate Solidity, Blockchain, and Smart Contract - Beginner to Expert Full Course | Python Edition
reentrancy-attacks reviews and mentions
A look into formal verification of smart contracts using Certora
5 projects | dev.to | 2 Dec 2022
The main challenge is dealing with non-view functions. The default behavior of the prover is to assume that an external call can alter all state on every contract but the caller, noted as HAVOC_ECF. This can lead to state changes in external contracts that are unreachable, making verification more difficult. Furthermore, it assumes that the call is non-reentrant, which in reality is a frequent source of attacks. This last issue can be avoided by indicating that calls can re-enter, noted as HAVOC_ALL, but this means that an external call can mutate any state in any contract, caller included. This leaves the contract being verified in a state where we don't know anything about it after an external call is made. This severely limits what we can prove.
pcaversaccio/reentrancy-attacks is an open source project licensed under GNU Affero General Public License v3.0 which is an OSI approved license.