kmbarry1

// BUGGED, DO NOT DEPLOY

// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity ^0.8.11;

/// @title AvsBGame
/// @notice A Liar's Game: Vote by putting ETH behind A or B ... the side with the least votes gets all the ETH
/// @author AvsB Team
/// @dev Built using a Commit-Reveal scheme

kmbarry1

# ./flap_checker.sh 1 10 1900
# will check flaps 1 through 9 if they are selling at more than 6% deviation from 1900

ID=$1
END_ID=$2
FAIR_PRICE=$3
while [[ ID -ne END_ID ]]
do
    ret=`seth call 0xC4269cC7acDEdC3794b221aA4D9205F564e27f0d "bids(uint256)(uint256,uint256,address,uint48,uint48)" $ID`
    a=($(echo "$ret" | tr ',' '\n'))

kmbarry1

paste in to console at at https://github.com/<org>/<repo_name>/labels:


[
    {
      "name": "Priority: Critical",
      "description": null,
      "color": "b60205"
    },
    {

kmbarry1

// Add these tests into DssVest.t.sol

    uint256 constant WAD = 10**18;
    function add(uint256 x, uint256 y) internal pure returns (uint256 z) {
        require((z = x + y) >= x);
    }
    function testFuzzFail_1() public {
        // derived from echidna failure:
        // test_init_ids(115792089237316195423570985008687907853269984665640564039457584007913129639935,100242773934347682338375481833561433633362664707040856359631189992494487309630,10,39080061795132864699069909921915714851660400468839437511646123280429906730201,1524785992,0x20000)

kmbarry1

#!/usr/bin/env bash

# Your ETH_RPC_URL envvar should point to an archive node.

# Not in principle perfectly accurate, since COL isn't necessarily monotonic.
# Also doesn't account for underwater Vaults, but these are rare (not sure
# if there has ever been one for ETH-A, in fact).

# But, should be good enough to give an idea when the problem began.

kmbarry1

Error message after rejection:

[Error] Critical:  (null)
  while evaluating function Set:in * 19537

The proof accepts if Vat == 10 is added to the act (if condition). (Vat == 11 also works)

K invocation:

kmbarry1

So, I was just starting to work through analyzing these right before everything blew up, so partially I'm piecing this together from notes I don't remember writing--trusting myself that I wrote down correct stuff.

The recent failures can be viewed at: https://reports.makerfoundation.com/k-dss/2addb6a7692db7ba72ef/

I went through the error logs for these previously. Most of them "exploded"--some intimidatingly abstruse stderr.

I tried to replicate Vow_cage-surplus_pass_rough locally; its stderr from the server was an explosion, but locally it just got "stuck" (no progress being made when viewing the trace in klab debug).

kmbarry1

"Instant DSR" Pot attack

This is a tough one. In general, it's always theoretically possible to get a "free lunch" off the DSR. E.g. if Jug.drip is not being called very frequently, it's trivial. It usually depends, however, on the behavior of the other market participants. The reason this bug was a big deal was that it was exploitable regardless of the behavior of others. So we need an invariant that doesn't just detect a "free lunch", but one that detects an easily-obtainable "free lunch". Ideally, one shouldn't have to specify in too much detail the behavior of other participants for detection. The current property just checks that Pot.join is not called in a block without Pot.drip being called first. A slightly more sophisticated check would be as follows:

kmbarry1

All constraints:

(May ==K 1)                                                                                                                                                                                                 
( Live ==K 1 )                                                                                                                                                                                              
( VCallValue ==K 0 )                                                                                                                                                                                        
( ( ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) <= 0 ) )                                                                                         
( ( minSInt256 <= ( Art_i * ( ( ( (#rpow( #Ray , ( Base + Duty ) , ( TIME - Rho ) , #Ray )) * Rate ) / #Ray ) - Rate ) ) ) )                                                           

kmbarry1

Installing klab (assuming you already have everything you need to build K installed)

1. git clone https://github.com/dapphub/klab
2. cd klab/
3. make deps
4. make deps-haskell
5. sudo make link
6. source ./env # <--you might need to chmod this to make it executable, it relies on pwd so you must run it in the klab directory, and you need to run it in any shell you want to use klab in--I like to add it to my .bashrc
7. the command-line tools jq and jshon are needed if you don't already have them

klab will fetch and compile the versions of K and KEVM that it needs, and the environment variables set by the env script will automatically cause klab to use these.