Krabcake Goals

Notes for revision

• (see inline comments!)
• some customers will already have some of this context
• "dont bake me cake"
  • at very least, add a design tradeoffs section, in particular "why not just instrument"
  • how is this different from Kani / doesn't Kani already give me this?
  • what is value proposition versus full-verification
• add customer-centric

Potential Questions from Readers

• Why not (re)use more of Miri itself, or extend Miri?
• Why can't Miri utilize foreign code?
  • Why can't Miri call the foreign machine code directly (control flow jump)
  • Why can't Miri interpret the foreign machine code
• Why not recompile the C code to fit Miri's model? (and/or recompile C code into MIR and then instrument that)
  • That's a lot of development effort. A lot.
  • Even when finished, that's a bad customer experience (having to recompile all their C dependencies).
  • This strategy pays off when third-party vendors provide precompiled objects of the "sanitized" C code etc. see e.g. LLVM's MemorySanitizer, where they provide a build of sanitized libc.
  • Also, may be untenable for customer's to recompile their code. Valgrind should handle this seamlessly for them.
  • Plus, the rules here are still being actively researched. We need to leverage dynamic instrumentation to let us iterate more quickly on the semantic checks we're putting in.
• Where does Valgrind fit into this?
  • people won't know much about Valgrind's architecture. Give mile-high view of it, what Krabcake is leveraging, and what Krabcake is adding.

Krabcake Goals

see also krabcake internals

Audience: people who want to use the tool, and want to understand its capabilities: 1. what it promises to do, and 2. what it does not promise (or cannot promise).

Press Release

2024-03-01: The Rust project, in partnership with the Valgrind developers, today announces the delivery of Krabcake, a tool for observing if a Rust program encounters undefined behavior.

Since 2018, Rust users have used Miri, Rust's MIR^[1] interpreter, and its Stacked Borrows memory model to validate snippets of unsafe code in isolation. Today, the same safety checks provided by Miri are available for large scale programs that depend on arbitrary C/C++ libraries.

Ferris DeCrab says "I've used Miri as a teaching aid for understanding Rust's memory model, and to exercise small prototype libraries leveraging unsafe code, but it was too much work to accommodate Miri for my day-to-day work. This is different. Now, if I have any unsafe code in my code or a new crate dependency, I just add krabcake to my command line, and I get all the same checking that Miri provided. It just works."

Krabcake provides the same validation features as Miri while removing its main limitations. Unlike Miri, Krabcake works with both inline assembly and calls to external C/C++ library code. Krabcake works on any Rust program compatible with Valgrind. The initial Krabcake release supports x86_64/Linux. Support for x86/Linux and ARM64/Linux is planned for late 2024.

(End Press Release)

Product Overview

REVISE STRUCTURE: Status Quo/Shiny Future framework doesn't work well here, because it forces upfront discussion of Miri details. Instead: Merge the two together, (Miri vs Krabcake) UX, (Miri vs Krabcake) removing limitations

The Krabcake Vision: Miri's benefits without the drawbacks

Rust promises that safety violations cannot arise from safe code.

Any safety violation in a Rust program is a fault in either the Rust build tools (e.g. the Rust compiler), or in some piece of unsafe Rust code that has been linked together with the safe Rust code. But how can one be confident that one's unsafe Rust code is free of such issues?

Krabcake is our answer.

To explain the problem being solved by Krabcake, we will imagine a developer, Alexis, working on a sort routine in Rust. Alexis has decided to use unsafe code blocks, and wants to validate their soundness.

Tool Invocation

note(Bryan): Suggestion for how to make this section shorter/more terse.

---

Today, Alexis might validate their code against Miri by invoking cargo miri run. This runs the code atop Miri, a MIR interpreter that checks that Rust's rules, e.g. for borrowing logic, are upheld.

To Alexis, Krabcake's workflow appears to be just like Miri's. Running cargo krabcake run/test will compile your Rust source in a mode that instruments Rust's borrowing operations^[2] in the generated native machine code. The resulting linked program or test suite is then run atop valgrind, and Krabcake ensures that every operation, both from Rust and from any native library linked to the program, obeys the rules of the instrumented borrowing logic embedded into the binary. The same flags as regular cargo run/test invocations are supported (for example, filter).

After installing Krabcake, invocations of cargo krabcake build will compile your Rust source in a mode that instruments Rust's borrowing operations^[2:1] in the generated native machine code.

cargo krabcake run executes the resulting linked program atop valgrind, and ensures that every operation, both from Rust and from any native library linked to the program, obeys the rules of the instrumented borrowing logic embedded into the binary.

