Runtime Verification: Advanced Rust Property Test Verification for Polkadot Ecosystem

Proposal Overview

We envision this proposal as the first phase of a multi-phase roadmap which will take Polkadot to the next level, by bringing accessible Rust formal verification tools to the Polkadot ecosystem via symbolic property testing, to enable higher levels of community trust and outside investment. But let's take a step back.

What does all of that mean? In 2023, Runtime Verification Inc. (RV), in concert with the Web3 Foundation, started the development of KMIR, a Rust code analysis toolkit. In this proposal, we seek to add formal verification support to KMIR via symbolic property test execution. Why Rust? The Rust language is an essential pillar of the Polkadot ecosystem; it powers the runtime, the SDK, parachain development, smart contract frameworks, and more. The upshot of all of this is that billions of dollars worth of DOT are secured by these critical Rust code bases. Thus, we believe that the safety, stability, and reliability of Polkadot depends on the safety, stability, and reliability of its underlying Rust code base.

Why formal verification? Unlike standard software testing or manual auditing, which can only prove the presence of bugs, formal verification can prove the absence of bugs. Of course, nothing is for free. Formal verification techniques can take years to master. That's where symbolic property testing comes in. If a developer already has existing property tests, then no code changes are required to start enjoying the benefits of symbolic property testing. Instead, a developer need only re-execute their tests with a symbolic property test engine, which uses a symbolic execution test strategy to evaluate the function(s) under test across all possible inputs simultaneously. That means, if there is some input which can cause your test to fail, the tool will be able to find it. Furthermore, previous work at Amazon Web Services and Google Research confirms that symbolic property testing is accessible to the broader developer community.

Why Runtime Verification Inc.? Firstly, because we have already successfully applied these techniques to the EVM ecosystem via our open-source tool Kontrol; we know they work. Secondly, after our previous collaboration, W3F encouraged RV to apply to the Polkadot treasury to continue KMIR development. Finally, RV is well-positioned to undertake this proposal due to our expertise in both formal verification and blockchain systems. RV has completed dozens of blockchain audits both inside and outside of Polkadot and verified several blockchain consensus protocols. Our flagship product, the K Framework, is a language-generic software analysis toolkit that has successfully analyzed and verified software written in a variety of languages including Solidity/EVM, Wasm, Michelson, and more.

Problem statement

Software security, reliability, and correctness are ever-present issues in the software development world. These problems are further compounded by the massively distributed, permissionless nature of blockchain systems. Due to this, we are convinced that existing software testing and auditing processes are not sufficient; future secure software development at scale will require accessible formal verification techniques, which can verify that a given piece of code is correct in all possible scenarios. Unfortunately, classical formal verification tools, such as theorem provers and model checkers are often difficult to learn and to adopt into standard software development workflows.

Why difficult to learn? Often, they require the user to learn an entirely new specification language which is used in order to communicate with the tool.

Why difficult to adopt? Typically, these types of tools are limited in language feature support (e.g. no loops), so users cannot verify the properties of real-world programs. We believe that a symbolic property testing solution by RV can help alleviate both of these issues. As blockchain and language semantics experts, RV has the experience to build tools that work with codebases that programmers use. Using symbolic property testing techniques, a programmer is able to verify their code base is correct by just writing tests in the language they already use every day, without learning an entirely new specification language. To ensure that our tool is powerful enough to be useful, we will leverage the K Framework, RV's programming language verification toolkit. The K Framework includes several important features: (a) full symbolic execution support including unbounded loops; (b) a modular language to define trusted operational semantics of target languages (we have previously modelled C, EVM, Wasm, and more).

Executive Summary

The objective of this first-phase proposal is to create a symbolic property testing engine which can parse Rust property tests and execute any function(s) under test across all inputs simultaneously using a symbolic execution engine, possibly guided by user-provided lemmas/loop-invariants (with such lemmas/loop-invariants being specified in a tool-specific format). The upshot of all this is that developers can prove the absence of bugs for their program; that is, there does not exist a scenario under which the function(s) under test will fail.

This proposal will bring the power of formal verification to Rust developers across the Polkadot ecosystem including maintainers of the Polkadot Runtime (written in Rust), parachain developers using Substate (a Rust library), smart contract developers using Ink! (which desugars into Rust), and more. Of course, there is no free lunch. Symbolic execution engines for a programming language are challenging to develop and maintain: they require a deep understanding of both the target language and symbolic execution techniques.

Thankfully, we have the needed building blocks. KMIR is our in-house Rust language interpreter. RV's flagship product, the K Framework, contains a language-generic symbolic execution engine.

Said more concretely, our goal is to build a toolchain that:

converts Rust source code/property tests into a form suitable for KMIR
extends KMIR with the ability to execute these Rust property tests
utilizes the K Framework to verify the property tests symbolically.

Finally, our proposal includes provisions for (a) presenting our current results at Polkadot Decoded, to help generate buzz for the broader community; and (b) a small-scale, targeted tool experience workshop with key developers in order for us to conduct user experience surveys and smooth out rough edges.

We envision multiple potential follow-up proposals to further advance the tool's utility for the Polkadot community as well as later, more broadly focused tutorial workshops which will teach Polkadot developers how to integrate the tool into their development workflow. See the future proposals section below for more details.

Symbolic Property Test Workflow Overview (see picture below)

Symbolic Property test workflow overview https://ibb.co/vBSxZT9

