Verification Options for Substrate

[p5150j]

Security is hard to get right in blockchains. It's even harder to make sure that code is correct while still actively developing the product: code changes are frequent, requirements are changing, and the codebase is growing.

Explore options for verifying blockchain code, specifically for the Substrate blockchain framework to try to verify the code of the Interlay blockchain.

The tool should be integrated into the Rust toolchain (no DSLs)

Please see:
https://harz.dev/blog/rust-verification/

Timebox:
2 days.

[rlaferla]

https://www.youtube.com/watch?v=vMGilPbIotw

[rlaferla]

I tried using Mirai and found no project issues, just issues with the dependencies. However, I am skeptical of the results and filed an issue with the Mirai project for confirmation. facebookexperimental/MIRAI#1206

[rlaferla]

I also tried using the Prusti extension for VSCode but was not able to because it was expecting the x86_64 version of OpenJDK but my system is an Apple Silicon m2 (arm64). I filed an issue with the Prusti project. viperproject/prusti-dev#1399. I will try the CLI version now.

[rlaferla]

The Prusti cli generated only errors of type: [Prusti internal error] and [Prusti: unsupported feature]

[rlaferla]

Prusti https://github.com/viperproject/prusti-dev
Kani https://github.com/model-checking/kani
Mirai https://github.com/facebookexperimental/MIRAI

[rlaferla]

A new one that I found and attempted to use but also didn't work.

Miri https://github.com/rust-lang/miri

[rlaferla]

For Kani, I ran into the same issue as the blog article author: