Code Patterns of False Positives for Transaction Field based detectors

[S3v3ru5]

Detectors such as feeCheck, canCloseAccount, canCloseAsset, rekeyTo traverse the CFG and detect if there's a check involving a transaction field.

txn [Fee | CloseTo | AssetCloseTo | RekeyTo]
[int ... | (addr ... | global ZeroAddress)]
[ == | < | > | .. ]

The same checks could be implemented following different patterns:
1.) Verifies transaction index in the group and then checks the transaction field by accessing it with gtxn INDEX FIELD. issue #75
e.g

txn GroupIndex
int 0
==
assert
gtxn 0 AssetCloseTo
global ZeroAddress
==
assert

2.) Verify the GroupSize is certain value and verify fields of all transactions in the group. issue #87
e.g

global GroupSize
int 2
==
...
gtxn 0 CloseRemainderTo
global ZeroAddress
==
&&
gtxn 1 CloseRemainderTo
global ZeroAddress
==
&&
...

3.) Using a loop to iterate over all transactions in the group and verifying the transaction field.
e.g

12: int 0
13: store 9

14: label1:
15: load 9
16: Gtxns RekeyTo
17: global ZeroAddress
18: ==
19: assert
20: load 9
21: int 1
22: +
23: store 9
24: load 9
25: global GroupSize
26: <
27: bnz label1

Few false positives stem from not using pruning for stateless detectors.
e.g. Account can be closed only if the transaction is a payment transaction. canCloseAccount doesn't need to explore paths where the path is taken only if transaction type is not payment. And also canCloseAccount can only explore paths which are taken if and only if the transaction type is payment. Similar pruning conditions can be considered for canCloseAsset detector.