SafePKT, a toolbox to verify rust-based smart contracts

safe PKT-01

In the SafePKT project, funded by the 3rd round of the NGI LEDGER program, our team focused on improving software development efficiency (and therefore time to market) for software used within the PKT ecosystem (e.g. PacketCrypt / CJDNS).

As security breaches in cryptocurrency software often lead to irrecoverable loss, such projects have higher than normal security requirements. However in this innovative and competitive space, time to market is also a critical to a project’s overall success.

With the help of cutting edge research in the academic space, we are developing improved software verification tools which will be easier to use and more helpful to developers who will apply them to improving software development efficiency and security in projects within the PKT ecosystem.

The technology

Software architecture

SafePKT technology consists of

Each frontend paired with the verification backend provide a software developer with reports about potential bugs or security issues in their code. Each pair offers reports containing verification results compiled by the backend by executing a test suite.

Such a test suite can be written by following the exact same steps one would follow, in order to test a rust-based smart-contract written on top of Parity’s ink! eDSL.

While the backend is responsible for handling all the transformation logic from a program source file or a rust library-oriented or binary-oriented project, one of the available frontends (single-page application, one of the two command-line implementations or the VS Code plugin) is responsible for enabling developers and researchers to triggers the verification process before receiving reports usually made available and formatted for command-line shells.

Verification process

In the same vein as for the frontend component, the command-line binary emitted at compilation of the backend, provides with the capability to verify a rust program when the constraints needed by the verifier are checked on a per instruction basis. Such verification process consists in running successively containerized jobs consisting in the following steps:

Eventually, we’ve decided to abandon the first approach since smart contract testing appears to be more library-oriented than dependant on some binary emitted at some point.

Changelog

In order to better understand how we ended up with today’s software architecture, here is a changelog of all the successive implementations, including failed attempts at levaraging Web Assembly as intermediate representation format to verify rust-based smart contracts.

Phase 1 – Web-based application implementation

In the initial phase, our web-based prototype clearly revealed some limitations in terms of usability and ergonomy. There were too many steps involved (three of them, which had to be taken in a specific and tedious order). However working with a web application also allowed us to better modularize and encapsulate the logic behind the verification process. It turned out that three distinct steps were enough to close a verification job for a trivial program (a multiplication of two 32-bits unsigned integers).

This basic arithmetic example taken from the RVT project let us discover the primitives of klee functions implemented by RVT maintainers for rust programs to be verified. It also prevented us from wandering off in too many directions associated with the complexity of the tools involved (LLVM and KLEE, being both two important pieces of complex technologies required by this project, which saved us tremendous amount of time and headaches thanks to the incredible work and deep documentation efforts provided by the RVT project authors).

Phase 2 – Scope reduction and simplification

Based on what we have learnt in Phase 1, we’ve realized from the feedback we’ve received (especially thanks to Dyne’s, while accompanying us all along the way) that

All these concerns led us to making the following decisions

From 3 steps at the beginning of the project, we simplified the verification process down to 1 step at the end by combining all of them from the backend component and optimizing intermediate operations like project dependencies download and caching

As a consequence, the HTTP API exposed by the backend inherited two additional steps (program verification and source restoration), whereas all previous routes except the one listing the available steps have been deprecated:

Additional routes have been added to the backend to facilitate project analysis management:

SafePKT Command-Line Interface

Optimizing the construction of the RVT-based toolset itself was a subtask described in this public issue. No official Docker image could be attached to project-oak/rvt project but we eventually managed to publish our own set of images and tags to ease the backend component set up from the official Docker registry, with the latest tag being worth of about 2Gb of compressed image layers available from https://hub.docker.com/repository/docker/safepkt/rvt

In the end, here is a screenshot showing some of the differences between the first iteration result and the latest UI release:

Transition between Phase 1 and Phase 2

Failed attempts and additional learning with Web Assembly as intermediate representation

We have also put some efforts to convert a smart contract rust source into web assembly,
right before returning to plain C code by relying on the WebAssembly Binary Toolkit (wabt).

However we had to quickly acknowledge such approach would be a dead-end for our particular use case,
as the amount of C code generated from wasm, for instance for some contracts like

At some point, either we ended up with

Most of the experiments, which has led us to this conclusion, can be found or replayed as targets of a Makefile,
available in our contribution clone of the substrate-nft project,
which is based on ink! eDSL to write smart contracts,
depending on the paritytech substrate platform.

Phase 3 – VS Code Extension implementation

Since the CLI application was working fine by the time when our second internal deadline has been hit, we have decided to follow up with the VS Code extension implementation, that has been anticipated to be deployed if we were to be on schedule with regards the previous critical steps (the verification of smart contracts itself and the report presentation to fellow users, developers and researchers).

As SafePKT verifier has been designed and implemented since the beginning as a set of loosely coupled components, it was fairly easy (all things considered AND after having cleared up how to best rely on rust verification tools) for us

SafePKT Verifier VS Code Extension

Dependencies

In a nutshell, all SafePKT software implementations and research results can be found in a single repository, including git submodules. Its main documentation entrypoint points to

Learning and limitations

The mixed approach based on both test fuzzing and symbolic execution as recommended by Rust Verifications Tools lead maintainers (Alastair Reid and Shaked Flur) in their last Retrospective blogpost clearly shows a way that would be both practical and not leading us too far away from being theoretically correct, while trying to prove that an implementation mirrors adequately specifications.

Therefore, it is of the utmost importance here to insist on the relative level of correctness one can only ensure, provided the distance between the program being verified and the actual target resulting from rustlang compiler emitting LLVM intermediate representation being submitted to verification with KLEE symbolic execution engine based in any case on hand-written assertions and assumptions to be specified upfront.

Besides, while testing smart contract examples provided by ink! eDSL project,
we could not help noticing that without narrowing enough the range of symbolic values declared with the rust-equivalent method of klee_assume function inherited from the verification-annotations library applied to values of i32 type for instance, the verification process would never stop in a reasonable amount of time, which proves to be not very practical in a day-to-day use of such verification process.

What’s next?

Even though we’ve reached the conclusion that a working solution in the context of rust-based smart contract verification consists in relying on KLEE via the Rust Verification Tools containerized so that a REST API for code instrumentation could be exposed for enabling developers or researchers to discover bugs otherwise difficult to detect (which happened to be true for instance with this buggy smart contract), we’ve also realized that complementary steps would definitely involve fuzz testing and most likely code generation which could reasonaby depend on the powerful Rust macros system for deriving assumptions and assertions from the underlying types of values under tests themselves in the same vein of what has been done with the propverify library, which itself took its inspiration from the proptest library (based on property testing).

Team

Thank you to all contributors

We’re very grateful towards the following organizations, projects and people:

Blumorpho - Dyne.org - FundingBox - NGI LEDGER - European Commission

Source: https://hackmd.io/@ZZ1Hc_T7RKanFpmdTouHSg/safepkt-toolbox-rust-based-smart-contracts-verification

Go back to Blog  

Read more