Likewise, cargo krabcake test compiles and runs your crate's test suite with the same embedding of Rust's borrowing logic.

cargo krabcake run/test supports the same flags as cargo run/test; for example, cargo krabcake test filter only runs the tests containing filter in their name.

Today, Alexis might validate their code against Miri by invoking cargo miri run. This runs the code atop Miri, a MIR interpreter that checks that Rust's rules for borrowing logic are upheld (and other things).

Krabcake's interface is just like Miri's: It is integrated with Cargo, so that you can just type cargo +nightly krabcake run and get the same feedback about Undefined Behavior that Miri would show.

Similarly, to run one's test suite atop Miri, one invokes cargo miri test. To run the testsuite atop Krabcake, one invokes cargo krabcake test.

The Feedback Loop

Both Miri and Krabcake can provide feedback about soundness violations that would otherwise go undetected.

Consider if Alexis invokes a swap procedure and passes the same pointer address for the two arguments to swap, like so:

let mut spot = 10;
unsafe {
    let ptr = std::ptr::addr_of_mut!(spot);
    std::mem::swap(&mut *ptr, &mut *ptr);
}
// with `fn swap<T>(x: &mut T, y: &mut T)`

The above code breaks Rust's semantic rules, but does so in a manner that is accepted at compile time.

Miri, unlike the Rust compiler, detects and signals the fault as it interprets the prologue of the fn swap method, and then explains^[3] the cause of the fault.

cargo +nightly miri run ends by emitting an error similar to this:

error: Memory location does not grant <4460> unique access
   --> /ruststd/library/core/src/mem/mod.rs:719:22
    |