Project Team Members

Engineering Team

Stephen Skeirik: Formal Verification Engineer

Stephen Skeirik's research interests include programming languages, formal logic, and program verification. His desire is to ground system design on practical logical foundations enabling formal verification to scale to real-world challenges. He obtained his Bachelor's degree in Computer Science from the University of Tennessee Knoxville and his Ph.D from the University of Illinois at Urbana-Champaign.

Daniel Cumming: Formal Verification Engineer

Daniel Cumming's interests are related to information flow security and automating the verification of programs. Daniel studied at The University of Queensland completing his Bachelor of Arts, and is completing his Masters of Information Technology. Between 2020 and 2022 he worked for The University of Queensland as a research and teaching assistant as a member of the Program Analysis Centre. He assisted in teaching formal methods, computer systems, and algorithms. Daniel worked on research projects related to specifying the ARM64 instruction set, invariant generation techniques, and automatic verification of EVM bytecode smart contracts with Vale. Daniel is passionate about digital music and digital music production.

Maria Kotsifakou: Formal Verification Engineer

Maria Kotsifakou is interested in programming languages, compilers and parallel programming. She received her B.Eng degree in Computer Engineering from National Technical University of Athens, and her MS and Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign. Her previous work has been mainly focused on compilers for heterogeneous architectures and developing formal semantics for various programming languages.

Project Management & Advisory team

Yale Vinson: Project Manager

Yale Vinson has spent over fifteen years working in the FinTech industry building digital financial services products. Ranging from SIM based payments to tokenized payments, digital gift cards, and peer to peer transactions, he has focused on delivering secure digital financial products that put the needs of consumers first. Most recently, Yale worked on products which enabled crypto for the masses at Diebold Nixdorf and MoneyGram. Yale has a B.S. and an M.S. in Electrical Engineering from Texas A&M University.

Everett Hildenbrandt Technical Advisor

Everett Hildenbrandt is a formal modeling engineer and CTO at RV. His interests include automated system analysis via symbolic model checking, rigorous software development via carefully designed development practices, and applying these techniques to the software used in the other sciences (eg. physics, biology). He strongly believes that programming languages and system description languages should not be put together in an ad-hoc manner, rather they should be carefully designed using state of the art language-building tools.

Gregory Makodzeba: Business Development Coordinator

Gregory brings a unique combination of technical education and business-related blockchain expertise. With prior education in Aviation Management from Georgian College and a Bachelor in Computer Science from the National Technical University of Ukraine ‘Kyiv Polytechnic Institute’, Gregory has built a robust foundation in both analytical and engineering disciplines. His entrepreneurial spirit is evidenced by his co-founding role at Rektoff, a community-driven cybersecurity R&D company specializing in Web3 security solutions, where he excelled in forging strategic partnerships and spearheading innovative security strategies. Beyond his business acumen, Gregory has actively contributed to the blockchain community as a mentor at ETHGlobal Waterloo and ETHToronto, guiding participants through the complexities of web3 development and security. At Runtime Verification, Gregory is leveraging his comprehensive background to enhance business strategy, client engagement and drive the adoption of secure, reliable decentralized applications.

Marketing team

Silvia Barredo: Marketing Manager

Silvia Barredo is the Marketing Manager at Runtime Verification. She is interested in growing online communities through the creation of learning resources. Prior to joining Runtime Verification, she worked at NEM Blockchain Malaysia as a Business Development and Events Manager. She has also worked with other Malaysian companies in the event and marketing field. She is also the event manager at Hello Decentralization, a conference that explores decentralized technologies from a technical perspective.

Project Milestones

Our milestones are divided into 4 categories: frontend (tool development and docs), backend (MIR engine development and verification), project management & advisory and socials (community event participation). For detailed milestones and project timeline breakdown — please see appendix of the full proposal: https://docs.google.com/document/d/1oPs1Nx34tyOsOxde-w70tZUxfn5_LSJr6vskX22kIV4/edit?usp=sharing

Timelines

Our expected timeline is 6 months (26 weeks) with 3 full-time engineers (FTEs), a project manager, a technical advisor and some help from an event/marketing coordinator. Note that, given the large time frame, we anticipate that at some point during the project, some engineers will need time off. We will assign backup personnel to avoid any impact on the overall schedule.

Timeline

Budget:

We are billing at the following rates:

Full-time employees: $20k/person-month
Part-time employees: $10k/person-month

For 3 full-time engineers, 1 part-time project manager, 1 part-time technical advisor and marketing/event coordinator, we are asking $526,000 or ~75,142 DOT (using the 7-day price average of $7).

Frontend Milestones

Rust to KMIR Bridge: $85,000
Property Test Compiler: $50,000
Concrete Property Test Executor: $40,000
Symbolic Property Test Executor: $50,000
User Guide, Documentation, and Tidying Up: $35,000

Backend Milestones

Property Test Collection: $15,000
MIR Interpreter Source Map: $17,500
Timeboxed MIR Interpreter Validation: $40,000
Simple Manual Property Test Verification: $20,000
Complex Property Test Problem Verification: $37,500

Project Management & Advisory Milestones

Project Management & Advisory Oversight (Part-Time): $130,000

Social Milestones

Present Results at Polkadot Decoded 2024 (Part-Time Marketing Coordinator): $3,000
Host virtual tester experience event (Part-Time Marketing Coordinator): $3,000