Aletheia

Aletheia is a mutation tool for Solidity Smart Contracts invariants validation and verification.

Table of Contents

• Installation
• Configuration
• CLI Usage
• Mutation Operators

Installation

To install sumo run npm install @geriul/aletheia

Implement new operators

Create the operator into the src/operators/FOLDER/OPERATOR.js Choose the most suitable FOLDER where implement the OPERATOR

Update the mutationGenerator.js file adding:

const IDOperator = require('./FOLDER/OPERATOR')

[...]

module.exports = {
  IDOperator: IDOperator,
}

Update the operator.config.json file adding:

{
   [...]
   "ID": true,
}

Update the mutationRunner.js file adding:

const mutGen = new mutationGenerator.MutationGenerator([
  [...], "ID"
].map(operator => new mutationGenerator[`${operator}Operator`]()));

If you want to reflect changes to your package, update the package version into package.json.

"version": "1.0.1"

Then push the changes to npm repository.

npm publish --access public 

Finally, install.

npm install @geriul/aletheia

Otherwise link the tool to the local changes.

Configuration ⚙️

Before using Aletheia you must specify your desired configuration in a sumo-config.js in the root directory of your project. The sumo-config.js is automatically generated when SuMo is installed.

Here's a simple example of sumo-config.js:

module.exports = {  
      buildDir: "auto",                               //build directory of the SUT (auto detect)
      contractsDir: "auto",                           //contract directory of the SUT (auto detect)
      testDir: "auto",                                //test directory of the SUT (auto detect)
      skipContracts: ["interfaces", "mock", "test"],  // Relative paths from contractsDir
      skipTests: [],                                  // Relative paths from testsDir
      testingFramework: "auto",                      //testing framework (auto detect)
      minimalOperators: false,                       // use minimal mutation rules
      randomSampling: false,                         //use random mutant sampling
      randomMutants: 100,                            //if random sampling is enabled, generate 100 mutants max
      testingTimeOutInSec: 500                       //testing time-out for a mutant
}

CLI Usage

Selecting the Mutation Operators

Before starting the mutation process you can choose which mutation operators to use:

| Command | Description | Usage | Example | |---------------|------------------------------------|--------------------------|-------------------------------------| | list | Shows the enabled mutation operators. | npx/yarn aletheia list | $ npx aletheia list | | enable | Enables one or more mutation operators. If no operator IDs are specified, all of them are enabled. | npx/yarn aletheia enable [...ID] | $ npx aletheia enable $ npx aletheia enable AOR BOR | | disable | Disables one or more mutation operators. If no operator IDs are specified, all of them are disabled. | npx/yarn aletheia disable [...ID] | $ npx aletheia disable $ npx aletheia disable FVR |

Viewing the available mutations

| Command | Description | Usage | Example | |---------------|------------------------------------|--------------------------|-------------------------------------| | lookup | Generates the mutations and creates reports without starting mutation testing. | npx/yarn aletheia lookup | $ npx aletheia lookup | | mutate | Generates the mutations and saves a copy of each .sol mutant to to ./aletheia/mutants. | npx/yarn aletheia mutate | $ npx aletheia mutate |

Running Mutation Testing

| Command | Description | Usage | Example | |---------------|------------------------------------|--------------------------|-------------------------------------| | pretest | Runs the test suite on the original smart contracts to check if all tests pass and can be successfully evaluated. Pretest is automatically run when aletheia test is executed. | npx/yarn aletheia pretest | $ npx aletheia pretest | | test | Starts the mutation testing process. You can also choose a single mutant / an interval of mutants to be tested by sepcifying <startHash> and (optionally) <endHash>.| npx/yarn aletheia test <startHash> <endHash> | $ npx aletheia test $ npx aletheia test mbc5e8f56 mbg5t86o6| | restore | Restores the SUT files to a clean version. This should be executed if you suddenly interrupt the mutation process. Note that the restore command overwrites your codebase with the files stored in the aletheia/baseline folder. If you need to restore the project files, make sure to do so before performing other operations as the baseline is automatically refreshed on subsequent preflight or test runs.| $ npx/yarn aletheia restore | $ npx aletheia restore|

Viewing the results

Aletheia automatically creates a sumo\results folder in the root directory of the project with the following reports:

• mutations.json: List of mutations in json format, synchronoysly updated during testing.
• index.html: A simple web display of the results (you can view this using VSCode extensions like Live Server). From here, you can also download a csv with the results.
• \mutants: Folder with mutated .sol source files (only if generated with sumo mutate)

