You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A common occurrence in smart contracts are calls to contracts with unknown code, whether for executing a simple eth payment, proxy/multisig actions or delegating control for a flash loan.
Such behaviour is naturally hard to specify, since the entire point is that these functions admit unspecified behaviour. Nevertheless, we want to be able to specify exactly what these functions do with respect to the domain for which their behaviour is defined, and express that beyond this domain, anything is allowed.
As an example, if we have a function with a flash loan, we have a clear expectation on the poststate of the contract itself, expressing that the loan need be paid back, while allowing any other part of the world state to change in ways we do not know.
Here's a suggested syntax for making such claims:
behaviour flash of A
interface flash(address flasher, uint amount)
iff in range uint256
token.balanceOf[A] + flashFee
storage A.token
balanceOf[A] => balanceOf[A] + A.flashFee
storage _
_
the meaning being that a call to A.flash(flasher, amount) will increment the A.token balance of A by whatever the storage variable flashFee is set to, and that, for any contract that isn't A or A.token, arbitrary changes to storage may occur.
In other words, the syntax
storage _
_
would be shorthand for something along the lines for "for all addresses X that are not the main contract of the spec nor any of the other contracts mentioned to in the spec, the storage contents of X can change arbitrarily".
Before I get to how to prove claims like this, let me say some things about the syntax.
First of all, I think we need a more general keyword than storage, since nonces and balances may also change, new addresses can be created, and so on. state is an obvious candidate that was also brought up before. Can every instance of storage be changed into state? Should storage be a subheader of state?
If we continue with the EVM opcodes in CAPS idea, then maybe just generalizing storage to state and allow for references to BALANCE and NONCE under this header could be nice:
behaviour f of A
interface f()
state
x => x + 1
BALANCE => BALANCE + 1
Second of all, it needs to clarified what a "contract mentioned in the spec" means. Every contract with a storage/state header present? In the current syntax, we can actually read and refer to variables of other contracts without introducing a storage header for them. Should we allow storage writes to read-only contracts? I'm don't think so... Can this be made clearer in the syntax?
Lastly, I would like to make a note on proving strategies for these types of specs. This is a crude write up and I apologize if it's hard to follow, but I needed to get this down. Refinements can come later.
In order to determine which branches to explore, we first need to establish a functional dependency for all of the specs of all of the "contracts mentioned in the spec" for which behaviour is defined. A spec S is functionally dependent on all the specs which can write to the reads of S.
Now, when encountering a call to an unknown contract, we branch and explore:
The case in which the external call does not enter any of the "contracts mentioned in the spec", and we simply carry on with exploring the rest of the function after the call.
For every "contract mentioned in the spec" and any spec which can modify state, apply the spec and notice which storage items can change (the changeset). We now branch again into
the case where the external call is done and we are back in the main function with all the storage items in the changeset set to arbitrary values.
explore any of the specs again, now with any storage item in the changeset set to an arbitrary value. If more variables can change, add them to the changeset and repeat. If the changeset has not grown, we do not need to continue looping here.
The text was updated successfully, but these errors were encountered:
It should be noted that by treating anything in the changeset as a new, arbitrary value, we are essentially forgetting information, which is a little dangerous – this is an overly pessimistic strategy. The actual values that any variable here can take is rather inductively defined by the behaviour constructors. If x is ensured to remain < 9 under the inductive system then resetting it to just a new unconstrained y, we need to be careful not to introduce unsoundness in our system.
As long as we are asserting the poststate of the defined domain as a function of its input, I don't think this will be an unsound strategy, only incomplete. But if we allow for existentially bound variables in the poststate, this strategy is definitely too coarse.
For a more refined approach, we would need to consider not only the fixpoint of the changeset, consisting of storage locations which may change, but the fixpoint of the possible values these storage locations can take. But this is much harder (as in likely undecidable) to do in general.
A common occurrence in smart contracts are calls to contracts with unknown code, whether for executing a simple eth payment, proxy/multisig actions or delegating control for a flash loan.
Such behaviour is naturally hard to specify, since the entire point is that these functions admit unspecified behaviour. Nevertheless, we want to be able to specify exactly what these functions do with respect to the domain for which their behaviour is defined, and express that beyond this domain, anything is allowed.
As an example, if we have a function with a flash loan, we have a clear expectation on the poststate of the contract itself, expressing that the loan need be paid back, while allowing any other part of the world state to change in ways we do not know.
Here's a suggested syntax for making such claims:
the meaning being that a call to
A.flash(flasher, amount)
will increment theA.token
balance ofA
by whatever the storage variableflashFee
is set to, and that, for any contract that isn'tA
orA.token
, arbitrary changes to storage may occur.In other words, the syntax
would be shorthand for something along the lines for "for all addresses
X
that are not the main contract of the spec nor any of the other contracts mentioned to in the spec, the storage contents ofX
can change arbitrarily".Before I get to how to prove claims like this, let me say some things about the syntax.
First of all, I think we need a more general keyword than
storage
, since nonces and balances may also change, new addresses can be created, and so on.state
is an obvious candidate that was also brought up before. Can every instance ofstorage
be changed intostate
? Shouldstorage
be a subheader ofstate
?If we continue with the EVM opcodes in CAPS idea, then maybe just generalizing
storage
tostate
and allow for references to BALANCE and NONCE under this header could be nice:Second of all, it needs to clarified what a "contract mentioned in the spec" means. Every contract with a
storage
/state
header present? In the current syntax, we can actually read and refer to variables of other contracts without introducing astorage
header for them. Should we allow storage writes to read-only contracts? I'm don't think so... Can this be made clearer in the syntax?Lastly, I would like to make a note on proving strategies for these types of specs. This is a crude write up and I apologize if it's hard to follow, but I needed to get this down. Refinements can come later.
In order to determine which branches to explore, we first need to establish a functional dependency for all of the specs of all of the "contracts mentioned in the spec" for which behaviour is defined. A spec
S
is functionally dependent on all the specs which can write to the reads ofS
.Now, when encountering a call to an unknown contract, we branch and explore:
changeset
). We now branch again intochangeset
set to arbitrary values.changeset
set to an arbitrary value. If more variables can change, add them to thechangeset
and repeat. If thechangeset
has not grown, we do not need to continue looping here.The text was updated successfully, but these errors were encountered: