I tried building a benchmark for formally verifying popular Rust OSS. Along the way, I ended up finding real security vulnerabilities.
In my previous article, I introduced h5i, an Axum-based Rust web framework that allows developers to translate application logic into Lean 4 and formally verify properties such as authorization, data isolation, and business rules.
The core idea of h5i is pretty simple: instead of relying on unit tests alone to check whether an application behaves correctly, we want to mathematically prove that real implementations satisfy specific properties. To achieve this, h5i adopts a kernel-based architecture that allows security-critical application logic to be automatically translated into Lean 4 (see my previous article for details).
To find out whether this approach works for real-world systems, I started building h5i-app-bench, a benchmark that takes existing Axum-based Rust open-source projects, ports their core implementations to h5i, and attempts to formally verify their correctness using Lean 4. Since h5i itself is built on Axum, porting existing Axum applications to h5i was relatively straightforward.
Although I was able to prove most of the selected security properties, I also encountered several properties that I couldn’t prove in Lean 4. Investigating these failed proof attempts revealed bugs in the original Rust implementations, which I then confirmed with concrete tests against the upstream projects.
Some turned out to be real security vulnerabilities, including cross-user data deletion, access-control bypasses, information disclosure, and denial of service in widely used open-source projects.
Here are a few findings that have already been fixed and publicly disclosed. Some of the corresponding benchmark cases, including RustiCal, are still being prepared and have not yet been published.
1. RustiCal: One User Could Delete Another User’s Data
The first example is RustiCal (GHSA-9cp5–7crm-9cf7), a Rust-based CalDAV and CardDAV server.
The bug was surprisingly simple. RustiCal stores calendar objects using three identifiers:
(principal, calendar_id, object_id)Here, principal identifies the owner. Suppose Alice and Bob both have a calendar named work, containing an event named meeting.ics. These are two completely different objects belonging to different users. However, the hard-delete path executed a database query equivalent to:
DELETE FROM calendarobjects
WHERE cal_id = ? AND id = ?;Notice what is missing? The owner’s identity. The application correctly checked that Alice was authorized to delete her own event. But the resulting SQL operation could also delete Bob’s event if the calendar and object identifiers matched.
In a reproduction against the original application:
Alice deletes Bob's event directly
-> 401 UnauthorizedAlice deletes her own matching event
-> 200 OK
Bob tries to read his event
-> 404 Not Found
The authorization check worked at the HTTP layer, but the database operation affected a larger set of objects than the authorization decision permitted.
2. OxiCloud: File Metadata Leaked Through Music Playlists
The next example comes from OxiCloud PR #796, a Rust-based file management and sharing platform.
OxiCloud has an authorization system that controls which files a user can access. The interesting part was its music playlist functionality.
A user could create a playlist and add file identifiers to it. However, the application checked whether the user could modify the playlist without sufficiently checking whether the user could access the referenced files.
The resulting behavior was roughly:
Alice owns a playlist
|
v
Alice adds Bob's file ID
|
v
Playlist accepts the reference
|
v
Alice requests playlist tracks
|
v
Bob's private file metadata is returnedThe leaked information included file names, sizes, MIME types, and audio metadata. The underlying issue was that permission to modify a playlist was being confused with permission to read the files referenced by that playlist.
3. RustFS: A Policy Evaluation That Could Loop Forever
Not every interesting finding involved authorization. While working with RustFS, an S3-compatible object storage system written in Rust, I also encountered a non-termination bug in its policy-variable resolution logic, which was published as GHSA-9wgh-5r68–49p7.
Specifically, RustFS supports variables in access-control policies, such as:
${aws:AccountId}
${aws:username}These variables are substituted with values from the request context.
The implementation already had a maximum iteration count intended to prevent unbounded expansion. However, the limit was enforced only in the outer resolution loop. A nested substitution routine could repeatedly reconstruct a variable expression and expand it again without returning to that outer loop.
As a result, a tiny input could trigger more than 100,000 resolver calls, while an ordinary input required just one. In certain configurations, this could lead to a denial of service.
4. Why Did Building a Verification Benchmark Reveal Bugs?
One lesson from this experiment was that formal verification changes how we inspect software.
When conducting ordinary security testing, we often start by looking for suspicious endpoints, missing checks, or known vulnerability patterns.
When formalizing an application, we start with a different question: What property is this code supposed to guarantee?
For example:
- Can one user ever modify another user’s data?
- Does every successful operation satisfy the declared access policy?
- Can an API response reveal an object that the caller cannot read?
- Does a recursive or iterative operation always terminate?
To prove these properties, we need to understand the relevant behavior precisely. That process often exposes assumptions that were never explicitly enforced.
- In RustiCal, authorization was checked, but the final database operation was insufficiently scoped.
- In OxiCloud, playlist permissions did not imply permissions on the referenced files.
- In RustFS, an iteration bound did not actually bound the inner computation.
Of course, an unsuccessful proof is not automatically evidence of a vulnerability. It may simply mean that the proof is incomplete, the model is incorrect, or the translation does not support some language feature.
But when a property cannot be proved, investigating why can sometimes reveal a real bug. And that is exactly what made this experiment interesting.
5. What’s Next?
I am continuing to develop h5i-app-bench to understand how formal verification with Lean 4 can scale to real Rust applications.
The benchmark currently includes six published application ports and 101 selected specifications, covering real-world authorization, identity management, file sharing, policy evaluation, and event visibility logic.
AI coding agents are making it dramatically easier to generate large amounts of application code. But generating more code does not automatically make it correct or secure.
We need better ways to check what that code actually guarantees. My original goal was simply to benchmark a framework for proving Rust application correctness. But along the way, I learned that formal verification isn’t just about proving software correct. It can also help us discover where our assumptions about correctness break down.
Links