crytic / tealer

Static Analyzer for Teal
GNU Affero General Public License v3.0
62 stars 14 forks source link

Update Fee field analysis to use unknown values #131

Closed S3v3ru5 closed 1 year ago

S3v3ru5 commented 1 year ago

While tracking the max possible fee, fee field analysis only considers comparisons against int values.

e.g

1.)
txn Fee
int 10000
<=
assert
2.)
txn Fee
pushint 1000
>=
bnz fail

For the above examples, Fee field analysis is able to determine that Fee should be less than 10000 in 1 and 1000 in 2. But when the compared value is not an instruction that pushes an int value, the analysis does not consider that comparison.

False positive examples:

txn Fee
global MinTxnFee
<=
assert
txn Fee
global MinTxnFee
int 2
*
<=
assert

This PR represents non-int compared values using a single value x whose semantics are:

  1. 0 < x < MAX_UINT64
  2. x is greater than all the known possible max fees in the contract.

x represents an unknown bounded integer.

if the max possible fee of an execution path is x it only means that the Fee is checked to be less than or equal to some value and is bounded by some unknown integer.

S3v3ru5 commented 1 year ago

Builds on #130