Introduction

In the Fall of 2024, I had the opportunity to participate in a practicum project at Carnegie Mellon University in collaboration with Amazon Web Services (AWS). The project focused on formal verification for the Rust programming language, leveraging the Kani (Rust verification tool) to ensure the correctness and security of critical components in the Rust standard library. Engaging with the Rust ecosystem and collaborating with AWS engineers, I gained deep insights into formal verification techniques and professional cloud environments. In this post, I share the project’s objectives, my responsibilities, the challenges encountered, and the lessons I learned.

Project Objectives

The primary goal of this practicum was to design and implement an automated verification tool to validate critical modules in the Rust standard library. Given Rust’s strong emphasis on memory safety and performance, AWS recognizes it as a promising foundation for secure software systems. Our efforts aligned with AWS’s broader commitment to security and reliability, aiming to minimize potential software errors in widely-used Rust libraries.

My Role and Responsibilities

During the practicum, I devoted about 20 hours per week to advancing this verification initiative. My key responsibilities included:

Designing the Verification Tool and Integrations

I worked on setting up and configuring Kani, ensuring a robust environment for verification tasks. I established preconditions (#[requires]) and postconditions (#[ensures]) for critical functions such as NonZero::new_unchecked, NonZero::unchecked_mul, NonZero::unchecked_add, and NonZero::from_mut_unchecked. These contracts guaranteed that each verified function adhered to strict correctness criteria.

Implementing and Optimizing Proof Harnesses

I developed six proof harnesses for unsafe code blocks related to functions including max, min, clamp, rotate_left, rotate_right, and count_ones. Leveraging symbolic execution, these harnesses validated the functions’ behavior under all input conditions. This process required a deep understanding of Rust’s ownership model, NonZero types, and unsafe code semantics.

Analysis and Reporting

Collaborating closely with AWS engineers, I analyzed verification results to identify root causes of any inconsistencies or failed properties. By diagnosing issues—whether stemming from overlooked edge cases, incorrect assumptions, or tool limitations—we iteratively refined the verification process and enhanced reliability.

Code Refactoring and Collaboration

Responding to feedback from AWS maintainers, I consolidated verification harnesses into a unified mod verify structure, improving code readability and maintainability. I also switched from using unsafe code blocks to employing kani::any() for input generation, making the verification harnesses both safer and more idiomatic.

Additional Highlights

Verifying NonZero Methods

Verified methods like rotate_left, rotate_right, count_ones, cmp, clamp, max, and min for NonZero integer types. Over multiple PRs, addressed challenges like preserving the non-zero invariant and incorporated feedback from AWS engineers.

Integration with mod verify

Initially, each function had its own verification module. After code reviews, unified them into mod verify, improving clarity and aligning with team guidelines.

Avoiding Unsafe Blocks and Improving Input Generation

Replaced unsafe blocks with kani::any() to directly generate inputs for NonZero types, reducing unnecessary unsafe usage and improving code clarity.

Refining Naming Conventions and Macro Usage

Standardized variable naming and streamlined macros based on PR feedback to enhance maintainability and ensure verification proofs’ correctness.

Technical Challenges and Solutions

Adapting Formal Methods to Rust’s Paradigm

Proving properties for NonZero types demanded carefully constructed proofs. Using Kani’s model checking, I accounted for edge cases and systematically refined these proofs, ensuring operations like rotate_left and clamp never violated the NonZero invariants.

Managing Complexity and Iterative Improvement

Each function required careful consideration of all possible states. With iterative feedback from AWS engineers, I simplified code structures and created verification frameworks more adaptable to other standard library functions.

Integration into Kani’s Ecosystem

Our code contributions were integrated into the Kani team’s Rust standard library verification repository on GitHub: verify-rust-std. By submitting and merging pull requests, we not only verified essential parts of the standard library but also helped the AWS team improve Kani itself. Issues we encountered, along with corresponding discussions, were documented in the repository’s issue tracker. Furthermore, we created documentation and explanatory videos, providing valuable guidance for future contributors who wish to build upon or extend our verification work.

Accomplishments

  • Initial Setup: Successfully installed and configured Kani for formal verification.
  • Preconditions and Postconditions: Established #[requires] and #[ensures] for:
    • NonZero::new_unchecked
    • NonZero::unchecked_mul
    • NonZero::unchecked_add
    • NonZero::from_mut_unchecked
  • 6 Proof Harnesses for Unsafe Code:
    • max
    • min
    • clamp
    • rotate_left
    • rotate_right
    • count_ones
  • Test Harness: Developed a harness using symbolic execution to ensure expected behavior across all inputs.

Results and Impact

The integrated code changes and PRs solidified correctness properties for multiple NonZero methods. Our contributions represent a meaningful step toward fully verified Rust code within AWS’s infrastructure. Beyond immediate verification gains, this effort provided insights that helped the AWS team enhance Kani. The recorded issues, discussions, documentation, and instructional videos serve as a valuable resource, guiding future developers and researchers in extending and maintaining the verification framework.

Reflections and Future Directions

This practicum reinforced the importance of formal verification in building secure, reliable, and maintainable systems. By navigating Rust’s intricate type system and contributing to Kani’s ecosystem, I gained confidence in leveraging verification tools and methodologies. In the future, I plan to explore advanced verification techniques and apply these lessons to more complex data structures, concurrency patterns, and other critical system components, ensuring the continuous improvement of both the Rust ecosystem and its verification tooling.