Echidna failure

[DanielVF]

Got an echidna failure somehow. Will need to dig into it later.

Analyzing contract: contracts/contracts/crytic/PropertiesOUSDTransferable.sol:PropertiesOUSDTransferable
crytic_approve_overwrites: passed! 🎉
crytic_self_transferFrom_to_other_ERC20PropertiesTransferable: failed!💥
Call sequence:
initialize("&\214&4#\216)?P1\170\141\254\162.\227\142\153BiZ\209\DC3\vqC9)\NAK\ETX\212$","\251\f\b\251\139x\n]$!\249\207_______\205\194\239\128p\SYN\255",0xf17f52151ebef6c7334fad080c5704d77216b732) from: 0x627306090abab3a6e1400e9345bc60c78a8bef57
mint(0xf17f52151ebef6c7334fad080c5704d77216b732,6) from: 0xf17f52151ebef6c7334fad080c5704d77216b732 Time delay: 363058 seconds Block delay: 6382
changeSupply(599290589) from: 0xf17f52151ebef6c7334fad080c5704d77216b732 Time delay: 40014 seconds Block delay: 39046

crytic_zero_always_empty_ERC20Properties: passed! 🎉
crytic_self_transfer_ERC20PropertiesTransferable: passed! 🎉
crytic_self_transferFrom_ERC20PropertiesTransferable: passed! 🎉
crytic_revert_transferFrom_to_zero_ERC20PropertiesTransferable: passed! 🎉
crytic_revert_transfer_to_user_ERC20PropertiesTransferable: passed! 🎉
crytic_revert_transfer_to_zero_ERC20PropertiesTransferable: passed! 🎉
crytic_transfer_to_other_ERC20PropertiesTransferable: failed!💥
Call sequence:
initialize("&\214&4#\216)?P1\170\141\254\162.\227\142\153BiZ\209\DC3\vqC9)\NAK\ETX\212$","\251\f\b\251\139x\n]$!\249\207_______\205\194\239\128p\SYN\255",0xf17f52151ebef6c7334fad080c5704d77216b732) from: 0x627306090abab3a6e1400e9345bc60c78a8bef57 Time delay: 411308 seconds Block delay: 14451
mint(0xf17f52151ebef6c7334fad080c5704d77216b732,6) from: 0xf17f52151ebef6c7334fad080c5704d77216b732 Time delay: 363058 seconds Block delay: 6382
changeSupply(599290589) from: 0xf17f52151ebef6c7334fad080c5704d77216b732

crytic_less_than_total_ERC20Properties: passed! 🎉

Unique instructions: 5450
Unique codehashes: 1
Seed: 5242621880353822340

[DanielVF]

Here's my initial decoding of this. (I like to imagine Echidna as being a little dramatic at times.)

• Start with three users, each having $113,427,455,640,312,821,154 OUSD.
• Mint raw 6 coins to one user
• BACKING STABLE COINGS ARE ALMOST GONE! ONLY BACKED NOW BY ONE BILLIONTH OF A CENT.
• One user transfers one raw coin, aka one billionth billionth of a cent, to another.
• One of the following properties does not hold:
  • balanceOf(sender) == starting_balance - 1)
  • balanceOf(receiver) >= 1)
  • the transfer succeeded

Now this makes all the sense in the world that this would fail, given that our rebase ratio has just been hammered flat by the backing coins going from $113,427,455,640,312,821,154 to something near zero in human scales.

The question I'm left with after reading the code is why this isn't happening every time echidna runs a couple hundred thousand tests. It may just be that it rarely ends up setting the supply to something truly low, since random uint256s cover a big range? Feels like I must be not understanding something somewhere.

The other side of this is that using such high initial balances for echidna may mask any problems going the opposite way, a normal supply massively increasing over the years.

[DanielVF]

Switched to running many parallel tests, giving everyone a starting balance of "10" for the joy of it. Got another failure in a different test.

crytic_self_transferFrom_to_other_ERC20PropertiesTransferable: failed!💥
Call sequence:
initialize("\NUL\202\195gZ'\248\197}\165\144\163\150\161\247\224\136\SI","{{(4\165\176<\244\161U",0x627306090abab3a6e1400e9345bc60c78a8bef57)
mint(0xf17f52151ebef6c7334fad080c5704d77216b732,2)
changeSupply(3)

OUSD doesn't seem to work well when the supply changes down to billionths of billionths of a cent.

[DanielVF]

From a triage point of view, I don't think these results are an indication of a security vulnerability.

We may want to discuss:

• if this is really not an issue
• if we should alter our tests to avoid triggering this as a false positive
• if we should alter our contract behavior in some way for exceptionally massive changes in supply.

[franckc]

Here is another reproduction:

crytic_transfer_to_other_ERC20PropertiesTransferable: FAILED! 

Call sequence, shrinking (2664/5000):
1.initialize("Governor::propose: proposal function information arity mismatch","\164:\v\173\173\173\173\173\173\173\1          
2.mint(0xf17f52151ebef6c7334fad080c5704d77216b732,1524785992) from: 0xc5fdf4076b8f3a5357c5e395ab970b5b54098fef Time d               
3.changeSupply(18) from: 0xc5fdf4076b8f3a5357c5e395ab970b5b54098fef Time delay: 496638 seconds Block delay: 19465 

[franckc]

Another repro:

crytic_transfer_to_other_ERC20PropertiesTransferable: failed!💥  
  Call sequence:
    initialize("Mismatch durations and rates","oUSD address es ziro",0xf17f52151ebef6c7334fad080c5704d77216b732) from: 0x627306090abab3a6e1400e9345bc60c78a8bef57 Time delay: 297689 seconds Block delay: 17161
    mint(0xf17f52151ebef6c7334fad080c5704d77216b732,1799) from: 0xf17f52151ebef6c7334fad080c5704d77216b732 Time delay: 471060 seconds Block delay: 41590
    changeSupply(1000000) from: 0xf17f52151ebef6c7334fad080c5704d77216b732 Time delay: 275425 seconds Block delay: 775