Skip to content

README-dev.md

Latest commit

 

History

History
214 lines (120 loc) · 11.4 KB

README-dev.md

File metadata and controls

214 lines (120 loc) · 11.4 KB

Overview

The following file contains an introduction to the files in this repository, an explanation of the output of ScType, an introduction to core components of ScType, and how to build and run the source code from scratch.

Please refer to README.md for information on pulling and running the Docker image for ScType.

Introduction to the Repository

|ScType

|--- README.md

|--- README-dev.md

|--- LICENSE

|--- test_benchmark_final.sh

|--- create_typefile.md

|--- financial_type_keys.py

|--- expected_results.txt

|--- icse2024-paper1049.pdf

|--- icse2024-paper1049-supplementary_material_upload.pdf

|--- run_results

|--- slither/detectors/my_detectors

|--- Benchmark

  • README.md contains a brief description of ScType and how to pull and run an executable Docker image of ScType.

  • README-dev.md is the file you are reading now.

  • LICENSE contains the license for ScType.

  • test_benchmark_final.sh is the script used for running ScType on the dataset provided in the paper. More details can be found in the "Reproducing Results in the Paper" section.

  • create_typefile.md contains instructions on how to manually build type files.

  • financial_type_keys.py stores a copy of a table from tcheck_parser.py (which is located in the directory slither/detectors/my_detectors) that contains the mappings of financial types and their keys. More information can be found in create_typefile.md.

  • expected_results.txt stores a copy of the ouput that should be produced from running the Docker image againsts the dataset in the paper. See the "Dataset Evaluation" subsection of the "Reproducing Results in the Paper" section for more details.

  • icse2024-paper1049.pdf and icse2024-paper1049-supplementary_material_upload.pdf contain the PDF files for the paper written for this tool, Towards Finding Accounting Errors in Smart Contracts and its supplementary materials.

  • run_results is a repository that contains the expected results from running ScType on the dataset used in the paper. More information can be found in the README.md file located there.

  • slither/detectors/my_detectors is a directory that contains all of the files that are used by ScType.

  • Benchmark is a directory that contains the testing dataset. It is not provided in this repository, but is available through the Docker Image. Each subdirectory within Benchmark contains the code for one smart contract project. They were obtained from this repository, as mentioned in the paper. The true positive reports came from past reports from Code4rena, a smart contract security vendor that hosts smart contract auditing competitions.

To see the specific directory within each project where ScType is run, please check test_benchmark_final.sh.

This repo does not include the Benchmark dataset in the paper, however the Docker image does.

All other code belongs to Slither.

Understanding ScType Output

For each project, ScType will output warnings corresponding to code impacted by an erroneous accounting bug.

Individual warnings are output with green text with the following format:

>typecheck error: Var name: A Func name: B in C

This warning means that the intermediate representation (IR) variable "A" located within function with name "B" is incorrect, and the problematic operation or declaration is within IR expression "C".

The total number of warnings reported by the tool are reported in the following line in the following format:

>XXX analyzed ... XXX result(s) found

Expected warnings for each project are reported in the line starting with "[*]":

>[*] Expected XXX warnings for XXX

For most test cases, the number of identified true positives will be less than the reported warnings. This is due to the propogation of a single accounting error throughout multiple operations within the contract.

For a small number of examples, the number of reported warnings may differ by a slight amount from the number of reported number of warnings in the paper, expected_results.txt file, and the run_results repository. This is due to the order of certain underlying single-static-assignment representations generated by Slither being inconsistent, in particular for Phi propagation representations.

Introduction to Core Components

The following section describes the core components of ScType and where they are located.

Abstract Type

The abstract type as introduced by Fig. 6 in our paper is defined in ExtendedType.py (which is located in the directory slither/detectors/my_detectors). It provides additional information to variables, such as token units, scaling factor, and financial type.

In particular, for every variable intermediate representation (IR) produced by Slither, there is a field, extok, that contains the ExtendedType object defined in ExtendedType.py.

For development or debugging, simply inputting the following python code print({var}.extok), where {var} is a variable IR, will display information about the variable including the three aforementioned attributes, as well as fields and addresses.

Type File Parsing

The type file provides initial abstract types for selected global variables or function parameters. Detailed instructions can be found in create_typefile.md

All of the type files for the testing dataset have already been provided; when counting the number of annotations made for type files, we exclude the ones which provide the return values of functions not in scope. We reason that this is a common cost for all static analysis tools and is an effort that we plan to improve upon in furture work.