719 | pub const fn swap<T>(x: &mut T, y: &mut T) {
    |                      ^

The tool's diagnostics tell us that swap tried to validate that x's borrow (named <4460> in this example) has mutually exclusive access to its data, but that memory location is no longer available for the borrow to claim exclusive access over.

The diagnostics finish by highlighting where the borrow was created…

help: <4460> was created by a SharedReadWrite retag
   --> src/main.rs:12:17
    |
12  |     std::mem::swap(&mut *ptr, &mut *ptr);
    |                    ^^^^^^^^^

…and where it lost its exclusive access:

help: <4460> was later invalidated here
   --> src/main.rs:12:28
    |
12  |     std::mem::swap(&mut *ptr, &mut *ptr);
    |                               ^^^^^^^^^

Using Miri in the manner above is the current state of the art for validating "Unsafe Rust" code.

Krabcake's user experience is just like that of Miri's (modulo details of diagnostic improvements). After running the program atop Krabcake, the tool signals the fault at the point where the program attempts to use exclusive access via a borrowing pointer that no longer has the rights for such access, with diagnostics indicating where the borrow was created and where the access was revoked.

Miri's limits

After addressing these problems, Alexis might also want to compare the performance of their sort routine against another, mysort, written in C. However, after adding the appropriate extern "C" { ... } block and an unsafe call to mysort in their code, Alexis encounters this error from Miri:

52 |     mysort(base, num_elems, size, compar, ctxt);
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |     |
   |     can't call foreign function `mysort` on OS `linux`

This represents a fundamental issue with Miri's interpretive architecture: Miri does not support several features used in real Rust programs. Leveraging Miri introduces new constraints on your software architecture:

• The unsafe code you want to check cannot use inline assembly nor foreign functions, except the small set for which Miri provides built-in support (Standard C shims, Unix shims).
• Furthermore, you must craft a miri-customized test suite that similarly avoids using any functionality unsupported by Miri.

There are ways to address these problems; one might design shims that emulate, in Rust, the input/output/side-effecting behavior of the foreign library routines your program needs. Or one might extend Miri itself to support the routines in question.

Resolving these issues requires effort. It is a significant barrier for leveraging Miri in one's validation strategy.

Miri's limitations = Krabcake's strengths

Krabcake operates on a compiled binary that is linked to native code. This means Krabcake carries neither of the limitations listed above for Miri:

• Krabcake handles inline assembly
• Krabcake handles functions that invoke foreign libraries

Lets continue with our running example of running a foreign sorting function, mysort.

Alexis can just run cargo +nightly krabcake run. Krabcake will dynamically instrument the code of both the compiled Rust binary and the implementation of the mysort routine.

fn process_1(data: &mut [&mut i32]) {
    let elem_sz = size_of::<&mut i32>();
    fn compare(a: &mut i32, b: &mut i32) -> isize { *a - *b }
    unsafe {
        // Krabcake calls back C into Rust with no problem
        mysort(data.as_ptr(), data.len(), elem_sz, compare);
    }
}

Assuming the Rust code is correct and the side-effects of running mysort do not violate any Rust language invariants, then no problems are signalled by Krabcake for invocations of process_1.

FIXME: Revise the paragraph below, potentially spelling out the two cases of interest of foreign code that breaks the rules:

1. broken foreign code
2. working foreign code but Garbage-In-Amplified-Garbage-Out

If there is some violation of Rust language invariants, either due to bugs in mysort itself, or due to bugs in the Rust code that cause it to violate preconditions of mysort that subsequently corrupt Rust's invariants, then Krabcake will signal that as an error as soon as it has evidence of the resulting corruption. See Appendix C for a detailed example.

Appendix A

Project Tenets

• No false positives: If the Krabcake tool says your program has undefined behavior, then it does (or you have found a bug in Krabcake).
  • Why this matters: We want people to treat the output of the tool seriously, and not try to handwave it away with "well this is just catching behavior that is correlated with bugs, but in this case I argue that this behavior is not an issue."
• Recompile and run: You do not need to change your source code to leverage Krabcake; you do not even need to disable release mode. You just do cargo krabcake run, and Krabcake handles the rest (namely: recompiling the program with the appropriate extra rustc flags, and then running it atop valgrind --tool=krabcake).
  • However, it is certainly expected that Krabcake will catch more instances of undefined behavior from your source code if you do disable optimizations (one might even go further and use -Zmir-opt-level=0, hypothetically?)
• Embrace incompleteness: Part of our goal is to operate on programs that have been subject to compiler optimizations. In that context, we cannot provide any guarantees to catch undefined behavior, because a compiler is free to convert a program with undefined behavior into a program that has any behavior at all.
• No unexplored territory: Every check put into Krabcake has already been prototyped in the context of Miri.

Appendix B

Broken Foreign Code Example

Appendix C

Garbage-In-Garbage-Out Example

Give a human readable explanation of what the hell we are talking about here.

Namely: The C code is working correctly, and this is illustrating garbage-in-garbage-out.

ALSO: think about presenting/discussion the other case of interest where the C code itself does have a bug that causes Rust UB and thus you would only find it atop a shim with a 100% faithful translation of the C code into a shim.

Consider this variation on the above:

fn process_2(data: &mut [&mut i32]) {
    let elem_sz = size_of::<&mut i32>();
    fn compare(a: &mut i32, b: &mut i32) -> isize { random() }
    unsafe {
        mysort(data.as_ptr(), data.len(), elem_sz, compare);
    }
}

Let us assume that if the preconditions of mysort are violated and the callback compare does not represent a transitive order, mysort may duplicate some elements in the array to be sorted. Thus, process_2 above may well modify data such that the same address occurs multiple time; that is, it may inject aliasing of data that was guaranteed to be unaliased, violating the internal invariants of Rust.

Krabcake, just like Miri, will detect this problem when there is proof in hand that the rules have been violated. Assume the distinct entries Ra and Rb in the incorrectly sorted data both point to a supposedly-unaliased memory location M, and that program attempts to access them at execution points 1. Ra, 2. Rb, 3. Ra. Then Krabcake will flag an error at either execution point 2. (the access to Rb that follows Ra) or point execution 3. (the second access to Ra that follows Rb), with a message like:

35     | let _b = *data[1];
       |          ^^^^^^^^
       |          |
       |          attempting a read access using <5305> at alloc2221[0x0], but that tag does not exist in the borrow stack for this location
       |          this error occurs as part of an access at alloc2221[0x0..0x4]
       |
       |      
       = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <5305> was created by a Unique retag at offsets [0x0..0x4]
  --> foreign_sort_code/mysort.c:8014
8014   |	*pi++ = *pj;
       |
help: <5305> was later invalidated at offsets [0x0..0x4] by a read access
  --> src/main.rs:34:15
       |
34     | let _a = *data[0];
       |          ^^^^^^^^

---

1. "MIR" is a Rust intermediate code representation that includes the explicit borrowing operators & and &mut. ↩︎

2. A Rust programmer must state intent when manipulating memory, stating whether each safe reference to memory, or "borrow", is mutually exclusive (&mut) or intended to be shared (&). However, these statements of intent are solely to serve Rust's compile-time analyses, and turn into normal memory addresses in the generated code generated from Rust's Middle IR (MIR). Thus, if we to distinguish &mut from & at runtime, we need extra information embedded into the object code generated by the compiler. ↩︎ ↩︎

3. In this presentation, we have replaced Miri's diagnostic jargon specific to the Stacked Borrows memory model proposed for Rust with readable english explanations.) ↩︎