Support Rust verification in SAW via `crucible-mir` #1859

RyanGlScott · 2023-04-18T19:07:16Z

This issue tracks the long-term goal of being able to verify Rust code by leveraging the mir-json tool to compile Rust code to .mir files, which can in turn be ingested by SAW. These .mir files then can be symbolically simulated using the crucible-mir library, which was recently split out of crux-mir to avoid having SAW incur a Crux dependency.

This is a fairly large undertaking, and as such, the work needed to add SAW support for Rust/MIR will likely be spread out over multiple PRs. Off of the top of my head, here are various tasks that will need to be done:

Nice to have, but not essential for a first cut:

Update the SAW bindists to include a mir-json-translated version of the Rust standard library, similar to what crux-mir does with this script. Also do this in the SAW Docker images. (Include MIR JSON files for Rust standard libs in SAW bindists #1868)
Run crux-mir-comp's test suite in CI (Run crux-mir-comp's test suite in CI #1887)
A mir_cast_to_immut_ref function for casting mutable refefences to immutable ones (Add mir_cast_to_immut_ref function #1954)
Reject duplicate mir_points_to statements in preconditions (Reject duplicate mir_points_to statements in a precondition #1956)
Mark Freeze statics as mutable (MIR: Require users to initialize Freeze statics in specifications #1957)
A mir_fresh_ref command, similar to llvm_fresh_pointer. (We would also want to implement mir_fresh_expanded_value such that it calls mir_fresh_ref under the hood to create fresh reference values.) (Handle reference types in mir_fresh_expanded_value #1975)
A mir_equal command, similar to llvm_equal (Add mir_equal and jvm_equal commands, similar to llvm_equal #1998)
Support for the &str type (Support MIR string slices #1997)
mir_ref_of/mir_ref_mut_of commands for taking a reference to a value, similar to Rust's &/&mut operators. (Add mir_ref_of/mir_ref_mut_of functions for allocating references directly from values #1999)
A mir_elem command for referencing elements of compound types, and a mir_field command for referencing fields of structs (mir_elem_{ref,value} and mir_field_{ref,value} #1983)
SAW options for configuring the behavior of the ?assertFalseOnError and ?printCrucible implicit parameters (crux-mir doesn't respect --assert-false-on-error crucible#1080)

The text was updated successfully, but these errors were encountered:

This implements an experimental `mir_load_module` command, the first SAW command dedicated to MIR (Rust) code. I have added a basic test case to kick the tires and ensure that everything works as you would expect. You can't do much with the resulting MIR module yet (besides printing it in the SAW repl), but more functionality for verifying the MIR code will come in future patches. This checks off one box in #1859.

This implements an experimental `mir_load_module` command, the first SAW command dedicated to MIR (Rust) code. I have added a basic test case to kick the tires and ensure that everything works as you would expect. You can't do much with the resulting MIR module yet (besides printing it in the SAW REPL), but more functionality for verifying the MIR code will come in future patches. Note that in order to produce a MIR JSON file suitable for SAW's needs, you must build your Rust code with one of the two `mir-json` tools added in GaloisInc/mir-json#41. This checks off one box in #1859.

When distributing SAW binaries, we want users to be able to turn their Rust code into MIR JSON with relatively minimal effort. To that end, this patch includes JSON files for the Rust standard libraries in SAW binary distributions so that users do not have to build this themselves. This mirrors how these files are included in `crux-mir` binary distributions. This checks off one box in #1859.

This implements just enough scaffolding to support the basics of a `mir_verify` command and related scaffolding, which is one of the main goals of #1859. When I say "basic", I really do mean that: there are quite a few things that do not work currently. These include: * `mir_alloc`/`mir_points_to` do not work yet. * Overrides (unsafe or otherwise) do not work yet. * There is no way to declare variables with `struct` or `enum` types. * Likely other things. These limitations notwithstanding, it is now possible to write MIR specifications for very simple functions such as the ones in the `test_mir_verify_basic` integration test. I will be adding additional capabilities in subsequent patches. Most of the code in this patch is not terribly exciting, as lots of it is cargo-culted from the LLVM and JVM backends. Ideally, we would find a way to deduplicate a lot more of this code, but this will not be straightforward without substantial refactoring in SAW. See #379. In addition to the code itself, I have also expanded the SAW manual to mention the variety of new MIR-related commands added in this patch. Of particular interest is that `mir_verify` allows you to specify function identifiers in multiple ways, which is provided as a convenience to SAW users. See the manual for more details. Checks off several boxes in #1859.

This patch adds support for specifying the memory layouts of allocations in MIR specifications through the following commands: * `mir_alloc`, which allocates an immutable reference, and `mir_alloc_mut`, which allocates a mutable reference. * `mir_points_to`, which declares that a reference points to a given value in a pre- or post-condition. These commands behave much like `llvm_alloc` and `llvm_points_to`, and the code for the MIR commands looks quite similar to the LLVM code as a result. The largest difference implementation-wise is that I need to call into the `crucible-mir` memory model in order to read values from and write values to references. This patch therefore bumps the `crucible` submodule to bring in the changes from GaloisInc/crucible#1105, which make it much more straightforward to use the `crucible-mir` memory model in a SAW setting. Along the way, this patch also performs some mild refactoring: * This adds a `ConditionMetadata` field to `MirPointsTo` for the benefit of using it in `learnPointsTo`. This required moving around some `ConditionMetadata` values in `crucible-mir-comp` as a result. * This moves the `CheckPointsToType` data type from `SAWScript.Crucible.LLVM.Builtins` to `SAWScript.Crucible.Common.Setup.Builtins`. This is because `CheckPointsToType` is now used in the `saw-remote-api` code that powers `mir_points_to` (see `SAWServer.MIRCrucibleSetup`), and it doesn't make much sense for this code to import LLVM-specific code. This checks off one box in #1859.

This adds support for a `mir_array_value` function in the MIR backend, which allows constructing array `SetupValue`s. This largely behaves like `llvm_array_value`s in the LLVM backend, but with the following differences: * Unlike in the LLVM backend, MIR arrays can have length 0. To account for this possibility, `mir_array_value` has a `MIRType` argument to ensure that SAW can always infer the type of the array, even if there are no element values from which to infer the type. Similarly, the SAW remote API's `array()` function now has an optional `element_type` kwarg that can be used to specify the element type in the event that there are no element values. * Because only the MIR backend makes use of the element type, this is encoded in the `XSetupArray` extension field. This checks off one box in #1859.

This adds support for the `mir_static` and `mir_static_initializer` functions in the MIR backend, which are used to write specifications involving top-level `static` values. These behave like the `llvm_global` and `llvm_global_initializer` functions in the LLVM backend, but with the following differences: 1. There is nor MIR counterpart to the `llvm_alloc_global` command, as MIR static values are not "allocated" in the same way that LLVM globals are. (We still require users to initialize mutable MIR statics, however.) 2. By design, static references created with `mir_static` cannot alias allocations created with `mir_alloc`, as the two forms of allocations are handled through different mechanisms in the `crucible-mir` memory model. This checks off one box in #1859.

This adds `mir_slice_value` and `mir_slice_range_value` functions to the MIR backend, which allow writing specifications involving slice arguments. Currently, only slices to array references are supported, although we may expand the scope of these commands in the future. Some interesting parts of the implementation: 1. The `TypeShape` for slices is _ever_-so-slightly different from the `TypeShape` for tuples (`TupleShape`), so I added a new `SliceShape` `TypeShape` to tell them apart. 2. There is a `MirSetupSliceRaw` constructor that is _only_ used for `crucible-mir-comp` purposes at the moment. In the future, we may want to expose a SAWScript command that uses this to allow users to directly construct a slice from a pointer and a length. 3. `mir_alloc` now explicitly disallows allocating slice references, so passing `mir_slice` or `mir_str` as an argument will throw an error. This checks off one box in #1859.

This adds a `mir_fresh_expanded_value` command, which creates a MIR value populated entirely by fresh symbolic variables. For compound types such as structs or arrays, this will explicitly set each field or element to contain a fresh symbolic variable. This is heavily inspired by the `llvm_fresh_expanded_val` command in the LLVM backend. This command will be important for the MIR user story going forward, as we will impose an requirement that all mutable allocations in an override must be explicitly set in the override's postconditions. The `mir_fresh_expanded_value` command provides a convenient way to quickly generate values to set in the postconditions. At present, `mir_fresh_expanded_value` comes with the limitation that it does not support reference types. This is not an inherent limitation, but it is one that will require some additional work to lift. In particular, we will likely need something like a `mir_fresh_ref` command (similar to LLVM's `llvm_fresh_pointer` command) to make this work. We leave the task of implementing `mir_fresh_ref` to a later patch. This checks off one box in #1859.

This implements supports for overrides in the SAW MIR backend, largely inspired by the existing implementation in the LLVM backend. I've added a `test_mir_unsafe_assume_spec` integration test to kick the tires and ensure the basics work as expected. Checks off one box in #1859. Still TODO: * Resolve the TODOs in the `test_mir_unsafe_assume_spec` test case (and the related code in `executeCond`) involving mutable allocations/statics in the postconditions of overrides. * Add a SAW remote API test case

This adds `mir_slice_value` and `mir_slice_range_value` functions to the MIR backend, which allow writing specifications involving slice arguments. Currently, only slices to array references are supported, although we may expand the scope of these commands in the future. Some interesting parts of the implementation: 1. The `TypeShape` for slices is _ever_-so-slightly different from the `TypeShape` for tuples (`TupleShape`), so I added a new `SliceShape` `TypeShape` to tell them apart. 2. There is a `MirSetupSliceRaw` constructor that is _only_ used for `crucible-mir-comp` purposes at the moment. In the future, we may want to expose a SAWScript command that uses this to allow users to directly construct a slice from a pointer and a length. 3. `mir_alloc` now explicitly disallows allocating slice references, so passing `mir_slice` or `mir_str` as an argument will throw an error. This checks off one box in #1859.

This implements supports for overrides in the SAW MIR backend, largely inspired by the existing implementation in the LLVM backend. I've added a `test_mir_unsafe_assume_spec` integration test to kick the tires and ensure the basics work as expected. Checks off one box in #1859. Still TODO: * Resolve the TODOs in the `test_mir_unsafe_assume_spec` test case (and the related code in `executeCond`) involving mutable allocations/statics in the postconditions of overrides. * Add a SAW remote API test case

This adds a `mir_fresh_expanded_value` command, which creates a MIR value populated entirely by fresh symbolic variables. For compound types such as structs or arrays, this will explicitly set each field or element to contain a fresh symbolic variable. This is heavily inspired by the `llvm_fresh_expanded_val` command in the LLVM backend. This command will be important for the MIR user story going forward, as we will impose an requirement that all mutable allocations in an override must be explicitly set in the override's postconditions. The `mir_fresh_expanded_value` command provides a convenient way to quickly generate values to set in the postconditions. At present, `mir_fresh_expanded_value` comes with the limitation that it does not support reference types. This is not an inherent limitation, but it is one that will require some additional work to lift. In particular, we will likely need something like a `mir_fresh_ref` command (similar to LLVM's `llvm_fresh_pointer` command) to make this work. We leave the task of implementing `mir_fresh_ref` to a later patch. This checks off one box in #1859.

This implements supports for compositional overrides in the SAW MIR backend, largely inspired by the existing implementation in the LLVM backend. I've added `test_mir_unsafe_assume_spec` and `test_mir_unsafe_assume_spec_statics` integration tests to kick the tires and ensure the basics work as expected. One place where the MIR backend meaningfully differs from the LLVM backend with respect to compositional overrides is in the treatment of mutable allocations. While the LLVM backend is content to simply invalidate the memory of underspecified mutable allocations that appear in the postconditions of overrides, the MIR backend is stricter and will outright reject any such underspecified mutable allocations, regardless of whether they are used or not. For further commentary on this, see the new sections of the SAW manual, as well as the `Note [MIR compositional verification and mutable allocations]` that describes the implementation. Checks off one box in #1859.

This adds basic support for enums in the MIR backend. In particular: * There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` function that constructs a value representing a specific enum variant, where the `String` indicates which variant to use. * The `mir_fresh_expanded_value` command can now create symbolic enum values. Implementation-wise, much of the complexity in this patch arises from the fact that MIR enums are represented with `VariantType`s at the Crucible level, which are a fair bit more involved than the `StructType`s used to power MIR structs. Some highlights of the implementation are: * There is now a new `EnumShape` constructor for `TypeShape`, which is in turn defined in terms of a new `VariantShape` data type that characterizes the shapes of all the fields in an enum variant. * There is a `MirSetupEnum` data type (exported by `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms of enum `MIRValue`s that one can construct. Currently, there is `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns when it creates a fresh enum value). * TODO RGS: Say something about symbolic enums * For now, there is no `crux-mir-comp` support for enums. We could conceivable add support, but there is not a pressing need to do so right now. I have opened #1990 as a reminder to do this later. This checks off one box in #1859.

This adds basic support for enums in the MIR backend. In particular: * There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` function that constructs a value representing a specific enum variant, where the `String` indicates which variant to use. * The `mir_fresh_expanded_value` command can now create symbolic enum values. Implementation-wise, much of the complexity in this patch arises from the fact that MIR enums are represented with `VariantType`s at the Crucible level, which are a fair bit more involved than the `StructType`s used to power MIR structs. Some highlights of the implementation are: * There is now a new `EnumShape` constructor for `TypeShape`, which is in turn defined in terms of a new `VariantShape` data type that characterizes the shapes of all the fields in an enum variant. * There is a `MirSetupEnum` data type (exported by `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms of enum `MIRValue`s that one can construct. Currently, there is `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns when it creates a fresh enum value). * The implementation of symbolic enum values in particular is somewhat complicated. I have written `Note [Symbolic enums]` to go over the general approach and highlight some potential pitfalls in implementing them. * For now, there is no `crux-mir-comp` support for enums. We could conceivable add support, but there is not a pressing need to do so right now. I have opened #1990 as a reminder to do this later. This checks off one box in #1859.

This patch adds an incomplete tutorial on how to use SAW to verify Rust code, which complements the existing tutorial that covers LLVM and JVM verification. This tutorial currently covers everything that has been implemented in SAW, which includes: * `mir-json` * `mir_verify` basics * References * Arrays * Tuples * Structs * Enums * `mir_fresh_expanded_value` * Slices As future patches add more changes to the SAW MIR backend, I will also update this tutorial at the same time to make sure that they stay in sync. Related to #1859.

This patch adds an incomplete tutorial on how to use SAW to verify Rust code, which complements the existing tutorial that covers LLVM and JVM verification. This tutorial currently covers everything that has been implemented in SAW, which includes: * `mir-json` * `mir_verify` basics * References * Arrays * Tuples * Structs * Enums * `mir_fresh_expanded_value` * Slices * Overrides * Statics As future patches add more changes to the SAW MIR backend, I will also update this tutorial at the same time to make sure that they stay in sync. Related to #1859.

This adds basic support for enums in the MIR backend. In particular: * There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` function that constructs a value representing a specific enum variant, where the `String` indicates which variant to use. * The `mir_fresh_expanded_value` command can now create symbolic enum values. Implementation-wise, much of the complexity in this patch arises from the fact that MIR enums are represented with `VariantType`s at the Crucible level, which are a fair bit more involved than the `StructType`s used to power MIR structs. Some highlights of the implementation are: * There is now a new `EnumShape` constructor for `TypeShape`, which is in turn defined in terms of a new `VariantShape` data type that characterizes the shapes of all the fields in an enum variant. * There is a `MirSetupEnum` data type (exported by `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms of enum `MIRValue`s that one can construct. Currently, there is `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns when it creates a fresh enum value). * The implementation of symbolic enum values in particular is somewhat complicated. I have written `Note [Symbolic enums]` to go over the general approach and highlight some potential pitfalls in implementing them. * For now, there is no `crux-mir-comp` support for enums. We could conceivable add support, but there is not a pressing need to do so right now. I have opened #1990 as a reminder to do this later. This checks off one box in #1859.

This patch adds an incomplete tutorial on how to use SAW to verify Rust code, which complements the existing tutorial that covers LLVM and JVM verification. This tutorial currently covers everything that has been implemented in SAW, which includes: * `mir-json` * `mir_verify` basics * References * Arrays * Tuples * Structs * Enums * `mir_fresh_expanded_value` * Slices * Overrides * Statics The final section of the tutorial describes a case study using SAW to verify a real-world piece of Rust code that implements the Salsa20 stream cipher. Related to #1859. [ci skip]

This patch adds an incomplete tutorial on how to use SAW to verify Rust code, which complements the existing tutorial that covers LLVM and JVM verification. This tutorial currently covers everything that has been implemented in SAW, which includes: * `mir-json` * `mir_verify` basics * References * Arrays * Tuples * Structs * Enums * `mir_fresh_expanded_value` * Slices * Overrides * Statics The final section of the tutorial describes a case study using SAW to verify a real-world piece of Rust code that implements the Salsa20 stream cipher. Related to #1859.

RyanGlScott · 2023-12-19T21:41:43Z

We have now implemented enough MIR-related functionality to write interesting SAW proofs involving Rust code. As such, I think this issue has outlived its usefulness, so I will close it. I have opened separate issues for the remaining tasks in the "nice to have" category, and I will tag related issues with the crucible/mir tag going forward.

RyanGlScott added the crucible/mir Related to crucible-mir verification label Apr 18, 2023

RyanGlScott self-assigned this Apr 18, 2023

This was referenced Apr 18, 2023

crucible-mir: Rename RustModule to MirModule GaloisInc/crucible#1082

Open

Add cargo saw-build command for producing MIR JSON files without testing them GaloisInc/mir-json#39

Closed

RyanGlScott mentioned this issue Apr 24, 2023

Implement mir_load_module #1863

Merged

RyanGlScott mentioned this issue May 9, 2023

Move copy of Rust standard libraries from crux-mir to crucible-mir GaloisInc/crucible#1089

Open

RyanGlScott mentioned this issue May 10, 2023

Include MIR JSON files for Rust standard libs in SAW bindists #1868

Draft

RyanGlScott mentioned this issue Aug 10, 2023

Prototype mir_verify command #1904

Merged

This was referenced Aug 21, 2023

Mir.Intrinsics functions use SimState when SymGlobalState/IntrinsicTypes would suffice GaloisInc/crucible#1105

Closed

Add Trees That Grow-style extension fields to SetupValue #1914

Closed

RyanGlScott mentioned this issue Aug 23, 2023

Support mir_alloc, mir_alloc_mut, and mir_points_to #1916

Merged

RyanGlScott mentioned this issue Aug 30, 2023

mir_array_value #1925

Merged

RyanGlScott mentioned this issue Oct 13, 2023

mir_unsafe_assume_spec #1959

Merged

RyanGlScott mentioned this issue Nov 27, 2023

MIR enums #1991

Merged

RyanGlScott closed this as completed Dec 19, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support Rust verification in SAW via `crucible-mir` #1859

Support Rust verification in SAW via `crucible-mir` #1859

RyanGlScott commented Apr 18, 2023 •

edited

Loading

RyanGlScott commented Dec 19, 2023

Support Rust verification in SAW via crucible-mir #1859

Support Rust verification in SAW via crucible-mir #1859

Comments

RyanGlScott commented Apr 18, 2023 • edited Loading

RyanGlScott commented Dec 19, 2023

Support Rust verification in SAW via `crucible-mir` #1859

Support Rust verification in SAW via `crucible-mir` #1859

RyanGlScott commented Apr 18, 2023 •

edited

Loading