Purpose

ScType is a static analysis tool written in Python3 to detect accounting errors in Solidity smart contracts. It can be found on Github.

ScType leverages the single-static-assignment representation produced by Slither to perform abstract type inference. It assigns initial abstract types to select variables based on a type file or inference from the code. Then, the abstract types are propogated throughout the contract based on the produced representation and typechecked accordingly.

ScType checks each individual function within the code. Users are able to specify the abstract types of the initial function parameters through the type file, however the majority of abstract type assignment to variables is done through propogation.

ScType can handle simple variables as well as arrays and object fields. It can also handle function calls as long as the function is located within the user-defined scope. This includes calls to functions outside of the current file being checked. See the section "Build and Run from Source Code" for more information on usage and scope.

In the following sections, we describe how to pull a Docker image for ScType, and how to reproduce the key results from our paper using the image.

The Docker Image requires 24GB of space.

ScType is applying for:

1. Available. ScType is publically available on Github. We have also provided a runnable image of the tool on Dockerhub and provide instructions to pull and run below.

2. Reusable. We provide detailed instructions on how to reproduce the results in the paper. We also provide an explanation of key components of ScType and how developers can leverage our tool in the file README_dev.md in this directory. Finally, ScType is built on top of Slither, a well-known open-source project. Using open-source code improves reusability by making the code easier to understand.

Provenance

ScType is publically available in this repository on Github, and a runnable docker image of the tool can be found on Dockerhub. Please refer to the "Setup" section for more details.

The DOI for this repository on Zenodo is provided below:

The pre-print for the corresponding paper to this artifact, Towards Finding Accounting Errors in Smart Contracts, can be found in this repository. For convenience, the link is provided.

Setup

The following subsections detail how to pull the Docker image and how to understand the output of the artifact.

Pulling the Docker Image

Docker needs to be installed in order to pull the image. It can be installed here.

To pull the Dockerhub image for ScType, ensure there is at least 24 GB of storage available and run the following command:

docker pull icse24sctype/full:latest

The pull should take around 40 minutes to finish.

To run the image as a container, run the following command:

docker run -it icse24sctype/full

Doing so should create an interactable shell. Commands in the "Usage" section below should be run inside that shell.

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 number of functions checked are reported in the following format:

>Function count: XXX

The number of annotations are reported in the following format:

>Annotation count: XXX

Please note that some outputs will contain more than one set of Annotation count and Function count. This is due to ScType checking more than one file. In such a scenario, disregard all but the last pair of Annotation count and Function count in a singular ScType execution.

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

This line represents the end of a singular ScType execution. For certain projects, ScType is run more than once.

The total expected warnings from all ScType executions for each project are reported in the line starting with "[*]":

>[*] Expected XXX warnings for XXX

The total execution time of all ScType executions is reported in the following format:

>Elapsed time: XXX.XXX seconds

Usage

The following subsections detail a basic usage command to test the artifact docker image installation, and how to reproduce the major results in our paper.

Basic Usage Command

In order to test the installation of the image, please run the following command within the interactable shell produced by the Docker Image.

./test_benchmark_final.sh 1

Refer to the "Setup" section for instructions on how to download the Docker Image and produce the interactable shell.

The output of the command should look like the following screenshot:

This output is produced by running ScType against the first smart contract project in our dataset, MarginSwap.

Dataset Evaluation

To run ScType against the entire dataset, run the following command within the interactable shell:

./test_benchmark_final.sh

The entire execution will take 10 minutes.

The expected results of the batch execution can be found in expected_output.txt.

To run ScType against individual projects in the dataset, append the index of the project to the previous command.

For example, Vader Protocol p1 is the 2nd project. Hence, to only run ScType against it, input the following command:

./test_benchmark_final.sh 2

Individual results are found in the run_results repository. See the README.md file within for more information.

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_output.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.

We briefly go over the reproduceable results in the paper as follows.

Table 3: Evaluation Results

The data from table 3 on page 8 of our paper was obtained by running ScType against the entire dataset:

The number of annotations was obtained through the metric defined in the "Type File Parsing" section of the file README-dev.md, which can be found in this directory. It can be compared to the Annotation count output.

The number of functions checked can be compared to the Function count output.

For projects 15, 17, and 19, ScType was run more than once. In this case, the number of annotations and number of function checked was obtained by adding the annotations and function checked for each execution. Please refer to the "Understanding ScType Output" subsection for more details on how to identify the end of an ScType execution.

The reported number of warnings is directly the amount reported by the tool.

The number of true positives, false positives, missed-type-errors and not-type-errors were determined by manual inspection of the warnings. The expected results and distribution of true and false positives can be found in the run_results directory. See the README.md file within for more details.

The execution time of the tool was obtained by using a clock within the testing scripts. It can be compared to the Elapsed time output.