Verification of set up process / authorization exhaustiveness

[MrChico]

The security of dss relies heavily on the fact certain functions are only callable by certain interface contracts. So far, all of our specs have only assumed certain addresses have been given allowance, not excluding the possibility of other access points.

[MrChico]

Currently, the storage contents in all specs are not specified further than what is explicitly given in the spec. But the security of dss relies on some assumptions on storage, in particular, that no other contracts than a carefully selected set are given access control to functions.

I suggest that we move away from an abstracted storage to storage bootstrapped in a particular way (leaving a proof obligation to the set up process). The global/initial storage assumptions can be given in the beginning of each contract:

initial state of Vat

storage
      #Vat.wards[Pit] |-> 1
      #Vat.wards[Drip] |-> 1
      #Vat.wards[Vow] |-> 1
      #Vat.wards[Cat] |-> 1
      #Vat.wards[GemJoin] |-> 1
      #Vat.wards[DaiJoin] |-> 1

The storage cell of each spec generated from an act should now be the initial state + the explicitly stated storage of the act, and nothing more, i.e. no _:Map or further variables in storage.

The acts of access controlled functions would then change from #Vat.wards[CALLER_ID] |-> Can + iff Can == 1 to

CALLER_ID in SetItem(Pit)
                       SetItem(Drip)
                       SetItem(Vow)
                       SetItem(Cat)
                       SetItem(GemJoin)
                       SetItem(DaiJoin)

[livnev]

@MrChico Nice, but we do lose some flexibility since we don't necessarily want to set in stone the list of authorised callers. For example there will be wards who aren't in the list of contracts that we are specifying/verifying, like the admin contracts (it can be argued that they should be added to the scope of FV at some point as well). And if we have CALLER_ID in SetItem(Pit) ... SetItem(RandomContract) ... then what are we gaining from this?

[MrChico]

@livnev Yes, I think it's mainly about being more explicit about which contracts are authorized, and crucially which are authorized at the time of launch. If some new contract is given auth access, then I think we can simply add it to the specs at that point.
I think admin contracts can be added to the context of these specs, even if we make no direct claims on them, similar to the way the auction contracts are only "indirectly present" in other specs right now

[livnev]

@MrChico I'm not sure how this is giving us any stronger guarantees though. what we would really want is to just be able to query the deployed contracts on the blockchain and enumerate the set of keys A for which Vat.wards[A] == 1, for example. But I don't see how putting in these extra assumptions into the specs is helping with that. We are still equally vulnerable to the contracts being deployed incorrectly, i.e. with addresses authorised that don't have to be.

[livnev]

Look at it this way: there will always be some governance contract address A that will probably we controlled by ds-chief, with Vat.wards[A] == 1, and A will have methods that will call Vat.rely(B) with arbitrary addresses B. This is the reason the system is set up this way, so that governance can add/remove future interfaces as needed. So will we be proving anything stronger by switching to this approach, or are we just making more assumptions?

[MrChico]

what we would really want is to just be able to query the deployed contracts on the blockchain and enumerate the set of keys A for which Vat.wards[A] == 1, for example.

Yes, this is essentially what I am suggesting. And yes, specifying the initial state does leave a proof obligation to the set up process (which is something we can tackle, if we make claims about the init code). Setting our proofs up with this approach I think makes the assumption more explicit, opening up the possibility of proving the assumption (or just declaring it obvious by looking at the current blockchain state).
Even though the set of authorized contracts may change, I think we are making a stronger claim. Right now, our specs are not saying much about the set of authorized contracts at all, while this approach would say
"Given a set up process ending in the specified poststate, these are the only authorized contracts, unless a governance action is taken"

[MrChico]

This is definitely stronger than the claims we are making now, which would be satisfied by contracts that have Vat.wards[A] |-> 1 for all A.

[livnev]

Our argument about this issue for posterity:
https://gist.github.com/livnev/8982c804d2552becb709af67307be6c4