I agree that the call order used in Tezos is unusual and difficult to reason with, however there is a way in which the balance can be properly updated in BFS and maybe it can lead to a more general mitigation for the call injection vulnerability. The idea is the following:
- In the storage we add a variable pending_to_transfer that keeps track of the amount of Tezos that is going to be transferred from this contract but has not been transferred yet.
- We add an entry_point update that takes as argument transferred_tezos and decreases pending_to_transfer by it. This entry point can only be called by SELF and does not accept tezos.
- Whenever we make a transfer op for t tezos we increase pending_to_transfer by t and in the list of emitted operations we add next to op a call to update with parameter t.
Then, since BFS is used, this both operations are executed back to back. Hence, the contract can know immediately when op was executed.
Therefore, the current_balance is actually balance - pending_to_transfer.
After adding these modifications, the Receiver contract in Figure 4 will be:
type parameter is
Receive of unit
| Set of unit
| Update of tez
type storage is
record
current_balance : tez;
pending_to_transfer : tez;
end
function entry_Receive (const store : storage) : (list(operation) * storage) is
block {
const alice : address = ("some_address": address);
const to_contract: contract(unit) = get_contract(alice);
const op1 : operation = transaction(unit, amount, to_contract);
store.pending_to_transfer := store.pending_to_transfer + amount;
const self_update: contract(tez) = get_entrypoint("%update", self_address);
const op2 : operation = transaction(amount, 0tz, self_update);
op_list := list op1; op2; end;
} with (op_list, store)
function entry_Set (const store : storage) : (list(operation) * storage) is
block {
if(amount > 0mutez) then {
failwith("Do not send tezos")
} else{
store.current_balance := balance - store.pending_to_transfer;
}
} with ((nil : list(operation)), store)
function entry_Update(const transfered_tezos : tez; const store : storage) : (list(operation) * storage) is
block {
if(amount > 0mutez) then {
failwith("Do not send tezos")
} else if (sender =/= self_address) then {
failwith("Do not call update from outside this smart contract")
} else {
store.pending_to_transfer := store.pending_to_transfer - transfered_tezos
}
}
with ((nil : list(operation)), store)
function main (const action : parameter; const store : storage) : (list(operation) * storage) is
case action of
Receive(x) -> entry_Receive(store)
| Set(x) -> entry_Set(store)
| Update(t) -> entry_Update(t,store)
end
Notice that in some smart contracts it is possible for the current_balance to be negative (here, it has tez type to simplify the code) without that implying that the whole transaction will fail.