How Open Source Projects are Using Kani to Write Better Software in Rust

Today we’re excited to tell you about the Kani Rust Verifier (or Kani, for short), an open source automated reasoning tool developed by Amazon Web Services for analyzing and proving properties of your Rust code. Like other automated reasoning tools, Kani provides a way to definitively check, using mathematical techniques, whether a property of your code is true under all circumstances. In this way, Kani helps you write better software with fewer bugs.

As developers, we love the Rust programming language because of its focus on performance, reliability and productivity. Out of the box, Rust is fast (it does not require a runtime or garbage collector) and safe in the sense that its strong type system and ownership model can statically guarantee memory and thread-safety by default.

This is an excellent foundation, but Rust still needs testing and automated reasoning tools to address properties beyond type safety, such as when a developer would like assurances about properties such as absence of runtime errors or functional correctness. Alternatively, a developer may need low-level control (e.g., for performance or resource efficiency) that is too subtle for the compiler to understand, so they must use unsafe Rust, which is not fully checked by the compiler. In cases like these, testing and automated reasoning tools can provide complementary and extended assurances to the built-in capabilities of Rust.

At AWS, we see a future where there is a smooth path for Rust developers to adopt as much testing and automated reasoning as they feel is appropriate for their project’s needs. A journey with lots of stops along the way: from the familiar built-in testing capabilities of the language, to automated testing with MIRI and sanitizers, to fuzzing and property-based testing, and then lightweight automated reasoning tools, such as MIRAI and now Kani, that prove simple requirements, and finally automated reasoning tools such as Creusot and Prusti that prove more-involved requirements. We imagine a wide spectrum of tools to help Rust developers ensure that their code is secure and correct.

Amazon has invested in Kani and made it open source. At AWS, we have used Kani on projects such as Firecracker and s2n-quic. The broader open source community continues to find more applications for Kani as well. In this post, we will highlight some of the notable examples of Kani’s impact.

Firecracker

In 2023, Firecracker engineers used Kani to validate security boundaries in the Firecracker codebase. In order to achieve the highest levels of security, Firecracker engineers have applied the Kani model checker to verify safety-critical properties in core components of the Firecracker Virtual Machine Monitor using mathematical logic.

Firecracker is also an open source project from Amazon. Written in Rust, Firecracker uses the Linux Kernel-based Virtual Machine (KVM) to create and manage microVMs. Firecracker has a minimalist design which allows for fast (~150ms) microVM start-up time. It also enables secure multi-tenancy of microVMs on the same host and memory/CPU over-subscription. AWS Lambda, AWS Fargate, and parts of AWS Analytics use Firecracker to build their service platforms.

In a previous blog post, we demonstrated how Kani helped Firecracker harden two core components, specifically the I/O rate limiter and I/O transport layer (VirtIO), by presenting the issues we were able to identify and fix. Particularly, the second part of this post picks up from a previous Kani/Firecracker blog post and shows how improvements to Kani over the last year made verifying conformance with a section of the VirtIO specification feasible.

Thanks to Kani, the Firecracker team was able to verify critical areas of code that were intractable to traditional methods. These include the noisy-neighbor mitigation, a rate limiter, where interactions with the system clock resulted in traditional testing being unreliable, as well as the VirtIO stack, where the interaction with guest memory lead to a state space impossible to cover by other means.

In total, five bugs were found in the rate limiter implementation, the most significant one was a rounding error that allowed guests to exceed their prescribed I/O bandwidth by up to 0.01% in some cases. Additionally, engineers found one bug in the VirtIO stack, where an untrusted guest could set up a virtio queue that partially overlapped with the MMIO memory region, resulting in Firecracker crashing on boot. Finally, the debug assertions added to the code under verification allowed us to identify a handful of unit tests which were not set up correctly. All issues have been investigated and fixed!

All in all, analysis of the code using Kani has proven a valuable defense-in-depth measure for Firecracker, nicely complementing the existing testing infrastructure.

Hifitime

Hifitime is a scientifically accurate time management library that provides nanosecond precision of durations and time computations for 65,000 centuries in most time scales (also called time systems). It is useful wherever a monotonic clock is needed, even in the presence of leap seconds or remote time corrections (like for Network Time Protocol or Precise Time Protocol). It is suitable for desktop applications and for embedded systems without a floating point unit (FPU). It also supports the typical features of date time management libraries, like the formatting and parsing of date times in a no-std environment using the typical C89 tokens, or a human friendly approximation of the difference between dates. For scientific and engineering applications, it is mostly tailored to astronomy (with the inclusion of the UT1 time scale), astrodynamics (with the ET and TDB time scales), and global navigation satellite systems (with the GPS, Galileo, and BeiDou time scales).

