Tealer

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

Usage

To detect vulnerabilities

tealer detect --contracts file.teal

To run a printer

tealer print <printer_name> --contracts file.teal

To run the regular expression engine

tealer regex <regex_file.txt> --contracts file.teal

For additional configuration, see the Usage documentation.

Detectors

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.

Printers

Printers output dot files. Use xdot to open the files (sudo apt install xdot).

Regular expression

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
  ins2

If 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:

• tests/regex/regex.txt
• tests/regex/vote_approval.teal

Which will generate regex_result.dot.

How to install

pip3 install tealer

Using Git

git clone https://github.com/crytic/tealer.git && cd tealer
python3 setup.py install

We recommend to install the tool in a virtualenv.

Group configuration

To 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

License

Slither is licensed and distributed under the AGPLv3 license. Contact us if you're looking for an exception to the terms.