Our exploration of mutation testing with Move offers a glimpse into how we can bolster the robustness of smart contract specifications, increasing overall assurance for developers working on the Aptos blockchain.

Introduction

Move Prover, an indispensable tool for Move developers, allows smart contracts written in Move to be formally verified against user specifications. Such formal verification is essential in asserting the correctness and security of contracts, an important tool next to the conventional assurance methods like fuzzing and static analysis.

However, the effectiveness of the Move Prover hinges on the quality of the specifications provided. Weak or incomplete specifications can lead to a false sense of security. To address this, we at Eiger developed two key tools, move-mutator and move-spec-test, available in their beta-release, to help developers identify and eliminate potential weak spots in their code's specifications.

Mutation Testing: A Quick Background

Mutation testing introduces deliberate errors (mutations) to source code to test the quality of existing tests. It's a robust method to identify blind spots that traditional coverage tools might miss. For instance, consider the following Move code snippet:

‍

public fun inc_and_check(x: &mut u64): bool {
   *x = *x + 1;
   x > 42
}‍
 
#[test]
fun test_it() { 
   let x = 3; 
   inc_and_check(&x); 
   assert!(x == 4, 0);
}

‍

Despite achieving full code coverage, the test suite for inc_and_check lacks checks for some function behaviors, illustrating the potential blind spots in testing. Mutation testing, by introducing changes such as replacing x > 42 with x < 42, helps verify if the tests can detect these changes. If a mutation passes the existing tests (i.e., the mutant survives), it indicates the tests could be improved.

Application to Specification Testing

The move-spec-test tool uses mutation testing principles to evaluate the completeness of Move specifications. We can identify whether the specifications are comprehensive enough by applying the move-mutator to introduce changes in the Move code and running these mutants against the unchanged specifications with the Move Prover.

For example, during testing our tool, we analyzed the specifications of the Diem Payment Network. The survival of several mutants highlighted gaps in the specifications, which were confirmed by proof engineers.

Consider a simplified Move function:

‍

fun div(x: u128, y: u128): u128 { 
   assert!(y != 0, 42); 
   x / y
}

‍

And its specification:

spec div { 
   aborts_if y == 0 with 42;
}

‍

A mutant where the division operation (/) is replaced with modulo (%) survives the specification verification because the specification does not consider the operation's outcome, only its abort condition. This illustrates a blind spot in the specification, which, when improved, can significantly enhance the assurance provided by formal verification.

Developed by Eiger, with support from engineers at Aptos Labs, these tools are set to revolutionize how developers approach smart contract security and reliability. Check out the tools on GitHub and share your feedback to help us refine and enhance their capabilities.

Who is Aptos?

Aptos is a prominent blockchain platform known for prioritizing security, scalability, and usability. It leverages the Move programming language to foster a robust environment for developing decentralized applications. Aptos' commitment to high-performance blockchain solutions makes it an ideal testbed for advanced tools like the Move Prover, enhancing the reliability of blockchain transactions and smart contract functionality.