Runtime Verification: Advanced Rust Property Test Verification for Polkadot Ecosystem
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)
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.
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
Comments (4)
Requested
Proposal Passed
Summary
0%
Aye
0%
Nay
Aye (69)0.0 DOT
Support0.0 DOT
Nay (7)0.0 DOT
Questions: Kontrol is built for evm, are you going to add support for polkadot as well in this proposal? https://github.com/runtimeverification/kontrol The pitch seems to be formal verification for rust, but how is this related to polkadot? As formal verification for rust is something very generic and could fit multiple other ecosystems like solana that is also written in rust. Formal verification has been around for a hot minute but is not so popular in more mainstream langauges but if you go to the academia world there already is Stable options for Haskell and Cox programming languages for this. Several other projects are currently working on various rust formal verifications such as: https://github.com/formal-land/coq-of-rust/(Aleph zero blockchain project funded this) https://inferara.com What is the difference between your system compaired to whats already avaliable?
@rust_syndicate
Thanks for your questions/engagement!
Kontrol is built for EVM, we are proposing to build the same tech-stack for Rust. Rust -> MIR is in general a much larger language/tech-stack than Solidity->EVM, so there is a decent amount of engineering work to do just to get to feature parity with Kontrol. We've done already quite a bit of research into how to integrate directly into rustc so that our tooling will be robust across all use cases. We definitely do plan to specialize to Polkadot as much as possible, and will draw all our examples from Polkadot examples (be it infrastructure tools that we can pull code from or smart contracts), but because of the size of the project and the advice we received to go for a smaller initial project, the first phase presented here is focused specifically on the core parts of the technology (MIR formalism, basic Rust property tests).
We do have a section of the proposal where we compare to some other Rust verification tools. Almost all the other tools (including the above linked one by Inferara) fall into 3 categories:
K, as a formalism, walks a very fine line between all of these approaches. It emphasizes the automated approach, and on keeping developers in their own workflow (working directly in Rust). In addition, we focus very heavily on ensuring that our semantics-based approach is correctly encoding the semantics of Rust, which is why emphasis is placed on collecting test-cases and actually making sure we agree on the execution of those test-cases with the existing Rust toolchains. This is the only way to make an industrial grade tool, is to integrate it directly into the existing toolchain and consume the entirety of the language, with confidence that we have the correct semantics.
However, when proving gets too difficult for fully automated techniques, you must have a way to assist the prover. K provides that as well, either directly in the form of K lemmas (expert mode), or as predicates in Rust (not planned for this proposal, but for future work, and is something we have experience with elsewhere).
The other main difference is the level of support we are willing to commit to a project. For 6 years we've been actively maintaining and updating our semantics of the Ethereum Virtual Machine (https://github.com/runtimeverification/evm-semantics/), and for 5 years we've been actively maintaining and updating our semantics of WebAssembly (https://github.com/runtimeverification/wasm-semantics). These are public goods used by more than just ourselves. We won't abandon the project or let it bitrot, we will continue to maintain it as Rust evolves. Indeed, the very nature of how the K Framework is designed (which is to separate the language semantics definition and the verification tooling), makes this possible. As our tools evolve and upgrade for Ethereum and other ecosystems, KMIR semantics will see the same benefits, and as Rust evolves and KMIR updates, the tools will continue to work.
We vote yes as this can benefit not only the Dotsama ecosystem but also open source rust code ecosystem. This being a win for more Rust tooling, We hope that this will make it to a public MIT repo soon and possible on crates.io.
@Rust Syndicate
Thank you for the support! We use BSD-3 license for all our software (which I believe is basically the same as MIT) as we want it to be unencumbered. Our repository is here https://github.com/runtimeverification/mir-semantics, where you can watch development, and we'll provide updates periodically at AAG!
Also, we will publish it as a crate!