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 runtime verification for monitoring contract execution (for example for preventing pitfalls dynamically).
Motivation
Monitors are a defensive mechanism. The main idea is to be able to take any smart contract and extend it with a protective wrapper that is executed at the end guaranteeing constraints of the execution (failing otherwise).
It is common that a contract calls another asking for information (and maybe paying beforehand for it), however, currently, there is nothing the contract can do if it does not receive a call back with the requested information. Monitors can ensure that the contract received the information it asked/payed for, and failing if it does not happen.
Another case where monitors are useful is when we want to limit how much tezos are spend overall in a transaction.
Implementation
Monitors are special functions that can only be called by the contracts they belong to, are allowed to modify the storage and fail but not emit other operations.
We want monitors to run after all other operations finish their execution. Right now [we think] this is not implementable, because the control flow does not return to the caller.
Since BFS is used to traverse the graph call, we need to insert the monitor at the end of the last level of it. One option can be to insert the monitor at the end of the first level and have it reinsert itself at the end of the next level (but there is currently no way to either know upfront the depth or to obtain whether this is the last level or there are no pending calls). Another option would be to add a special queue for monitors which will be executed after the queue with the internal operation is empty (effectively mixing BFS for normal operations and DFS for monitors).
In a full DFS, and without adding any extra feature to Michelson, we can have simpler monitors that only control the operations in a subtree of the call graph (which cover many practical applications). This can be achieved by just appending to the internal operations list a call to it. When the monitor is called all the other operations in the subtree have already executed and therefore their effects in this contract are visible and can be verified by the monitor.
