#back-end #static-analysis #verification #automation #programs #component #prototype

bin+lib safepkt-backend

A backend to run static analysis tools against rust-based programs

10 releases (1 stable)

1.0.0 Nov 24, 2021
0.2.15 Nov 22, 2021
0.2.2 Oct 20, 2021
0.1.0 Aug 30, 2021

#729 in Filesystem

MIT/Apache

150KB
2.5K SLoC

Rust 2K SLoC // 0.0% comments Shell 454 SLoC // 0.0% comments Bitbake 33 SLoC

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

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

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.

Dependencies

~24–38MB
~604K SLoC