Skip to content

Research paper On The Termination of Borrow Checking for Rust and a web application, CLI application and VSCode extension for running static analysis of rust-based smart contracts with a ready-to-be-verified project example.

License

Apache-2.0, MIT licenses found

Licenses found

Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT
Notifications You must be signed in to change notification settings

LedgerProject/safepkt

Repository files navigation

SafePKT

This project is implemented in the context of the European NGI LEDGER program.

This prototype aims at bringing more automation
to the field of software verification tools targeting rust-based smart contracts.

See SafePKT description

Table of contents

Demo

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.

Preview

As of today, SafePKT offers an opportunity for

Such program must be minimalist as we're in a prototyping phase i.e.
it should consist in a single-file program (lib.rs) without dependencies
other than rvt verification-annotations,
as there are some concerns remaining to be covered like:

  • the security aspects coming along with the compilation and execution of arbitrary source code
  • the compatibility of such programs with the underlying verification tools
  • the compatibility of KLEE, the symbolic execution engine with such programs dependencies
  • the compatibility of KLEE with the latest LLVM intrinsics, which could be leveraged for compiling such programs

Some screenshots of the successive steps execution can be found

Learn more about the latest version of the minimal viable product

Install

In a nutshell, the installation steps consist in

  • Cloning this repository and its submodules
git clone --recursive github.com:LedgerProject/safepkt
cd safepkt
  • Installing the requirements
  • Installing the project dependencies

Provided the following requirements are already available:

  • git,
  • docker,
  • rust (with cargo) and
  • node.js (with npm) you should be able to install the project by running the next command
make install

Contribute

In order to be able to contribute to the project, you might need to follow the installation steps
after having considered opening an issue to start a discussion
regards contributions to the project.

Running the project in a local environment is described by the development section.

In the best-case scenario, a local environment can be built by running

make contribution

Acknowledgment

We're very grateful towards all members of the NGI-Ledger Consortium for accompanying us
Blumorpho Dyne
FundingBox NGI LEDGER
European Commission

License

This project is distributed under either the MIT license or the Apache License.

About

Research paper On The Termination of Borrow Checking for Rust and a web application, CLI application and VSCode extension for running static analysis of rust-based smart contracts with a ready-to-be-verified project example.

Topics

Resources

License

Apache-2.0, MIT licenses found

Licenses found

Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT

Stars

Watchers

Forks

Packages

No packages published