Check out the SafePKT official website: https://safepkt.cjdns.fr/
SafePKT is a project to study and build static analysis technology for the Rust code used in the PKT project. PKT is a project for disintermediating telecom monopolies by de-coupling the roles of infrastructure operation from (internet) service provision. PKT uses a blockchain based on the bitcoin protocol and a proof of work algorithm called PacketCrypt which requires bandwidth in order to mine. The vision of PacketCrypt is to drive investment into network infrastructure by creating artificial demand for bandwidth.
You can find out more about the overall PKT project by going to: https://pkt.cash/
In the SafePKT project we are focused on improving software development efficiency (and therefore time to market) for software used within the PKT ecosystem (e.g. PacketCrypt / cjdns). As security breaches in cryptocurrency software often lead to irrecoverable loss, such projects have higher than normal security requirements. However in this innovative and competitive space, time to market is also a critical to a project's overall success. With the help of cutting edge research in the academic space, we are developing improved software verification tools which will be easier to use and more helpful to developers who will apply them to improving software development efficiency and security in projects within the PKT ecosystem.
The technology of PKT overall includes PacketCrypt bandwidth-hard proof of work, Lightning Network, and cjdns networking protocol.
SafePKT technology consists of a web based frontend and server-side backend, which work together to provide a software developer with reports about potential bugs or security issues in their code.
Both a command-line (CLI) application and a Visual Studio Code plugin offer independently from the two previous components,
reports containing the same level of detail offered by the backend when it comes to
analyzing a rust-based smart-contract written on top of Parity's ink! eDSL - see https://github.com/paritytech/ink/tree/v2.1.0.
SafePKT depends on the following technologies:
- Single-page application:
- Server-side back-end and rust command-line application:
- Node.js command-line application:
- SafePKT assertion library:
- Rust,
- VS Code extension:
SafePKT consists of three separate components:
- a backend leveraging
- the Rust Verification Tools,
- the KLEE Symbolic Execution Engine,
- the Docker Engine.
This backend offers capabilities to verify program written in Rust,
by emitting LLVM bitcode, consumed by KLEE Symbolic Execution Engine.
Besides it provides developers and researchers with two separate execution modes: - HTTP verification with a REST API,
- CLI (Command-Line Interface) verification.
- a frontend based on NuxtJS,
- a secondary CLI (command-line application) based on Node.js,
- an assertion library based on rvt verification annotations library,
- a ready-for-verification smart contract project example,
based on one of ink! eDSL examples: a Plain Multisig Wallet, - an extension for Visual Studio Code,
- and at last but not least, a research paper "On the Termination of Borrow Checking for Rust" authored by
A fourth repository has been created to ease
- automation of compilation and publication (from GitHub) of the research paper
- installation of the project frontend, backend and CLI components and
- contribution to those components, along with maintenance of the VS Code extension
An online demo of a rust-based smart contract verification is available from
Rust-based smart contract analysis and verification is also available to developers and researchers by installing VS Code and SafePKT Verifier extension from VS Code Marketplace.