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
150KB
2.5K
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.
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 scriptUID_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.
Dependencies
~24–38MB
~604K SLoC