SafePKT backend

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

This component is the backend of a prototype aiming at bringing more automation
to the field of software verification tools targeting rust-based programs.

See SafePKT description

Table of contents

• Development
  • Help
  • Install cargo with rustup
  • Configuration
  • Build the project
  • Build a new release
  • Documentation
  • Run tests
  • Run program verification in CLI (command-line interface)
  • Run program fuzzing in CLI (command-line interface)
• Web deployment
  • Run the backend
  • Use nginx as reverse-proxy
• Acknowledgment
• License

Development

Help

List all the Makefile targets.

shell make help

Install cargo with rustup

Download rustup and install Rust dependencies per official instructions

shell make install-deps

Configuration

Copy the configuration file template and update its entries per your need.

shell make copy-configuration-file

• HOST - the host where the backend will be available from,
• PORT - the port which the backend will be listening on,
• SOURCE_DIRECTORY - the directory where the backend will upload source codes to,
• RVT_DIRECTORY - the directory where the rust verifications tools have been cloned,
• RVT_DOCKER_IMAGE - the name of a container image pulled from a registry or built manually,
• VERIFICATION_SCRIPT - Path to shell verification script
• UID_GID - uid and gid of system user running commands in container

Build the project

shell make build

Build a new release

Compile a binary and copy it to ./target/release/safepkt-backend.

shell make release

Documentation

Generate the documentation.

shell make docs

Run tests

shell make test

Run program verification in CLI (command-line interface)

```shell

Plain Multisig Wallet

See https://github.com/paritytech/ink/tree/v2.1.0/examples/multisig_plain

./target/release/safepkt-cli verifyprogram --source ./examples/multisigplain.rs

erc721

See https://github.com/paritytech/ink/tree/v2.1.0/examples/erc721

./target/release/safepkt-cli verify_program --source ./examples/erc721.rs ```

Run program fuzzing in CLI (command-line interface)

```shell

erc721

See https://github.com/paritytech/ink/tree/v2.1.0/examples/erc721

./target/release/safepkt-cli verify_program --source ./examples/erc721.rs --fuzz ```

Web deployment

Run the backend

shell ./target/release/safepkt-backend

Run nginx as reverse-proxy

Configuration templates for nginx are available from provisioning/web-server/nginx. Configuration files for running the backend with docker and docker-compose are available from - provisioning/web-server/docker-compose.yml - provisioning/web-server/docker-compose.override.yml.dist
allowing to declare - paths to TLS certificates, - docker network - basic authentication (as arbitrary source files can be uploaded and compiled)

Acknowledgment

We're very grateful towards the following organizations, projects and people: - the Project Oak maintainers for making Rust Verifications Tools, a dual-licensed open-source project (MIT / Apache).
The RVT tools allowed us to integrate with industrial-grade verification tools in a very effective way. - the KLEE Symbolic Execution Engine maintainers - the Rust community at large - All members of the NGI-Ledger Consortium for accompanying us

License

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