Asymmetry contest - 0xc0ffEE's results

Lines of code

https://github.com/code-423n4/2023-03-asymmetry/blob/44b5cd94ebedc187a08884a7f685e950e987261c/contracts/SafEth/SafEth.sol#L83-L98

Vulnerability details

Impact

In cases like: a)After SafEth is deployed and there is no derivative added yet b)derivate weights set to 0, accidentally set or malicious owners stakers would receive mintAmount of 0 while spending at least minAmount ETH. Stakers can not withdraw this amount of ETH

Proof of Concept

https://prover.certora.com/output/85902/34363f7f37cf4b17bc7190ea0dfb8d35?anonymousKey=1950f1f3e3cd53876f902057e69958bf9576d133

spec file

rule stakers_funds_locked() {
  env e;
  
  require derivativeCount() == 0 || totalWeight() == 0;

  require e.msg.sender != currentContract;
  require e.msg.value > 0;

  uint256 balance = balanceOf(e.msg.sender);
  stake(e);
  uint256 balanceAfter = balanceOf(e.msg.sender);

  assert balanceAfter == balance;
}

Tools Used

Certora

Recommended Mitigation Steps

Add require(mintAmount > 0);