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.

make help

Install cargo with rustup

Download rustup and install Rust dependencies per official instructions

make install-deps

Configuration

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

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

make build

Build a new release

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

make release

Documentation

Generate the documentation.

make docs

Run tests

make test

Run program verification in CLI (command-line interface)

# Plain Multisig Wallet
# See https://github.com/LedgerProject/safepkt_backend/blob/main/examples/multisig_plain.rs
./target/release/safepkt-cli verify_program --source ./examples/multisig_plain.rs

# erc721
# See https://github.com/LedgerProject/safepkt_backend/blob/main/examples/erc721.rs
./target/release/safepkt-cli verify_program --source ./examples/erc721.rs

# erc20-based smart contract showcasing a bug,
# which can be highlighted by running SafePKT CLI verifier
# See https://github.com/LedgerProject/safepkt_backend/blob/main/examples/buggy-erc20.rs
./target/release/safepkt-cli verify_program --source ./examples/buggy-erc20.rs

Run program fuzzing in CLI (command-line interface)

# erc721
# See https://github.com/LedgerProject/safepkt_backend/blob/main/examples/erc721.rs
./target/release/safepkt-cli verify_program --source ./examples/erc721.rs --fuzz

Web deployment

Run the backend

./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.