SafePKT 后端

此项目是在欧洲 NGI LEDGER 项目 的背景下实现的。

此组件是一个原型的后端，旨在将更多自动化
引入针对基于 Rust 的程序软件验证工具领域。

见 SafePKT 描述

目录

• 开发
  • 帮助
  • 使用 rustup 安装 cargo
  • 配置
  • 构建项目
  • 构建新版本
  • 文档
  • 运行测试
  • 在 CLI（命令行界面）中运行程序验证
  • 在 CLI（命令行界面）中运行程序模糊测试
• Web 部署
  • 运行后端
  • 使用 nginx 作为反向代理
• 致谢
• 许可证

开发

帮助

列出所有 Makefile 目标。

make help

使用 rustup 安装 cargo

下载 rustup 并根据官方说明安装 Rust 依赖项 [官方说明]

make install-deps

配置

复制配置文件模板并按需更新其条目。

make copy-configuration-file

• HOST - 后端可从其获取的主机
• PORT - 后端将监听的端口
• SOURCE_DIRECTORY - 后端将上传源代码的目录
• RVT_DIRECTORY - 已克隆 rust 验证工具 的目录
• RVT_DOCKER_IMAGE - 从 仓库 或 手动构建 的容器镜像名称
• VERIFICATION_SCRIPT - shell 验证脚本路径
• UID_GID - 在容器中运行命令的系统用户的 uid 和 gid

构建项目

make build

构建新版本

编译二进制文件并将其复制到 ./target/release/safepkt-backend。

make release

文档

生成文档。

make docs

运行测试

make test

在 CLI（命令行界面）中运行程序验证

# 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

在 CLI（命令行界面）中运行程序模糊测试

# 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 部署

运行后端

./target/release/safepkt-backend

以反向代理模式运行nginx

nginx的配置模板可以从provisioning/web-server/nginx获取。使用docker和docker-compose运行后端的配置文件可以从以下位置获取：

• provisioning/web-server/docker-compose.yml
• provisioning/web-server/docker-compose.override.yml.dist
  允许声明
  • TLS证书的路径，
  • docker网络，
  • 基本认证（因为可以上传和编译任意源文件）

致谢

我们对以下组织、项目和人员表示衷心的感谢

• Project Oak的维护者，他们创建了Rust Verifications Tools，这是一个双许可的开源项目（MIT / Apache）。
  RVT工具使我们能够非常有效地与工业级验证工具集成。
• KLEE符号执行引擎的维护者
• 整个Rust社区
• 所有陪伴我们的NGI-Ledger联盟成员
  
  

许可证

本项目根据MIT许可证或Apache许可证进行分发。