SafePKT, a toolbox to verify rust-based smart contracts

# SafePKT, a toolbox to verify rust-based smart contracts In the [SafePKT](https://ledgerproject.github.io/home/#/teams/SafePKT) project, funded by the 3rd round of the [NGI LEDGER program](https://www.ngi.eu/ngi-projects/ledger/), our team focused on improving software development efficiency (and therefore time to market) for software used within the PKT ecosystem (e.g. [PacketCrypt](https://github.com/cjdelisle/packetcrypt_rs) / [CJDNS](https://github.com/CJDNS-Development-Team/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 - a verification backend and - a variety of frontends such as - two distinct command-line (CLI) implementations, - a web application - a VS Code plugin 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](https://github.com/paritytech/ink/tree/v2.1.0). 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`](https://safepkt.cjdns.fr/), one of the two [`command-line implementations`](https://github.com/LedgerProject/safepkt_cli) or the [`VS Code plugin`](https://marketplace.visualstudio.com/items?itemName=CJDNS.safepkt-verifier)) 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: - *Scaffolding of a new rust project* uniquely identified from a rust program source file - *Generation of LLVM bitcode* from the newly created project - *Symbolic execution of the program* based on two strategies successively adopted - ~~the declaration of assumed input values types before having the program intermediate representation (obtained from the previous step) run by KLEE symbolic execution engine~~ - the addition of tests also run by KLEE for library-oriented project (what we've eventually decided we would be focusing on) 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](https://developer.mozilla.org/en-US/docs/WebAssembly) as intermediate representation format to verify rust-based smart contracts. ### Phase 1 - Web-based application implementation - Implementation of backend application skeleton, responding to HTTP requests matching the following routes: - POST `/source` to upload program source code (rust-based program for compiling a binary) - GET `/steps` to list verifications steps - POST `/llvm-bitcode-generation/{{ project_id }}` to run LLVM bitcode generation from a previously uploaded source - GET `/llvm-bitcode-generation/{{ project_id }}/report` to get a report for some LLVM bitcode generation - GET `/llvm-bitcode-generation/{{ project_id }}/progress` to get the completion status for some LLVM bitcode generation - POST `/symbolic-execution/{ project_id }` to run KLEE symbolic execution from a previously uploaded program after having generated intermediate representation with LLVM - GET `/symbolic-execution/{{ project_id }}/report` to get a report for some symbolic execution - GET `/symbolic-execution/{{ project_id }}/progress` to get the completion status for some symbolic execution - Implementation of a frontend application enabling a developer or a researcher to chain commands required to verify a program written in Rust by using the [Rust Verification Tools](https://github.com/project-oak/rust-verification-tools) from the comfort of a web browser. 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](https://github.com/project-oak/rust-verification-tools/blob/b179e90daa9ec77c2a81b903ff832aaca4f87b5b/demos/simple/klee/src/main.rs) 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](https://llvm.org/) and [KLEE](http://klee.github.io/), 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](https://github.com/project-oak/rust-verification-tools/graphs/contributors)). ### 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](https://www.dyne.org/)'s, while accompanying us all along the way) that - there were two many steps involved in the verification process - the web-based UI was costly for large programs (without further optimization of the editor) - the verification process was quite fragile since it depended on intermediate representation obtained from a rust program with LLVM linker and bitcode generation - the most recent programs would not be well supported as the KLEE version we could rely upon was not compiled against the most up-to-date version of LLVM (available for `rustc` compiler available out there). As a result the rust compiler version, we used to leverage Rust Verification Tools would not be most of the time compatible with the targeted programs, which were in essence alway quite edgy given the rapid pace of evolution in the field of blockchain smart contract implementation. All these concerns led us to making the following decisions - 🎯 To reduce the number of steps down to the very strict minimum 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 - 🎯 To part away from the web interface by considering the implementation of command-line interface (CLI). The web app was great for prototyping and collecting feedback without having to install the whole suite of tools, which would take at best 20 min to set up. However and as it was stated before, large programs made the UI sluggish and would have required further optimization, new libraries selection. 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: - POST `/program-verification/{ project_id }` to run a smart contract verification - GET `/program-verification/{{ project_id }}/report` to get a report for some program verification - GET `/program-verification/{{ project_id }}/progress` to get the completion status of a verification - POST `/source-restoration/{ project_id }` to restore a previously uploaded source - GET `/source-restoration/{{ project_id }}/report` to get a report for some source restoration - GET `/source-restoration/{{ project_id }}/progress` to get the completion status of a source restoration Additional routes have been added to the backend to facilitate project analysis management: - `POST` `/uploaded_sources_listing/{project_id}` to run a container executing `ls` from the directory where uploaded sources are - `GET` `/uploaded_sources_listing/{project_id}/report` to get the logs of the container which output contains all the uploaded sources id (`project_id`) - `DELETE` `/program-verification/{project_id}` to stop container executing the verification process for a previously uploaded source under project id passed as parameter ![SafePKT Command-Line Interface](https://i.imgur.com/oySu9bY.png) Optimizing the construction of the RVT-based toolset itself was a subtask described in this [public issue](https://github.com/project-oak/rust-verification-tools/pull/149). 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](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: - A more significant program (real-world case based on `ink!`) against a trivial multiplication example - The reduction of steps down to a single-step program verification (responsible for source upload, with LLVM bitcode generation and symbolic execution with KLEE being abstracted away by the backend). ![Transition between Phase 1 and Phase 2](https://i.imgur.com/ifiyeD0.png) #### 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)](https://github.com/WebAssembly/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 - a [simple NFT implementation](https://github.com/polk4-net/substrate-nft) or - by relying on a [Hyperledger Sawtooth SDK](https://github.com/hyperledger/sawtooth-sdk-rust) implementation in rust. At some point, either we ended up with - too much code to be analyzed with klee (symbolic execution engine running under the wood) or - too many failures hard to debug because of the numerous dependencies for the sdk we've tried to analyze. 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](https://github.com/thierrymarianne/contrib-substrate-nft/blob/main/nft/Makefile) project, which is based on [ink! eDSL](https://github.com/paritytech/ink) to write smart contracts, depending on the paritytech [substrate platform](https://github.com/paritytech/substrate). ### 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 - to reduce the [number of steps](https://github.com/LedgerProject/safepkt_backend/blob/a6d757c20958df480e97805f9f7e5f0d879fe243/src/infrastructure/verification.rs#L14-L16) for the overall verification process (from the backend or/and the frontend by considering deployment for both components or one of them only) - to add new steps to the verification pipeline matching a new route of the HTTP API exposed by backend - to remove deprecated steps once everything was working as expected from the frontend - to introduce the SafePKT CLI command communicating internally with the backend API. The [SafePKT library](https://github.com/LedgerProject/safepkt_backend/blob/a6d757c20958df480e97805f9f7e5f0d879fe243/src/lib.rs) is consumed by two separate entrypoints: - the [CLI entrypoint](https://github.com/LedgerProject/safepkt_backend/blob/a6d757c20958df480e97805f9f7e5f0d879fe243/src/cli.rs) - the [HTTP entrypoint](https://github.com/LedgerProject/safepkt_backend/blob/a6d757c20958df480e97805f9f7e5f0d879fe243/src/http.rs) serving responses one can expect for each of the compliant HTTP requests - to port the [logic implemented](https://github.com/LedgerProject/safepkt_frontend/blob/f41c1a91c838355ed7c66379abee96dee91db95e/mixins/step/program-verification.ts#L73-L82) from the frontend when reaching out to the API exposed by the backend to a [VS Code extension](https://github.com/LedgerProject/safepkt_vscode-plugin/blob/e64a47ff5f0d3e76236565e7d0db51a31bed7a79/src/verifier.ts#L101-L143) ![SafePKT Verifier VS Code Extension](https://i.imgur.com/QVdTlFQ.png) ### Dependencies In a nutshell, all SafePKT software implementations and research results can be found in [a single repository, including git submodules](https://github.com/LedgerProject/safepkt). Its [main documentation entrypoint](https://github.com/LedgerProject/safepkt/tree/f98c106d24f3e13b098eb1afe54bf67416dbbe3e#readme) points to - [a Single-page application](https://github.com/LedgerProject/safepkt_frontend): - [Node.js](https://nodejs.org/), - [Typescript](https://www.typescriptlang.org/), - [Vue.js](https://vuejs.org/), - [NuxtJs](https://nuxtjs.org/) - [a Server-side back-end and a rust command-line application](https://github.com/LedgerProject/safepkt_backend/releases): - [Rust](https://www.rust-lang.org/), - [Docker engine](https://www.docker.com/products/container-runtime), - [Rust Verification Tools](https://project-oak.github.io/rust-verification-tools/), - [SafePKT RVT's fork](https://github.com/LedgerProject/safepkt_rust-verification-tools) - [SafePKT verification container image](https://hub.docker.com/r/safepkt/rvt/tags) - [LLVM](https://llvm.org/), - [KLEE](http://klee.github.io/) - [an additional command-line application](https://github.com/LedgerProject/safepkt_cli) - [Node.js](https://nodejs.org/) - [a VS Code extension](https://marketplace.visualstudio.com/items?itemName=CJDNS.safepkt-verifier): - [Got](https://github.com/sindresorhus/got/tree/v11.8.2), - [Tree-sitter](https://tree-sitter.github.io/tree-sitter/), - [Typescript](https://www.typescriptlang.org/), - [VS Code Extension API](https://code.visualstudio.com/api) - [a ready-for-verification smart-contract project example](https://github.com/LedgerProject/safepkt_smart-contract-example) - [a research paper "On the Termination of Borrow Checking for Rust"](https://github.com/LedgerProject/safepkt_paper) ## Learning and limitations The mixed approach based on both test fuzzing and symbolic execution as recommended by [Rust Verifications Tools](https://project-oak.github.io/rust-verification-tools) lead maintainers (Alastair Reid and Shaked Flur) in their last [*Retrospective*](https://project-oak.github.io/rust-verification-tools/2021/09/01/retrospective.html) 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](http://klee.github.io/) based in any case on hand-written [assertions](https://github.com/LedgerProject/safepkt_smart-contract-example/blob/buggy-smart-contract/src/lib.rs#L175-L177) and [assumptions](https://github.com/LedgerProject/safepkt_smart-contract-example/blob/buggy-smart-contract/src/lib.rs#L174) to be specified upfront. Besides, while testing smart contract examples provided by [`ink! eDSL` project](https://github.com/paritytech/ink/tree/v2.1.0/examples/), we could not help noticing that without narrowing enough the range of symbolic values declared with the [rust-equivalent method of `klee_assume`](https://github.com/LedgerProject/safepkt_assert/blob/main/src/lib.rs#L7) function inherited from the [`verification-annotations` library](https://github.com/project-oak/rust-verification-tools/blob/main/verification-annotations/src/verifier/klee.rs#L138-L140) applied to values of [`i32` type](https://doc.rust-lang.org/std/primitive.i32.html) 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](http://klee.github.io/) via [the Rust Verification Tools](https://github.com/LedgerProject/safepkt_rust-verification-tools) [containerized](https://hub.docker.com/r/safepkt/rvt/tags) so that a [REST API for code instrumentation](https://github.com/LedgerProject/safepkt_backend) 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](https://github.com/LedgerProject/safepkt_smart-contract-example/tree/buggy-smart-contract)), we've also realized that complementary steps would definitely involve [fuzz testing](https://en.wikipedia.org/wiki/Fuzzing) 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](https://github.com/project-oak/rust-verification-tools/tree/b179e90daa9ec77c2a81b903ff832aaca4f87b5b/propverify), which itself took its inspiration from the [proptest](https://altsysrq.github.io/proptest-book/intro.html) library (based on [`property testing`](https://en.wikipedia.org/wiki/Property_testing)). ## Team - [Caleb James de Lisle](https://github.com/cjdelisle) - [Thierry Marianne](https://github.com/thierrymarianne) - [Étienne Payet](https://github.com/etiennepayet) - [David Pearce](https://github.com/DavePearce) - [Fausto Spoto](https://github.com/spoto) ## Thank you to all contributors We're very grateful towards the following organizations, projects and people: - the Project Oak maintainers for making [Rust Verifications Tools](https://project-oak.github.io/rust-verification-tools/), a dual-licensed open-source project (MIT / Apache). The [RVT tools allowed us](https://github.com/project-oak/rust-verification-tools/issues/150) to integrate with industrial grade verification tools in a very effective way. - the [KLEE Symbolic Execution Engine](http://klee.github.io/) maintainers - the [Rust community](https://www.rust-lang.org/community) at large - the JavaScript and [NuxtJS community](https://nuxtjs.org/teams) at large - The [University of Reunion Island](https://www.univ-reunion.fr/university-of-reunion-island/research) and the [University of Verona](https://www.di.univr.it/?lang=en) and especially - All members of the NGI-Ledger program for accompanying us - [Blumorpho](https://www.blumorpho.com/) - [Dyne](https://www.dyne.org/ledger/) - [FundingBox](https://fundingbox.com/) - [NGI LEDGER](https://ledgerproject.eu/) - [European Commission](https://ec.europa.eu/programmes/horizon2020/en/home) ![Blumorpho - Dyne.org - FundingBox - NGI LEDGER - European Commission](https://i.imgur.com/WbI9f37.png)