Polkadot Virtual Machine (PVM) Formal Specification Development

Total ask: 371,875 USDC

Overview

We are excited to present a comprehensive proposal to the Polkadot community aimed at developing KPVM, a formal semantics of the Polkadot Virtual Machine (PVM) using the K Framework. This project is designed to span approximately 4 months and will involve two full-time engineers, with potential follow-up work to extend PVM tooling based on the formal semantics established in this proposal.

The formalization of PVM in K offers several significant advantages that will not only enhance the security and reliability of the Polkadot ecosystem but also provide immediate value to participants of the JAM bounty program. By establishing a precise and mathematically rigorous model of PVM, we lay the foundation for diverse client development, thorough conformance testing, and the creation of advanced developer tools.

Key Benefits of Formalizing PVM in K

Client Diversity: Formal semantics provide a single, authoritative source of truth for PVM’s expected behavior, independent of any specific implementation. This clarity eases the development of new PVM clients, particularly in the context of the JAM bounty, by allowing developers to refer to a precise but high-level semantics instead of grappling with the intricacies of a particular reference implementation. This will facilitate the development of a diverse ecosystem of PVM clients, enhancing the overall resilience and flexibility of the Polkadot network.
Conformance Testing: The formal model and corresponding reference interpreter generated from this model will allow for comprehensive conformance testing of various PVM implementations. This includes the PVM-to-x86 toolchain and other submissions for the JAM bounty program. By ensuring consistency and reliability across different platforms, we can significantly reduce the risk of discrepancies and vulnerabilities in PVM implementations, leading to a more secure and robust network.
Developer Tooling: Formal semantics are not just about correctness; they also provide a solid foundation for developing various developer tools. The K Framework automates much of this process, enabling the rapid creation of debuggers, property testing tools, and symbolic execution frameworks. These tools can significantly streamline the development workflow, making it easier for developers to write, test, and verify their code. This will ultimately lead to higher-quality software and faster development cycles within the Polkadot ecosystem.

Our Expertise and Track Record

Runtime Verification (RV) is particularly well-suited to undertake this project. We have a proven track record of applying these techniques to other blockchain ecosystems, notably through our work on KEVM—a formal semantics of the Ethereum Virtual Machine (EVM). The K Framework, our flagship product, has been successfully used to analyze and verify software across various languages, including Solidity/EVM, WebAssembly (Wasm), Michelson, and more. Our existing semantics for the RISC-V RV32EM architecture will enable us to quickly and efficiently develop KPVM.

Our past work includes the development of a range of tooling based on formal semantics, such as:

Formal Reference Specifications: Online auto-updated specifications of language semantics derived directly from their mathematical specification. For example, the JelloPaper.
Debuggers: Tools that allow developers to step through code execution to identify and fix bugs. For example, Simbolik.
Property Testing Tools: Automated tools that generate test cases to verify that software adheres to its specifications. For example, Kontrol.
Symbolic Execution Frameworks: Tools that analyze the behavior of software across all possible inputs to ensure correctness and security.

We are in close contact with Parity and the developers of PVM, and after our discussions, Parity encouraged RV to apply to the Polkadot treasury to proceed with this formal specification development. We bring extensive experience in both formal verification and blockchain systems, having completed numerous blockchain audits both inside and outside of Polkadot and verified several blockchain consensus protocols.

Problem Statement

In an increasingly digitized world, ensuring software correctness has never been more critical. This is especially true for blockchain applications, where the permissionless nature and the intertwining of financial systems and software make absolute correctness paramount. Traditional testing techniques and ad-hoc implementations have proven inadequate to secure these complex systems, as evidenced by the numerous exploits and security breaches that have occurred in recent years.

The Polkadot Virtual Machine (PVM) currently lacks a formal specification, which poses significant risks, including undetected bugs and vulnerabilities and the hindrance of new PVM client development. The K Framework offers the perfect environment to address these challenges, providing precise and executable formal definitions and a well-tested approach to developing the necessary tooling on top of this foundation.

By creating a formal semantics of PVM using the K Framework, we will establish the required level of correctness, security, and reliability for the software systems running on the Polkadot ecosystem. This foundational work is essential for the continued evolution and success of Polkadot as a leading multi-chain ecosystem, enabling a wide range of decentralized applications and services to thrive.

We welcome feedback from the community and look forward to working together to strengthen the security and reliability of Polkadot through this critical initiative.

Here are 5 key points about the SubSquare post on developing KPVM, a formal semantics of the Polkadot Virtual Machine (PVM) using the K Framework:

The project aims to develop a precise and mathematically rigorous model of PVM, which will enhance the security and reliability of the Polkadot ecosystem and provide immediate value to participants of the JAM bounty program.
Formal semantics provide a single, authoritative source of truth for PVM's expected behavior, independent of any specific implementation. This clarity eases the development of new PVM clients, particularly in the context of the JAM bounty, by allowing developers to refer to a precise but high-level semantics instead of grappling with the intricacies of a particular reference implementation.
The formal model and corresponding reference interpreter generated from this model will allow for comprehensive conformance testing of various PVM implementations, significantly reducing the risk of discrepancies and vulnerabilities in PVM implementations, leading to a more secure and robust network.
Formal semantics also provide a solid foundation for developing various developer tools, such as debuggers, property testing tools, and symbolic execution frameworks. These tools can significantly streamline the development workflow, making it easier for developers to write, test, and verify their code, ultimately leading to higher-quality software and faster development cycles within the Polkadot ecosystem.
The team behind the proposal, Runtime Verification (RV), has a proven track record of applying formal verification techniques to other blockchain ecosystems, notably through their work on KEVM, a formal semantics of the Ethereum Virtual Machine (EVM). They bring extensive experience in both formal verification and blockchain systems, having completed numerous blockchain audits both inside and outside of Polkadot and verified several blockchain consensus protocols.