Add main body and diagrams for phase II formal verification blog article - #7
Add main body and diagrams for phase II formal verification blog article#7chrihop wants to merge 6 commits into
Conversation
There was a problem hiding this comment.
Pull request overview
Adds a new blog post draft describing Phase II formal verification progress for OSTD soundness (with diagrams), and introduces an English logo SVG asset.
Changes:
- Add a new post: “Verifying OSTD soundness” describing vertical/horizontal composition and invariants for UB-freedom.
- Add a new SVG asset (
logo_en.svg) underassets/images/.
Reviewed changes
Copilot reviewed 1 out of 6 changed files in this pull request and generated 10 comments.
| File | Description |
|---|---|
assets/images/logo_en.svg |
Adds a new SVG logo asset to the site’s image bundle. |
_posts/2026-tbd-verifying-ostd-soundness.md |
Adds the main body of the formal verification blog article, including figures/diagrams and example specs. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tatetian
left a comment
tatetian
left a comment
There was a problem hiding this comment.
Thanks for writing up this post! The core technical content -- proving soundness via defined behavior, vertical composition (soundness-correctness feedback loop), and horizontal composition (invariant preservation) -- is solid.
However, the post needs significant revision before it's ready for a broad audience:
- Blocking: Missing Jekyll front matter and placeholder filename date prevent the post from rendering.
- Title and framing: "Verifying OSTD soundness" frames the post as a project update, but its real value is educational -- a methodology piece on proving soundness for unsafe Rust.
- Audience accessibility: Many Asterinas/OSTD-specific concepts are used without introduction, but the post will reach a broad Rust audience via "This Week in Rust."
- Narrative structure: The Verus section is misplaced and disconnected from the composition narrative; the Vertical Composition subsection ends on a tangent; multiple "soundness" variants create unnecessary confusion.
- Repetition: Every major section restates its core insight 3-5 times across prose, blockquotes, and figure captions -- the single biggest obstacle to the PR description's own "concise requirement."
- Diagrams: Figure 1's text doesn't match the diagram's labels; Figure 3 is unreadable at rendered size.
| **Enter: [Verus](https://github.com/verus-lang/verus).** Verus is a dialect of Rust intended for formal deductive verification of code. Unlike Rust, Verus has no distinction between safe and unsafe code. Instead, all operations that might cause **UB** in Rust (and many that are defined but might cause unexpected behavior, like integer arithmetic that could overflow or underflow) require the checker to construct a proof that their preconditions are satisfied. | ||
|
|
||
| Verus verifies proofs on a per-function basis, annotating each function with pre- and post-conditions that its SMT solver checks at every exit point. Many of these proofs are discharged automatically from the surrounding code: for instance, when `x` is `unsigned`, | ||
|
|
||
| ```rust | ||
| if x > 0 { x - 1 } else { 0 } | ||
| ``` | ||
|
|
||
| requires no human intervention to prove the subtraction is safe. For operations the solver cannot resolve on its own, the user provides an explicit *witness*, a piece of ghost code that carries a logical ‘fact’ the compiler needs but discards after verification. | ||
|
|
||
| For memory accesses, this witness is a [`PointsTo`](https://asterinas.github.io/vostd/vstd_extra/cast_ptr/struct.PointsTo.html) object, encoding the fact that an address holds a particular value. This means that Verus code can reason explicitly about unsafe code that is still well-defined in the Rust memory model. In the Rust MM, writing through a pointer that was cast from an integer is valid if there is some known object in that location that previously had its address ‘exposed’, but it is incumbent on the programmer to ensure that this is the case, and that the object in question is always the one that was intended. In Verus reading and writing through any pointer requires an explicit proof that the target object exists, in the form of the `PointsTo` token. The programmer's job is to use ghost state to track the value of the tokens, much like the Rust programmer tracks objects in memory, but now with a verifier to check the work. | ||
|
|
||
| Verifying individual functions in isolation, however, is only the beginning. The real challenge lies in how those per-function specifications are composed across the entire codebase. As we will see, it is precisely this composition, both vertical across call stacks and horizontal across calling contexts, that allows local proof obligations to accumulate into a system-wide guarantee. | ||
|
|
||
| > **The key to effective verification is composing those specifications, both vertically and horizontally.** |
There was a problem hiding this comment.
Verus material deserves its own section and needs tighter focus on what serves the post's narrative: Two issues:
1. Structure -- Verus is wedged into "Proving Rust Soundness Positively" but is a separate topic. The section is about a conceptual insight (prove defined behavior, not absence of UB). The Verus material is about tooling. Verus deserves its own ## heading (e.g., "Verification with Verus") to make the structure honest.
2. Relevance -- much of the Verus content doesn't connect to the rest of the post:
-
PointsTotokens (line 55): Explained at length, including a deep dive into Rust memory model provenance and exposed-address semantics. ButPointsTonever appears again in the post -- not in the vertical composition example (which usesEntry::replaceandCursorMut::map), nor in the horizontal composition invariant (which usesEntryOwnerandMetaRegionOwners). The reader invests effort understanding it and then it's abandoned. Thepoints-to.pngimage, which illustrates this concept well, is included in the PR but never referenced. IfPointsTostays, use the diagram; if it's cut, remove the image. -
SMT solver and automatic proof discharge (lines 47-51): The
if x > 0 { x - 1 } else { 0 }example illustrates Verus basics but has nothing to do with kernel verification. It doesn't set up any concept used later. -
Witnesses and ghost code (line 53): This concept is important --
EntryOwnerandMetaRegionOwnersin the horizontal composition section are exactly this kind of ghost state, andCursorModelis a ghost struct. But the connection is never made explicit. The reader learns about "ghost code" here and encounters ghost structs later without realizing they're the same concept. -
Missing: how Verus specs compose -- The one thing the Verus section should set up -- that Verus verifies per-function pre/post-conditions, and that a caller's preconditions can be discharged by its callee's postconditions -- is mentioned in passing (line 47) but not emphasized. This is exactly the mechanism that makes vertical composition work, and it deserves to be the centerpiece.
In short, the Verus section explains how Verus works in general rather than the aspects that matter for this post. Consider restructuring to: (a) briefly introduce Verus; (b) focus on per-function specs with pre/post-conditions (the basis for vertical composition); (c) introduce ghost state as the mechanism for tracking invariants (the basis for horizontal composition); and (d) either cut or drastically shorten the PointsTo/provenance material.
Also, line 55's paragraph is very long -- it covers PointsTo, Rust MM provenance semantics, and ghost-state tracking in a single block. If the PointsTo content is kept, break it into shorter paragraphs.
There was a problem hiding this comment.
Verus material is now introduced right away, before moving on to the actual property definition. Vertical composition is explained at this point, because it's so fundamental to Verus' structure, leaving the question of horizontal composition to be explained once we have the property.
| At the top of the stack, the [**public API of OSTD**](https://asterinas.github.io/api-docs/0.17.1/ostd/index.html), we are no longer writing specs for other proofs to consume. This changes what a good specification looks like. Internal specs must track implementation details closely because they are consumed by other proofs. The consumer for an external spec is the reader, attempting to understand exactly what has been verified. For a human audience, the specifications should be more abstract, so that it is clear at a glance that they capture desirable properties of the system. And in being more abstract, they are also represented differently from the code they describe, meaning that if the original code is buggy, the specification is less likely to simply reproduce the bug. | ||
|
|
||
| > Descriptions of what a module *should* do, not of what it *happens* to do. | ||
|
|
||
| For instance, the [specification for a linked list cursor](https://asterinas.github.io/vostd/ostd/specs/mm/frame/linked_list/linked_list_owners/struct.CursorModel.html) is a pair of mathematical sequences, representing the whole list bifurcated by the cursor: | ||
|
|
||
| ```rust | ||
| // Verus mathematical sequence model | ||
| pub ghost struct CursorModel { | ||
| pub ghost fore: Seq<LinkModel>, | ||
| pub ghost rear: Seq<LinkModel>, | ||
| pub ghost list_model: LinkedListModel, | ||
| } | ||
| ``` |
There was a problem hiding this comment.
Tangent that derails Vertical Composition and ends abruptly: The Vertical Composition subsection (lines 61-89) has two parts, and the second doesn't belong:
Lines 61-74 are the actual vertical composition argument: caller soundness requires callee correctness, illustrated with the Entry::replace → CursorMut::replace_cur_entry → CursorMut::map chain, capped by Figure 2. This is strong and self-contained.
Lines 76-89 pivot to a different topic: what makes a good spec at the API boundary (abstract vs. implementation-tracking). This is a spec design philosophy point, not a composition point.
The CursorModel example compounds the problem:
- It has no connection to the vertical composition argument. The reader was following
Entry::replace→CursorMut::mapand suddenly encounters a linked list cursor. - It ends the subsection abruptly. The code block is the last thing before "Horizontal Composition" -- no concluding sentence, no tie-back.
- The reader has no context for why a linked list cursor exists in a memory management module, or what
LinkModelandLinkedListModelrepresent.
Consider either: (a) cutting lines 76-89 entirely and ending the subsection on the strong Figure 2 at line 74, or (b) giving the abstract-spec point its own short subsection with a better-motivated example.
There was a problem hiding this comment.
Dropped the CursorModel example. We don't really need to get into the different kinds of specifications. The rest of this section has been merged into the Verus discussion, where hopefully it flows better.
|
|
||
| *(Foreword: This post summarizes our progress in verifying OSTD and highlights key results from our research papers. This work is carried out in collaboration with [CertiK](https://www.certik.com/).)* | ||
|
|
||
| You can trust Rust. Millions of developers sleep soundly on the promise that Rust is safer than other systems-level programming languages. That's why we chose it for Asterinas -- if any system needs to be trusted, it's a kernel. Our framekernel architecture confines all unsafe code to OSTD, a minimal 15,000-line trusted core. If OSTD is unsound, the entire 100,000-line kernel is unsafe as well. |
There was a problem hiding this comment.
Minor wording nit: In a post about Rust verification, "unsafe" is an overloaded term. The kernel's code doesn't become unsafe Rust -- its safety guarantees are voided. Consider: "...the safety guarantees of the entire 100,000-line kernel are compromised."
There was a problem hiding this comment.
Filename uses placeholder date tbd: The Jekyll filename convention is YYYY-MM-DD-slug.md. The tbd will cause Jekyll to either fail to parse the date or sort the post incorrectly. This should be updated to the intended publication date before merging.
Please ensure that the post can be rendered correctly before marking the PR as "Ready for Review".
There was a problem hiding this comment.
The current draft is 2026-04-01-verifying-ostd-soundness.md because that's when I created it. When we decide on a publication date I will change it.
tatetian
left a comment
tatetian
left a comment
There was a problem hiding this comment.
(Supplementary comment from the same review — the original submission missed this one due to a parser limitation.)
|
I marked this PR as "Draft". Please resolve or reply all issues. When you are done with the revision, mark it as "Ready for Review". Thanks. |
| ```rust-verus | ||
| impl<C: PageTableConfig> EntryOwner<C> { | ||
|
|
||
| pub open spec fn metaregion_sound(self, regions: MetaRegionOwners) -> bool { |
There was a problem hiding this comment.
This code does not match the latest version. Please modify this after we finalize our model in June.
|
|
||
| We began a year ago with a proof of concept, verifying selected properties of individual functions but leaving the bulk of the code unverified. After taking lessons from that phase and scaling up our efforts, in just over a year we have expanded to cover the entire virtual memory subsystem of the memory management (`mm`) module, from raw physical frame allocation at the bottom to virtual address space mapping at the top. Recall that horizontal composition is vital for proving soundness: verifying an entire subsystem is much more valuable than disconnected functions. Meanwhile, a parallel project called [CortenMM](https://dl.acm.org/doi/10.1145/3731569.3764836) has verified the complex concurrent correctness of the page table's fine-grained locking, and has been published in SOSP '25. | ||
|
|
||
| As a proxy for cost, historically, formal verification requires about 20 lines of mathematical proof for every 1 line of code (a 1:20 ratio). This immense cost has blocked widespread industrial adoption. **We reduced this ratio to below 1:4.** |
There was a problem hiding this comment.
Do we still need to show the proof-code-ratio, as more and more proofs are generated by AI (which is not very good at generating concise proofs)?
There was a problem hiding this comment.
I've been debating this myself. On the one hand, the ration is still close to accurate. Even with AI generating very verbose proofs, we are at 32,000 LoC total, ~27,000 proof lines and ~5,000 original. So that's about 5:1, still much less verbose than many Rocq developments.
On the other hand, using this as a performance metric does imply some strange incentives, and AI magnifies them. Currently, shrinking proofs requires a separate manual or AI pass, so it takes more time, not less. It may still be desirable for readability, but that's a separate issue.
I'm going to look around a little this weekend and see if I can get some reference points for person-months:LoC rations on similar projects. That is a much more direct measurement.
There was a problem hiding this comment.
I'm finding that many projects focus on proof-to-code ratios rather than actual labor time. SeL4 is the odd one out, they openly mention their 20py. Individual CertiKOS papers are pretty consistent about claiming 2py for each paper's worth of improvement on the project. Our most direct comparison point is probably Atmosphere, but they only present proof:code ratio, not labor time.
There is also the confounding factor that an employee-year and a grad-student-year are probably not directly comparable, which may explain why CertiKOS comes in so low.
We can do a proper accounting of how much total labor we've put in, and that would be interesting to discuss. But proof:code ratio is a more established metric in the literature, and it's one where we are still doing well despite AI being verbose.
There was a problem hiding this comment.
Thanks for your detailed discussion! Labor time is indeed a very valuable metric, we should take this into account. As for the proof-code ratio, I agree to preserve it since the figure still looks good.
|
|
||
| This architecture gives kernel developers access to the powerful abstractions and guarantees of safe Rust. It also makes OSTD's soundness incredibly load-bearing. OSTD consists of about 15,000 lines of mechanism code. Sitting above it are over 100,000 lines of safe policy code, written under the guarantees of Rust's high-level features. This massive upper layer automatically inherits Rust's guarantees if and only if OSTD's public API is sound. A bug in OSTD isn't just a localized issue; it compromises the safety guarantees of the entire rest of the kernel. | ||
|
|
||
| When a small piece of code has an outsized impact on system reliability, it is the perfect candidate for **formal verification** (FV). FV uses mathematical logic to create machine-checked proofs that guarantee the code behaves exactly as intended. |
There was a problem hiding this comment.
Perhaps we can add a hyperlink to the Wikipedia page of Hoare Logic here, as the audience may not be familiar with FV.
|
|
||
| For complex verification, Verus also allows us to add *ghost state* that exists only during the verification. Because ghost variables are not compiled into executable code, they have no performance impact. They are only used to instrument the code to make information about the broader system legible to the verifier. For example, Verus' pointer libraries provide a ghost [`PointsTo<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/simple_pptr/struct.PointsTo.html) type which encodes the current state of a piece of raw memory containing an object of type `T`. A `PointsTo` can only be constructed and modified through [*valid pointer operations*](https://verus-lang.github.io/verus/verusdoc/vstd/simple_pptr/struct.PPtr.html#example), so its existence provides the "witness" for Verus that the current state of an object in memory is valid. | ||
|
|
||
| We define our own ghost types that track parts of the system state that are invisible to any given function. A page table is a tree of nodes and their entries, so a [`PageTableOwner`](https://asterinas.github.io/vostd/ostd/specs/mm/page_table/struct.PageTableOwner.html) is a tree of [`EntryOwner`](https://asterinas.github.io/vostd/ostd/specs/mm/page_table/node/entry_owners/struct.EntryOwner.html) and [`NodeOwner`](https://asterinas.github.io/vostd/ostd/specs/mm/page_table/node/owners/struct.NodeOwner.html) ghost objects, each describing the current state of a concrete object in the system without the need for executable code to access it. |
There was a problem hiding this comment.
These two owners are not well-documented. Users who visit these links will be confused, I believe.
There was a problem hiding this comment.
Added some explanation to the text, and will push the accompanying documentation later tonight.
There was a problem hiding this comment.
The level correspondence part of the OwnerSubtree documentation (which is closely related to PageTableOwner) is ill-formed.
| } | ||
| ``` | ||
|
|
||
| The [`paths_if_in_pt`](https://asterinas.github.io/vostd/ostd/specs/mm/frame/meta_owners/struct.MetaSlotOwner.html#structfield.path_if_in_pt) clause, present only in the `is_node()` branch, ensures that each page table **node** corresponds to exactly one position in the tree. The equivalent condition for mapped frames (`.is_frame()`) is weaker, only requiring that the current entry's path be contained in the set. Because the same physical frame may legitimately be mapped to multiple virtual addresses simultaneously, this does not cause UB from the kernel's perspective. Soundness proofs do not let us place obligations on the caller; our model needs to be flexible enough to specify even erroneous (but well-defined) calls. |
|
|
||
| The [`paths_if_in_pt`](https://asterinas.github.io/vostd/ostd/specs/mm/frame/meta_owners/struct.MetaSlotOwner.html#structfield.path_if_in_pt) clause, present only in the `is_node()` branch, ensures that each page table **node** corresponds to exactly one position in the tree. The equivalent condition for mapped frames (`.is_frame()`) is weaker, only requiring that the current entry's path be contained in the set. Because the same physical frame may legitimately be mapped to multiple virtual addresses simultaneously, this does not cause UB from the kernel's perspective. Soundness proofs do not let us place obligations on the caller; our model needs to be flexible enough to specify even erroneous (but well-defined) calls. | ||
|
|
||
| Collectively, system invariants like metaregion_sound define the strict rules that every public API must preserve. This is exactly why verifying isolated functions is insufficient. Even if individual functions are completely correct in a vacuum, any unverified code touching the same data structures could silently violate these shared invariants, thus collapsing the entire system's proof. To guarantee true soundness, the module must be verified as a cohesive whole. We check the final soundness property by embedding the specifications of verified functions in a state machine, which may take arbitrary steps using the specification of any function in any order. |
There was a problem hiding this comment.
Should metaregion _sound use a code format?
|
|
||
| This efficiency comes from two factors: Verus’ automated SMT solver effortlessly handles routine mathematical obligations in the background, and OSTD’s tightly scoped, modular architecture prevents proof complexity from spiraling out of control. | ||
|
|
||
| Advances in AI help us scale even faster. Because proof annotations often follow predictable patterns derived from the system model, AI can be very effective in helping the SMT solver handle proofs that previously would require human guidance. To this end we built **KVerus**, an AI-assisted tool that automatically generates a growing fraction of our proofs. Crucially, AI assistance accelerates the writing process but does not alter the trustworthiness of the results. Every single proof generated by KVerus is strictly checked and validated by Verus's mathematical solver. AI frees our engineers to focus on the big picture questions: specifications, system models, and proof strategy. |
There was a problem hiding this comment.
Please add the arXiv link for KVerus. https://arxiv.org/abs/2605.03822
| } else { | ||
| true | ||
| } | ||
| } |
There was a problem hiding this comment.
Maybe we do not need the definition in such detail. We may only keep key definitions like &&& regions.slot_owners[idx].paths_in_pt == set![self.path] and add some inline comments. It is up to you.
|
|
||
| Advances in AI help us scale even faster. Because proof annotations often follow predictable patterns derived from the system model, AI can be very effective in helping the SMT solver handle proofs that previously would require human guidance. To this end we built **KVerus**, an AI-assisted tool that automatically generates a growing fraction of our proofs. Crucially, AI assistance accelerates the writing process but does not alter the trustworthiness of the results. Every single proof generated by KVerus is strictly checked and validated by Verus's mathematical solver. AI frees our engineers to focus on the big picture questions: specifications, system models, and proof strategy. | ||
|
|
||
| Another common critique of formal verification is that proofs quickly become outdated as code evolves. Verification projects are usually static, pinned to a particular version of the target software. We began our verification on OSTD v0.15 and are currently tracking v0.16.0. Thanks to our modular invariant structure and KVerus's ability to help repair proofs, updating our verification alongside codebase changes has proven quite manageable. Our ultimate goal is continuous verification: updating proofs in the same pull request as the code they cover. |
There was a problem hiding this comment.
I'm not sure whether we can make any strong statements about this, as Asterinas has evolved to 0.18.0.
There was a problem hiding this comment.
Do we have plans to roll the verified code up to 0.17, or even to 0.18? If so we could frame this more as future work, with 0.15 -> 0.16 as a proof of concept.
There was a problem hiding this comment.
Yes, it is planned, but it will be no earlier than 26Q4. Framing as future work sounds like a good idea.
| **[Asterinas](https://github.com/asterinas/asterinas)** is a Linux ABI-compatible, general purpose OS kernel written entirely in Rust. It uses a novel **[framekernel architecture](https://asterinas.github.io/book/kernel/the-framekernel-architecture.html)** that enforces a strict separation between *mechanism* and *policy*: | ||
|
|
||
| - **Mechanism:** The Operating System Standard Library ([OSTD](https://asterinas.github.io/book/ostd/index.html)) handles the raw, dangerous primitives: physical memory management, page tables, and hardware configuration. These are the operations that cannot be implemented in safe Rust. | ||
| - **Policy:** Everything built on top of OSTD, such as scheduling, file systems, and network protocols, dictates system behavior. This layer is implemented entirely in *safe Rust*, strictly enforced by `#![deny(unsafe_code)]` in every crate outside OSTD. |
There was a problem hiding this comment.
I think the beginning could flow more smoothly. The introduction of Asterinas seems to interrupt the narrative a bit. Do we need to go into the Framekernel structure again, given that it has already been covered in another blog post? https://asterinas.github.io/2025/06/04/kernel-memory-safety-mission-accomplished.html
There was a problem hiding this comment.
I agree. I'm streamlining that, still talking about the frame kernel structure and its implications, but more briefly.
|
|
||
| ### Methodology of the Verification | ||
|
|
||
| Our verification tool of choice is [Verus](https://github.com/verus-lang/verus), which integrates directly with the Rust language. Verus code is Rust code, with additional constructs that allow us to annotate functions with preconditions (boolean formulae that must be true in order to safely call the function) and postconditions (which we would like to prove to hold when the function returns). The Verus compiler converts the pre- and postconditions of each function's into constraints in a satisfiability problem and feeds the result to an SMT solver to exhaustively check whether the postconditions hold. |
There was a problem hiding this comment.
The SMT part does not seem to be very helpful to a kernel developer. Instead, we may emphasize Verus prove codes by logic.
|
Pushing a new version that addresses these. |
rikosellic
left a comment
rikosellic
left a comment
There was a problem hiding this comment.
LGTM. All my concerns have been addressed, except for the labour time statistics. Thanks for your contribution!
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Syntax highlighting is not enabled on the preview sites. I will look into it. |
This comment was marked as resolved.
This comment was marked as resolved.
|
Regarding labor time, if we want to include that: on our end, phase II would be about 1.5py. I don't know how you guys distributed your work between |
@SNoAnd Does this 1.5py include Haobin's previous work at CertiK? |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Yes. |
|
@SNoAnd It will be 0.9 py in total, of which 0.5 on sync, 0.2 on mm, and 0.2 on general infrastructure. |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
tatetian
left a comment
tatetian
left a comment
There was a problem hiding this comment.
Before I make any comments on the content of the post, I need to get rid of the following distractions:
- It contains too many commits (24 in total). A lot of them seems to be intermediate ones. Please clean up the Git history by squashing all intermediate commits. Make sure that each resulting commits are atomic.
- It adds many figures. This shows that putting all figures in
image/is unscalable. I suggest adding a subdirectoryimage/<post-name>for all images to be added for this post. - It adds many font files. Because the Git history is a mess, I didn't bother to locate the exact commit that adds these font files. I assume that they added because text embed in the added SVG figures require fonts. While I like SVG, adding whatever font files required by a new SVG file would be unsustainable for this website. I think we got two options:
- Edit your SVG files locally to use the fonts that are already used by the Website;
- Turn your SVG files into PNG.
- It adds many HTML snippets (
highlights/*.html): Again, because the Git history is a mess, I don't even bother to look up the Git history to try figure out why these HTML snippets are added. I assume that there is no strong justification because the Phase 1 blog post also includes Rust and Verus source code and they are syntax highlighted just fine. And even if you want to enhance syntax highlighting, this should be done in a separate PR. Show the improvement using the Phase 1 blog post. - It includes some changes to the CSS. As I said, the Phase 1 blog post contains all the Markdown elements used in the Phase 2 blog post. If any bugs are found in the CSS or improvements are to be made, do so in a separate PR.
- It includes several Ruby scripts. After the Git history is clean, I will read the commit message to figure out the rationale of adding them. Please make a good justification for adding these scripts.
tatetian
left a comment
tatetian
left a comment
There was a problem hiding this comment.
Thanks for improving this post constantly. It looks much strong than its previous versions.
2925f9d to
48f3707
Compare
85803c4 to
3721605
Compare
All commits are now squashed into a single one.
All figures are now housed under
This site does not currently feature a proprietary font family. Instead, it utilizes the fonts provided by the operating system. To ensure consistency of figures across all operating systems, PNG files are employed to display all diagrams.
The default syntax highlighting engine in Jekyll (Rouge) has a known limitation when rendering Rust code with nested generic angle brackets (e.g.,
The CSS is added to improve the display of LaTeX formulas. Will submit a separate PR to address this.
All Ruby scripts have been removed since we now use pure PNG to display the diagrams, maintaining the hygiene of this repo. |
3721605 to
a70bd01
Compare
Add the Phase II formal verification article, supporting diagrams, and the small layout/style updates needed to render it.
a70bd01 to
ef0349d
Compare
|
We've gone through all your comments and have updated the draft accordingly. We're eager to hear your thoughts on the new version. Please feel free to share any feedback or suggestions! |
|
|
||
| Our verification tool of choice is [Verus](https://github.com/verus-lang/verus), which integrates directly with the Rust language. Verus code is Rust code, with additional constructs that allow us to annotate functions with preconditions (boolean formulae that must be true in order to safely call the function) and postconditions (which we would like to prove to hold when the function returns). The Verus compiler converts the pre- and postconditions of each function into a logical representation and searches for a proof that all executions that satisfy the preconditions must, at each function exit, satisfy the postconditions. | ||
|
|
||
| For complex verification, Verus also allows us to add *ghost state* that exists only during the verification. Because ghost variables are not compiled into executable code, they have no performance impact. They are only used to instrument the code to make information about the broader system legible to the verifier. For example, Verus' pointer libraries provide a ghost [`PointsTo<T>`](https://verus-lang.github.io/verus/verusdoc/vstd/simple_pptr/struct.PointsTo.html) type which encodes the current state of a piece of raw memory containing an object of type `T`. A `PointsTo` can only be constructed and modified through [*valid pointer operations*](https://verus-lang.github.io/verus/verusdoc/vstd/simple_pptr/struct.PPtr.html#example), so its existence provides the "witness" for Verus that the current state of an object in memory is valid. |
There was a problem hiding this comment.
Should we add a small figure or code example of PointsTo here to give the reader a taste of ghost state?
There was a problem hiding this comment.
I added a simple side-by-side code example.
|
|
||
| <img src="/assets/images/verifying-ostd-soundness/horizontal.png" alt="Soundness as Horizontal Composition" style="max-width: 800px; width: 100%; height: auto;"> | ||
|
|
||
| To see this in practice, let's look at selected clauses from `metaregion_sound`, the most critical system invariant in the memory management (`mm`) module. Below is an abbreviated version. This rule is defined on an [`EntryOwner`](https://asterinas.github.io/vostd/ostd/specs/mm/page_table/node/entry_owners/struct.EntryOwner.html#method.metaregion_sound), the abstract ghost state associated with an entry in a page table. It asserts that the associated page table entry matches the global physical memory records ([`MetaRegionOwners`](https://asterinas.github.io/vostd/ostd/specs/mm/frame/meta_region_owners/struct.MetaRegionOwners.html)), which live in a special metadata region. |
There was a problem hiding this comment.
I'm not sure whether we need this metaregion_sound part. I feel it is impossible for a reader without FV or Verus background to understand this. It may be enough to only give the high-level concepts of composition, soundness and invariants.
There was a problem hiding this comment.
In place of embedded code, I gave some examples of invariants in plain language with links to their locations if someone wants to look at the actual code.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
|
||
| In short, we describe the overall system in terms of logical state, and specify how that state is allowed to change during execution. Then, Verus checks that our specifications hold through mathematical deduction. These individual function specifications, combined across the entire system, must support our ultimate claim of soundness. | ||
|
|
||
| What does that mean? |
There was a problem hiding this comment.
I think the key idea in the Methodology of Verification section is that formal verification gives us the ability to precisely describe the program’s state and its properties. The state and its properties do not live directly in the code; rather, they often exist implicitly in developers’ minds as they write code and make abstract inferences about its behavior.
Once we can express states explicitly, we can also define composition and invariants around them. We can keep the discussion at a high level and include less actual Verus code.
There was a problem hiding this comment.
Then, soundness means that the program will never reach a state where UB occurs, while correctness characterizes the set of states the program is allowed to reach.
Therefore, to prove soundness, we need to establish correctness: unless we know which states the program can reach, we cannot determine whether the program will eventually enter a state that triggers UB!
There was a problem hiding this comment.
I've made some changes, mostly in the introduction to the section, to adopt this framing.
|
@tatetian, could you please take a look and share your feedback? |
303580f to
ed48c36
Compare
ed48c36 to
91b2640
Compare
tatetian
left a comment
tatetian
left a comment
There was a problem hiding this comment.
This version is much stronger! I appreciate the hard work. It is a strong piece, but not yet ready to ship. Here is my comments to further improve it.
| perm: Tracked<&mut PointsTo<u8>>) | ||
| requires | ||
| old(perm).pptr() == ptr, | ||
| !old(perm).is_init(), |
There was a problem hiding this comment.
The pre-condition requires the memory pointed by ptr to be uninitialized? This is a surprise to me. In Rust, valid pointers must refer to initialized memory.
There was a problem hiding this comment.
Verus pointers have take/put semantics. Reading a value from the pointer with take leaves it 'uninitialized' to represent the value being moved, which ensures no duplication of values. Storing a value with put conversely requires the pointer to be in that 'uninitialized' state. The value of the latter is less clear to me than the former, but it does ask the programmer to be explicit about destroying overwritten values, by first withdrawing them and letting them fall out of scope.
There was a problem hiding this comment.
Thanks for explaining. But based on your explanation, I don't think that the spec for set should include the !old(perm).is_init() precondition. u8 is a scalar type of Copy. In Rust semantics, it can be overwritten arbitrarily. An ordinary Rust program would think a set function with the set(ptr: *mut u8, val: u8) signature would allow any value inside ptr to be overwritten. On the other hand, if we change the signature to set(ptr: *mut Vec<u8>, val: Vec<u8>), requiring !is_init() would be important.
In summary, we can remove this precondition to avoid potential confusion.
| </div> | ||
| </div> | ||
|
|
||
| We define our own ghost types that track parts of the system state that are invisible to any given function. A page table is a tree of nodes and their entries, so a [`PageTableOwner`](https://asterinas.github.io/vostd/ostd/specs/mm/page_table/struct.PageTableOwner.html) is a tree of [`EntryOwner`](https://asterinas.github.io/vostd/ostd/specs/mm/page_table/node/entry_owners/struct.EntryOwner.html) and [`NodeOwner`](https://asterinas.github.io/vostd/ostd/specs/mm/page_table/node/owners/struct.NodeOwner.html) ghost objects, each describing the current state of a concrete object in the system without the need for executable code to access it. |
There was a problem hiding this comment.
"A page table is a tree of nodes" --> "For example, a page table is a tree of nodes"
The latter one reads better.
Now that the page table is an example (of ghost states), we should not say Entry::replace is "a concrete example" (see the next paragraph). Instead, we can write: "Let's zoom into a concrete function, Entry::replace, which overwrites ...".
In addition, I think we should make Entry::replace a hyperlink so that interested people can look into its code.
There was a problem hiding this comment.
I've linked directly to its code. It might be better to link to a Rustdoc so that the link doesn't break if the line number changes, but Entry::replace is not public visibility, so it currently doesn't get a Rustdoc.
There was a problem hiding this comment.
but
Entry::replaceis not public visibility, so it currently doesn't get a Rustdoc.
Use Github's permlink. Here is an example:
|
Thanks for the feedback! I believe this version addresses all of these comments. |
|
Updated the |
We’d love for you to take a look and share any suggestions you might have about the lessons learned from our recent work on the formal verification of Asterinas OSTD. Your input would be really valuable! Thanks!
Principles and outlines:
Target audience: Kernel and Rust developers. We may briefly recap verification basics, but avoid explaining concepts they already know (e.g., do not trust the caller in the "adversarial guarantees" or link to unsafe in “What is soundness”).
Key idea: To prove no UB, we have to prove defined behaviour.
Concise requirement: The blog is currently too long; aim for roughly 5–6 pages with tighter exposition and reduced repetition.
Compositional verification goals:
-- Vertical composability: Individual functions should be verified in a way that enables sound composition across abstraction layers.
-- Horizontal composability: The system architecture should support composition across modules/components.
Invariant design: Move specific and concrete invariants, avoiding vague descriptions.
Whole picture: Put all things into the whole picture, distinguishing user and kernel memory.