SafePKT

This project is implemented in the context of the European NGI LEDGER program.

This prototype aims at bringing more automation
to the field of software verification tools targeting rust-based smart contracts.

See SafePKT description

Table of contents

• Preview
• Learn more about the latest minimal viable product
• Install
• Contribute
• Acknowledgement
• License

Demo

An online demo of a rust-based smart contract verification is available from

• https://safepkt.cjdns.fr

Rust-based smart contract analysis and verification is also available to developers and researchers by installing VS Code and SafePKT Verifier extension from VS Code Marketplace.

• https://marketplace.visualstudio.com/items?itemName=CJDNS.safepkt-verifier

Preview

As of today, SafePKT offers an opportunity for

• generating LLVM bitcode from a rust binary program,
• running KLEE symbolic engine from the output
• verifying rust-based smart contracts implemented on top of ink! framework
• fuzzing programs, which tests would have been enriched by following propverify conventions

Such program must be minimalist as we're in a prototyping phase i.e.
it should consist in a single-file program (lib.rs) without dependencies
other than rvt verification-annotations,
as there are some concerns remaining to be covered like:

• the security aspects coming along with the compilation and execution of arbitrary source code
• the compatibility of such programs with the underlying verification tools
• the compatibility of KLEE, the symbolic execution engine with such programs dependencies
• the compatibility of KLEE with the latest LLVM intrinsics, which could be leveraged for compiling such programs

Some screenshots of the successive steps execution can be found

• in the web frontend preview section,
• in the CLI preview section or
• in the VSCode preview section

Learn more about the latest version of the minimal viable product

• Latest MVP for Smart-Contract verification with SafePKT

Install

In a nutshell, the installation steps consist in

• Cloning this repository and its submodules

git clone --recursive github.com:LedgerProject/safepkt
cd safepkt

• Installing the requirements
• Installing the project dependencies

Provided the following requirements are already available:

• git,
• docker,
• rust (with cargo) and
• node.js (with npm) you should be able to install the project by running the next command

make install

Contribute

In order to be able to contribute to the project, you might need to follow the installation steps
after having considered opening an issue to start a discussion
regards contributions to the project.

Running the project in a local environment is described by the development section.

In the best-case scenario, a local environment can be built by running

make contribution

Acknowledgment

We're very grateful towards all members of the NGI-Ledger Consortium for accompanying us

License

This project is distributed under either the MIT license or the Apache License.