One of Tinyman’s latest issues has been integer overflows.
Questions:
Does PyTeal’s interpreter have functionality that deals with integer overflows or do we need to take them into account when designing a smart contract?
If we were to deal with them on our own (in the case of multiplication/division), how could we go about it?
Ideas in the case of a multiplication overflow:
if multiplication >= 2**64, then:do something about it.
I don’t really know what “do something about it” means in the context of an overflow.
In the case of divisions, I have no idea as to how to deal with overflows.
PyTEAL doesn’t perform checks on overflows, since PyTEAL compiler just generates TEAL source code from PyTEAL expressions (representing abstract syntax trees). PyTEAL does not execute TEAL programs on compiling.
The AVM default panics on overflows, underflows or division by zero. If panic is acceptable as expected application’s behaviour then you can stick with the default AVM reaction in this situations.
Otherwise you should:
Impose limitations on variables involved in operations that can possibly result in an overflow, underflow or division by zero;
or
Catch all the operations on which an overflow, underflow or division by zero may occur and handle it accordingly (differently from just panic as default);
Tinyman’s issue, occurred on Jan 1st/2nd, has nothing to do with the overflow condition.
This being said, there was a known minor corner case in Tinyman’s Price Oracle, for specific conditions of liquidity, in which an overflow could result in Tinyman’s LPs lock. This overflow condition has been addressed and solved in latest Tinyman’s contracts update.
You have to code your check by yourself, there is no Try/Catch like structure in PyTEAL nor as native TEAL opcode. If you come up with a general implementation, useful for other PyTEAL users, you can consider proposing it in PyTEAL-utils.
To add on @cusma’s excellent response, when working with fixed-size integer in critical software, you should be doing a semi-formal or formal range analysis.
Concretely, for any integer x in your smart contract, you want to show that it is always between values a and b, where a and b can be represented by the integer chosen (i.e., they fit in 64 bits)
To do that semi-formally, you first show that when initializing the smart contract, this is the case. (A trivial example is when the integer is 0 at the beginning and the lower bound a is also 0). Then you analyse all possible calls to the smart contract and show the following invariant:
if the integer x was between a and b before the call, then during the call and after the call, the integer x stays between a and b
This ensures that at any point x stays between a and b.
This analysis is complex and time-consuming but I believe it is of the outmost importance in critical software, such as smart contracts.
This kind of analysis is done in plane or rocket embedded software for example (often in a slightly more formal and automated way).
If you are dealing with floating point (which TEAL does not have), the analysis is even more complex, as floating point not only have issues with bounds (max and min values) but also with precision. But this is another story. Here, you would most likely need an expert to deal with a critical software with floating point.
