---
breaks: false
---

# 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](https://hackmd.io/pZLgqsx8RQCjb-V3BUXQPA)

:::info
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.

[Valgrind]: https://valgrind.org/

Since [2018][sb-implemented], Rust users have used Miri, Rust's MIR[^what-is-mir] 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.

[^what-is-mir]: "MIR" is a Rust intermediate code representation that includes the explicit borrowing operators `&` and `&mut`.

[sb-implemented]: https://www.ralfj.de/blog/2018/11/16/stacked-borrows-implementation.html

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

:::info
*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

:::info
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[^borrow-ops] 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`).

[^borrow-ops]: 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.

:::

After installing Krabcake, invocations of `cargo krabcake build` will compile your Rust source in a mode that instruments Rust's borrowing operations[^borrow-ops] 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.

[^borrow-ops]: 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.

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[^creative-liberties] the cause of the fault.

[^creative-liberties]: In this presentation, we have replaced Miri's diagnostic jargon specific to the [Stacked Borrows][] memory model proposed for Rust with readable english explanations.)

[Stacked Borrows]: https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md

`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][Miri Common Shims], [Unix shims][Miri Unix Shims]).
* Furthermore, you must craft a miri-customized test suite that similarly avoids using any functionality unsupported by Miri.

[Miri Common Shims]: https://github.com/rust-lang/rust/blob/c50c62d225e004f5b488006d3d205a34363a128c/src/tools/miri/src/shims/foreign_items.rs#L527

[Miri Unix Shims]: https://github.com/rust-lang/rust/blob/c50c62d225e004f5b488006d3d205a34363a128c/src/tools/miri/src/shims/unix/foreign_items.rs#L27

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`.

:::info
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]: #Appendix-A
[Appendix B]: #Appendix-B
[Appendix C]: #Appendix-C

<a id="Appendix-A"></a>

## 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

:::info
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];
       |          ^^^^^^^^