Extensions to Tezos to control reentrancy and more

My name is Margarita Capretto. I am doing research with prof. Cesar
Sanchez at the IMDEA Software Institute. We are working on different
lines of applications of formal methods for Tezos smart contracts,
including (1) verification of Ligo contracts and (2) runtime
verification for monitoring contract execution (for example for
preventing pitfalls dynamically).

While playing with smart contracts and their verification, we
envisioned some extensions to Tezos that would be very useful:

  1. Provide contracts access to the call graph: this way smart
    contracts (or wrapper code inserted for the purpose of monitoring)
    would be able to differentiate between reentrant calls and external
    calls and change their behaviour accordingly. As far as we
    understand, it is not possible to write a smart contract in Tezos
    that rejects only reentrant calls.

  2. Once all emitted operations are executed, return the control to the
    caller contract to perform read-only operations and then decided
    whether to accept or reject the whole transaction known the
    effect. For example, a smart contract or a wrapper monitoring code
    can check how much of its balance was spent overall in the
    transaction to accept or reject. We envision a simple monitoring
    language that allows to express constraints on the effect of the
    transaction (balanced used, reentrancy, etc) and create
    automatically monitors that reject upon violations of the
    constraint. This enables writing super-imposition code that works
    (provably correct) for every contract monitored.

  3. Alongside their tokens and storage, allow contracts to access and
    manipulate “intermediate variables”. These variables will be
    initialized every time a new transaction is started (a new block),
    can be read and updated by the contract and they will live as long
    as the transaction lives. This variables would allow, among other
    things, to implement locks, know the actual available balance (the
    operation BALANCE in Michelson is updated when the emitted
    operations are executed, so sometimes it does not reflect the
    actual amount of tokens available to spend) and, again, distinguish
    reentrant calls from external calls.

We can discuss particular examples if you wish.



I have just sent you an email to you and prof. Cesar Sanchez to discuss this.