The parser for the type file is located in tcheck_parser.py . It checks each annotation that follows the format as described in create_typefile.md, and stores the abstract types in dictionaries for use later in type checking. Each variable type has its own dictionary, and can be checked within tcheck_parser.py.

Typechecking Engine

The propogation and typechecking of the tool are implemented in tcheck.py and tcheck_propogation.py (which are both located in the directory slither/detectors/my_detectors). tcheck.py receives the representation from Slither, and performs the typechecking of individual operations within the function check_type().

In particular, tcheck.py receives the SSA from Slither, and first determines which contracts are marked to be typechecked. More details on how to do so can be found in create_typefile.md, located in this directory.

For the contracts that have been marked, Slither typechecks them one-by-one via the function _tcheck_contract(). Per each contract, the global variables are read, and assigned initial type info if annotations have been provided in the type files. This is done through the function _tcheck_contract_state_var().

Then, each individual function is used as an entry point and typechecked. This is done in the function _tcheck_function().

In particular, the function _check_type() typechecks each operation or declaration in the SSA nodes, by calling the appropriate helper function. Helper functions include type_bin(), which checks binary operations, type_fc(), which checks calls to functions with the contract, and type_hlc(), which checks calls to functions outside of the contract.

Certain helper functions make calls to functions stored in tcheck_propogation.py.

tcheck_propogation.py stores functions related to the propogation and comparison of the abstract types. For example, function pass_ftype() takes as parameters a LHS variable, a RHS variable, and the name of a binary operation, and checks to see if it is in violation of the financial type propogation rules.

We have selected one of the helper functions to explain more in detail, in particular type_bin_add(), which is used to typecheck addition operations.

Explanation for function type_bin_add()

type_bin_add() takes as parameters: a destination variable (dest), the left operand variable of the addition (lir), and the right operand variable of the addition (rir).

If both operands are not undefined or constant variables, the token units are compared through the function calls compare_token_type() and handle_trace().

If the token units are incompatible, an error is reported via the function add_errors().

If not, the scaling factors of the operands are compared and the result is passed to the destination variable via the function call bin_norm().

Additionally, type_bin_add() checks whether or not the addition operation violated any financial type rules by calling pass_ftype(), which in turn calls the pass_ftype() function in tcheck_propogation.py that was previously mentioned.

Then, the appropriate token units are assigned to the destination variable, and type_bin_add() returns.

Build and Run from Source Code

To download a copy of ScType, clone the repository like so:

git clone https://github.com/NioTheFirst/ScType.git

To compile the source code, navigate to the home directory of ScType and run:

pip3 install . --upgrade

To run ScType, it is required for the target file(s) to be compiled. Hence, any dependencies for the files must also be installed. These instructions are usually provided by the developers of smart contracts.

Once the depencencies have been installed, navigate to the directory of the file and run:

slither --detect tcheck {target_file_name}

To run ScType against a directory, run:

slither --detect tcheck .

ScType will be able to automatically typecheck calls to any functions as long as the function is located within the directory.

However, ScType needs type files to be made for each contract that shall be typechecked. Details on how to do so can be found in the create_typefile.md file.

Dataset Evaluation using the Source Compilation

The dataset used to test ScType has been pushed intp a separate Github repository named ScType_Data.

It can be cloned by running the command:

git clone https://github.com/NioTheFirst/ScType_Data.git

It requires 30GB of space and take around 50 minutes to clone from Github.

Once the repository has been cloned, move the directory named Benchmark from ScType_Data to the ScType directory cloned in the first section by running the command:

mv /path/to/ScType_Data/Benchmark /path/to/ScType

Replace /path/to/ScType_Data/Benchmark and /path_to_ScType as needed.

Then, it is necessary to install the Soilidity compilations used in the various projects in the dataset.

To do so, install the solc-select package by running:

pip3 install solc-select

then, run the following commands:

solc-select install 0.6.12
solc-select install 0.7.6
solc-select install 0.8.0
solc-select install 0.8.1
solc-select install 0.8.3
solc-select install 0.8.4
solc-select install 0.8.6
solc-select install 0.8.7
solc-select install 0.8.9
solc-select install 0.8.10
solc-select install 0.8.12
solc-select install 0.4.25 && solc-select use 0.4.25

Once the move is complete and the Solidity compilations have been downloaded, evaluation of ScType against the dataset can proceed as directed in the "Usage" section of the README.md.