Tealer is a static analyzer for Teal code. It parses the Teal program, and builds its CFG. The analyzer comes with a set of vulnerabilities detectors and printers allowing to quickly review the contracts. In addition, tealer allows for custom path discovery through regular expression, and can be configured to follow the group information of the application.
- Usage
- Detectors: Vulnerabilities detectors
- Printers: Visual information
- Regular expression: Regular expression engine
- How to install
- Group configuration
To detect vulnerabilities
tealer detect --contracts file.tealTo run a printer
tealer print <printer_name> --contracts file.tealTo run the regular expression engine
tealer regex <regex_file.txt> --contracts file.tealFor additional configuration, see the Usage documentation.
| Num | Detector | What it detects | Applies To | Impact | Confidence |
|---|---|---|---|---|---|
| 1 | is-deletable |
Deletable Applications | Stateful | High | High |
| 2 | is-updatable |
Upgradable Applications | Stateful | High | High |
| 3 | unprotected-deletable |
Unprotected Deletable Applications | Stateful | High | High |
| 4 | unprotected-updatable |
Unprotected Upgradable Applications | Stateful | High | High |
| 5 | group-size-check |
Usage of absolute indexes without validating GroupSize | Stateless, Stateful | High | High |
| 6 | can-close-account |
Missing CloseRemainderTo field Validation | Stateless | High | High |
| 7 | can-close-asset |
Missing AssetCloseTo Field Validation | Stateless | High | High |
| 8 | missing-fee-check |
Missing Fee Field Validation | Stateless | High | High |
| 9 | rekey-to |
Rekeyable Logic Signatures | Stateless | High | High |
| 10 | constant-gtxn |
Unoptimized Gtxn | Stateless | Optimization | High |
| 11 | self-access |
Unoptimized self access | Stateless | Optimization | High |
| 12 | sender-access |
Unoptimized Gtxn | Stateless | Optimization | High |
For more information, see
- The Detector Documentation for information on each detector
- The Detection Selection to run only selected detectors. By default, all the detectors are ran.
| Num | Printer | What it prints |
|---|---|---|
| 1 | call-graph |
Export the call graph of contract to a dot file |
| 2 | cfg |
Export the CFG of entire contract |
| 3 | human-summary |
Print a human-readable summary of the contract |
| 4 | subroutine-cfg |
Export the CFG of each subroutine |
| 5 | transaction-context |
Output possible values of GroupIndices, GroupSize |
Printers output dot files.
Use xdot to open the files (sudo apt install xdot).
Tealer can detect if there is a path between a given label and a set of instruction using the regex subcommand: tealer regex regex.txt --contracts file.teal.
The Regular expression file must be on the form:
label =>
ins1
ins2If there is a match, tealer will generate a DOT file with the graph.
For an example, run tealer regex tests/regex/regex.txt --contract tests/regex/vote_approval.teal, with:
Which will generate regex_result.dot.
pip3 install tealer
git clone https://github.com/crytic/tealer.git && cd tealer
make devTo help tealer reasons about applications that are meant to be run in a group of transaction, the user can provide the group information through a configuration file:
- See the ANS configuration example
- See Lightweight group information specification discussion.
The file format is still in development, and it is likely to evolve in the future
Tealer is licensed and distributed under the AGPLv3 license. Contact us if you're looking for an exception to the terms.