This blog post on the Kani Rust Verifier Blog shows how Kani helped solve a number of important non-trivial bugs in hifitime. For the sake of completeness, let’s start with an introduction of the notion of time, how hifitime avoids loss of precision, and finally why Kani is crucial to ensuring the correctness of hifitime. Kani has helped fix at least eight different categories of bugs in a single pull request: https://github.com/nyx-space/hifitime/pull/192. Most of these were bugs near the boundaries of a Duration definition: around the zero, maximum, and minimum durations. But many of the bugs were on important and common operations: partial equality, negation, addition, and subtraction operations. These bugs weren’t due to lax testing: there are over 74 integration tests with plenty of checks within each. This was the first blog post from an external contributor to the Kani blog. The Kani team is very excited for this contribution and thanks Christopher Rabotin for his time, interest, and copacetic use of Kani.

S2N-QUIC

s2n-quic is a Rust implementation of the QUIC protocol, a transport protocol designed for fast and secure communication between hosts in a network. QUIC is relatively new, but it builds upon and learns from TCP (Transmission Control Protocol), the transport protocol that has been the standard for communication on the Internet for decades.

TCP is the underlying protocol for HTTP/1.1 and HTTP/2, but for the latest generation HTTP/3, QUIC is used instead. In that respect, QUIC can be thought of as a next-generation version of TCP with new features such as stream multiplexing and connection migration.

However, the improvements over TCP go beyond just new features and functionality. Notably, QUIC is secure by default; the specification requires TLS be used within the QUIC handshake to establish encryption and authentication keys, and subsequently every QUIC packet is protected using these keys. With TCP, confidentiality and integrity were not part of the protocol design, and thus TLS was layered on top of TCP, as is done in HTTPS.

Requiring encryption by default is one of many improvements to security, functionality, and performance that the designers of the QUIC protocol learned from earlier protocols such as TCP. And similarly, when s2n-quic was developed at AWS, engineers incorporated learnings from other protocol implementations. One of these learnings was the importance of using a verification tool like Kani to gain confidence in the properties we assert about critical code that is used for processing terabytes or more of data formatted, transmitted and encrypted as part of the QUIC protocol.

In the remainder of this blog post, we’ll show a few examples of how AWS uses Kani to easily and automatically verify the correctness of the code. It ultimately inspires confidence and helps in improving and optimizing s2n-quic.

Kani & Bolero

Ever wonder if you can combine fuzz testing techniques and verification? On the Kani blog we show how you can use fuzzing and verification in a unified framework, which is enabled by the integration of the Kani Rust Verifier in Bolero.

Bolero is a property-testing framework that makes it easy for users to test a piece of Rust code with multiple fuzzing engines, and Kani is a verification tool that allows users to prove certain properties about their Rust code. Integrating Kani with Bolero has enabled users to apply multiple testing methods, namely fuzzing and proofs, to the same harness.

Kani & ChatGPT

Recently, ChatGPT—OpenAI’s AI chatbot built on top of Large Language Models (LLMs)—has taken the world by storm. People are using ChatGPT to write blog posts, do homework, and even write code! That’s right: LLMs like ChatGPT can be used to write code, since code is essentially just another kind of text. All you need to do is provide a text prompt describing the program you want, and ChatGPT will generate the code for you, along with an explanation.

The Kani team was also eager to explore the possibilities of using LLMs for daily coding tasks, so they decided to put ChatGPT to the test. In this blog post, they share their experiences with using ChatGPT and Kani to solve example coding problems, and explore how these technologies could revolutionize the way to approach software development. The experiments include the following three tasks:

1. Writing a prompt to generate unverified code with ChatGPT.
2. Checking the generated code with Kani to see if it’s correct.
3. Using ChatGPT and Kani iteratively to converge to code that passes verification.

The experiments show that, while ChatGPT is easy to use and can efficiently generate code from text description, the generated code does not always do what it is supposed to do. This is where verification tools like Kani can help detect bugs, corner cases and unexpected behavior in the generated code, thereby helping users of ChatGPT write more proven code.

Conclusion

Kani is a multi-faceted tool that can be used to prove properties on a system, exhaustively test a system, and be integrated with other frameworks to achieve a twofer. The open source community has adopted and reacted extremely positively to Kani, as is evident by the usage of Kani in open source projects such as s2n-quic, firecracker, and hifitime. Here is a direct quote from an unknown user on Kani’s Reddit community:

I’m very impressed with Kani. My previous attempts to learn something about formal verification via Lean and Coq never got off the ground. Along with my LinkedIn post, I also posted links on Reddit (https://www.reddit.com/user/carlk22) to the article. I’m disappointed that more people aren’t excited about the idea of formal verification of AI-generated code. I have been tweaking the article based on feedback (including adding a “related work” section that references the Kani blog post from May). I also plan to more fully address the concern that formal specifications are always hard to write. I’ll submit a link to next week’s This Week in Rust, which should get some notice.

Kani is succeeding in changing the perception, effectiveness, and usability of verification tools that were previously thought to be cumbersome or beyond reach. AWS invests in Kani to strengthen the Rust community at large and develop an ecosystem that enables the development of the most secure, reliable, and available software/services. Kani is an epitome of Amazon investing in open source software for achieving the long term vision of a two way collaboration between industry and research organizations. We at AWS encourage you to join this effort and be part of the conversation!