# Extensions to Tezos to control reentrancy and more
**URL:** https://forum.tezosagora.org/t/extensions-to-tezos-to-control-reentrancy-and-more/1918
**Category:** Research and Development
**Created:** [May 18, 2020, 3:20pm UTC](https://forum.tezosagora.org/t/extensions-to-tezos-to-control-reentrancy-and-more/1918 "2020-05-18T15:20:55Z")
**Posts on this page:** 2
**Page:** 1
### Author:  [@mcapretto](https://forum.tezosagora.org/u/mcapretto)
#### Post date: [May 18, 2020, 3:20pm UTC](https://forum.tezosagora.org/t/extensions-to-tezos-to-control-reentrancy-and-more/1918/1 "2020-05-18T15:20:55Z")
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.
---
### Author:  [@galfour](https://forum.tezosagora.org/u/galfour)
#### Post date: [May 18, 2020, 4:16pm UTC](https://forum.tezosagora.org/t/extensions-to-tezos-to-control-reentrancy-and-more/1918/2 "2020-05-18T16:16:33Z")
Hi,
I have just sent you an email to you and prof. Cesar Sanchez to discuss this.