kmbarry1

The act looks like:

behaviour canCall-true of MkrAuthority
interface canCall(address src, address dst, bytes4 sig)

types
  May : uint256

storage
  wards[src] |-> May

kmbarry1

Note: refer to the following branch of k-dss for latest work https://github.com/makerdao/k-dss/tree/pot-rpow

So far I've only looked at the rpow proofs in the Pot contract.

First, I updated the pc values in Pot.rpow-loop, which passes without any issue.

Latest pc values: // 13af => 13f3 pc

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.

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

"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

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

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

#!/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

// 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

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


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