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

Development
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 cp .env{.dist,}

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,

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

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