Mutation Operators 👾

Aletheia includes the following Traditional and Solidity-specific operators. Note that not all mutation operators are enabled by default.

Traditional Mutation Operators

| Operator | Name | Mutation Example | Enabled by Default | Minimal Available | | ------ | ------ | ------ | ------ | :----: | | ACM| Argument Change of overloaded Method call | overloadedFunc(a,b); → overloadedFunc(a,b,c); | Y | N | | AOR | Assignment Operator Replacement | += → = | Y | N | | BCRD | Break and Continue Replacement and Deletion | break → continue → break | Y | N | | BLR | Boolean Literal Replacement | true → false | Y | N | | BOR | Binary Operator Replacement | + → - < → >= | Y | Y | | CBD | Catch Block Deletion | catch{} → | Y | N | | CSC | Conditional Statement Change | if(condition) → if(false) else{} → | Y | N | | ER | Enum Replacemet | enum.member1 → enum.member2 | Y | Y | | ECS | Explicit Conversion to Smaller type | uint256 → uint8 | Y | N | | FCD | Function Call Deletion | foo() → | Y | N | | HLR | Hexadecimal Literal Replacement | hex\"01\" → hex\"random\"| Y | N | | ILR | Integer Literal Replacement | 1 → 0 | Y | N | | LCS | Loop Statement Change | while(condition) → while(false) | Y | N | | OLFD | Overloaded Function Deletion | function overloadedF(){} → | Y | N | | ORFD | Overridden Function Deletion | function f() override {} → | Y | N | | SKR | Super Keyword Replacement | x = getData() → x = super.getData() | Y | N | | SLR | String Literal Replacement | "string" → "" | Y | N | | UORD | Unary Operator Replacement and Deletion | ++ → -- ! → | Y | Y |

Solidity Mutation Operators

| Operator | Name | Mutation Example |Enabled by Default | Minimal version available | | ------ | ------ | ------ | ------ | :----: | | AVR | Address Value Replacement | 0x67ED2e5dD3d0... → address.this()| Y | Y | | CCD | Contract Constructor Deletion | constructor(){} → | Y | N | | DLR | Data Location Keyword Replacement | memory → storage | N | N | | DOD | Delete Operator Deletion | delete → | Y | N | | ETR | Ether Transfer function Replacement | delegatecall() → call() | Y | Y | | EED | Event Emission Deletion | emit Deposit(...) → /*emit Deposit(...)*/ | Y | N | | EHD | Exception Handling Deletion | require(...) → /*require(...)*/ | Y | N | | FVR | Function Visibility Replacement | function f() public → function f() private | N | Y | | GVR | Global Variable Replacement | msg.value() → tx.gasprice() | Y | Y | | MCR | Mathematical and Cryptographic function Replacement | addmod → mulmod keccak256 → sha256 | Y | Y | | MOD | Modifier Deletion | function f() onlyOwner → function f() | Y | Y | | MOI | Modifier Insertion | function f() → function f() onlyOwner | N | Y | | OMD | Overridden Modifier Deletion | modifier m() override {} → | Y | N | | PKD | Payable Keyword Deletion | function f() payable → function f() | Y | N | | RSD | Return Statement Deletion | return amount; → //return amount; | Y | N | | RVS | Return Values Swap | return (1, "msg", 100); → return (100, "msg", 1); | Y | Y | | SCD | Selfdestruct Call Deletion | selfdestruct(); → //selfdestruct(); | Y | N | | SFR | SafeMath Function Replacement | SafeMath.add → SafeMath.sub | Y | Y | | SCEC | Switch Call Expression Casting | Contract c = Contract(0x86C9...); → Contract c = Contract(0x67ED...); | Y | N | | TOR | Transaction Origin Replacement | msg.sender → tx.origin | Y | N | | VUR | Variable Unit Replacement | wei → ether minutes → hours | Y | Y | | VVR | Variable Visibility Replacement | uint private data; → uint public data; | N | Y |

Minimal Mutation Rules

Some mutation operators foresee a minimal version:

• The extended operators generate a more comprehensive set of mutants. These guarantee a more in-depth test adequacy assessment, but they can generate more than one replacement per target (e.g., + is mutated in both - and *), which can lead to longer execution times.
• The minimal operators define simplified rules that only inject one replacement per target (e.g., + is mutated in -), limiting the generation of subsumed mutants and speeding up the testing process.

By default, SuMo employs the extended operators. However, you can enable the minimal rules in the sumo-config.js file.