In that case they verify correctness, defined by the authors as
adherence to safe programming practices
What they are effectively testing is the root cause of reentrency vulnerabilities: not respecting the CHECK - EFFECT - INTERACTION pattern.
Take their example code:
function withdrawBalance() {
uint amountToWithdraw = userBalances[msg.sender];
// CHECK
if (amountToWithdraw > 0) {
// INTERACTION
withdrawBalance’();
msg.sender.call(userBalances[msg.sender]);
// EFFECT
userBalances[msg.sender] = 0;
}
}
Which doesn't respect the paradigm, here it is CHECK - INTERACTION - EFFECT. Meaning that a malicious attacker could potentially call withdrawBalance from itself by implementing a fallback function that calls withdrawBalance again.
The call stack would therefore be :
- WithdrawBalance
- Fallback Function
- WithdrawBalance
Executing withdrawBalance twice, so withdrawing twice where it should obvioulsy be forbidden. Their cloning methods artificially creates a path potentially allowing a reentrency attack.
If the verifier finds a path leading to this assert, it indicates a
bug.
Indeed, if that path can be exploited, there is a vulnerability such as double withdrawal in our example. If the correct programming practices are respected, this path should not be exploitable.
Now take this slightly modified example, same as before but just respecting the CHECK - EFFECT - INTERACTION pattern :
function withdrawBalance() {
uint amountToWithdraw = userBalances[msg.sender];
// CHECK
if (amountToWithdraw > 0) {
// EFFECT
userBalances[msg.sender] = 0;
// INTERACTION
withdrawBalance’();
msg.sender.call(userBalances[msg.sender]);
}
}
Once again, we have the included call to the clone function but the path it creates is not exploitable, since the rentrency attack would not pass the CHECK step (if (amountToWithdraw > 0)) as the EFFECT ( userBalances[msg.sender] = 0;) are applied before the INTERACTION step.
Is this a valid method of testing a smart Contract (SC) because we are
modifying the SC? Can we modify the SC during testing?
You can see for yourself that it is valid on those example. It does slightly modify the original function flow, and add a gas small gas overhead but it allows for explicit detection of same function reentrency vulnerabilities, which is the intended goal.
As long as your test doesn't change the logic or any invariant of the smart contract, it is perfectly fine. This cloning method doesn't change any of those (at least in this example).
There are examples where this method doesn't work and unintentionally interfere with the smart contract logic / invariants, take a similar function where you expect to be called with X gas, and expect to be left with Y gas before exiting your function or revert, the gas overhead of their detection method would break your contract logic.
It would however be a bad practice, since you should not assume that opcodes gas cost are constant in time. But it shows that this cloning method while mostly correct, is not always correct.
