Add option to restrict vtable function pointers #536

avanhatt · 2021-10-01T21:01:08Z

Description of changes:

RMC can currently take a long time to verify code with lots of virtual function pointer calls (or, never terminate). This is in part because CBMC uses a very general heuristic to reason about function pointers: it assumes any function of the right type signature could be a target. CBMC does allow you to restrict possible function targets via a command line option and auxiliary json file: http://cprover.diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_restrict-function-pointer.html

Note, using this functionality requires this branch of CBMC, diffblue/cbmc#6376, tracking issue to update RMC once that merges: #671

For virtual function pointer through a vtable, we can often do much better than CBMC's default heuristic. In particular, we can virtually guarantee (unless the user transmutes the vtable memory) that a call through a vtable will be one of the trait-defined method for that trait type that we have previously seen in codegen. Because CBMC asserts(false) if the function pointer is not actually within the restricted set, this optimization is sound.

This is especially helpful for drop_in_place destructor calls through a vtable. Many functions have types that match drop since it takes a single self argument and returns unit. In a Firecracker example, we have seen 300+ function targets identified by the default CBMC heuristic for a single virtual drop call, which otherwise renders CBMC verification basically intractable (think: a massive, 300+ arm if block after CBMC performs function pointer elimination).

This PR add a VtableCtx object that build a map from virtual call sites to possible trait-defined method implementations, then writes out the restrictions as a JSON file.

You can invoke this on single Rust files by passing a --restrict-vtables flag to rmc, or on full crates with dependencies by adding the following to your harness script (which should eventually be handled by cargo rmc:

RUST_BACKTRACE=full RUSTFLAGS=" -Z restrict_vtable_fn_ptrs ...
... 
rmc-link-restrictions . <output dir>
...
goto-instrument  --function-pointer-restrictions-file restrictions.json ...

Example:

Say we have two traits that both implement a noise method, Animal and Other. Without the vtable restriction flag, any call to noise and any implicit drop on a dynamic trait object would unroll to every implementation of either trait:

  if(!(var_21.vtable->3 == (int (*)(void *))Sheep::noise))
  {
    if(var_21.vtable->3 == (int (*)(void *))i32::noise)
      goto __CPROVER_DUMP_L11;

    if(var_21.vtable->3 == (int (*)(void *))Cow::noise)
      goto __CPROVER_DUMP_L12;

    __CPROVER_assume(0);
  }

Now, we see each call site only considers the implementations that match that trait type:

// Animal::noise 
  if(!(main_1_function_pointer_call_1 == (int (*)(void *))Sheep::noise))
  {
    if(main_1_function_pointer_call_1 == (int (*)(void *))Cow::noise)
      goto __CPROVER_DUMP_L2;

    /* dereferenced function pointer at must be one of [Sheep::noise, Cow::noise] */
    assert(0);
    __CPROVER_assume(0);
  }
  
// Other::noise
  if(!(main_2_function_pointer_call_1 == (int (*)(void *))i32::noise))
  {
    /* dereferenced function pointer at must be i32::noise */
    assert(0);
    __CPROVER_assume(0);
  }

We also get the benefit of CBMC inserting an assert(0) at the end of the block instead of just an assume(0).

Resolved issues:

Resolves #521

Call-outs:

Using this feature will require this CBMC update to land (which fixes a limitation with command line restriction validation): Use remove-function-pointers code for restricted function pointers diffblue/cbmc#6376.

Testing:

How is this change tested?

Manually improved performance on the Firecracker block device example.

Is this a refactor change?

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

celinval

Is it possible to make this change less CBMC dependent? Split between collecting potential candidates and doing the CBMC translation after that.

avanhatt · 2021-10-01T21:43:31Z

@celinval Agreed on the goal. I tried to keep the totally CBMC-specific logic to within get_virtual_function_restrictions, do you see other place that it would make sense to split off?

celinval · 2021-10-04T22:19:30Z

@avanhatt I was thinking about whether we should split this file: compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

avanhatt · 2021-11-12T00:44:58Z

@celinval many rebases and switching to serde later, this is now ready for re-review! The CBMC specifics are now in an entirely different crate.

compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

danielsn · 2021-10-04T20:19:59Z

compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

+
+    /// Add a given call site for a virtual function, incremementing the call
+    /// site index.
+    fn add_call_site(&mut self, trait_name: String, method: usize, function_location: String) {


This is a lot of things of type "String"

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

danielsn · 2021-11-12T02:09:41Z

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

danielsn · 2021-11-12T02:14:36Z

compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

Is the tostring needed

Not anymore at least

danielsn · 2021-11-12T02:15:53Z

library/rmc_restrictions/src/lib.rs

Interned string

danielsn · 2021-11-12T02:16:19Z

library/rmc_restrictions/src/lib.rs

What is the format of this

It's just the name now, renamed the variable to make clear

danielsn · 2021-11-12T02:20:19Z

src/tools/rmc-link-restrictions/src/main.rs

Is this the right place to put the clone?

danielsn · 2021-11-12T03:06:47Z

compiler/rustc_codegen_rmc/src/codegen/assumptions.rs

we talked about this in a chime sync, this is just the set of assumptions on the type, so returning None is no less safe than unimplemented! but let's us not crash.

Not sure I understand. Can you please add a comment to the code?

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

danielsn · 2021-11-12T03:36:12Z

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

If you intern the string these clones become unnecessary

danielsn · 2021-11-12T03:38:30Z

compiler/rustc_codegen_rmc/src/compiler_interface.rs

Why are we using a serde_json Value instead of the actual struct?

danielsn · 2021-11-12T03:40:40Z

compiler/rustc_codegen_rmc/src/context/goto_ctx.rs

IS this the best name for this flag?

do you like emit_vtable_restrictions better?

danielsn · 2021-11-12T03:56:31Z

src/tools/rmc-link-restrictions/src/main.rs

This comment makes me expect a list of files, not the data from inside them

danielsn · 2021-11-12T03:57:39Z

src/tools/rmc-link-restrictions/src/main.rs

I'd expect linking and serializing to be independent steps?

it's a single call to serde_json::to_value(&output).unwrap() so I don't feel strongly about that, but happy to move if you prefer?

It just feels weird given the function name

danielsn · 2021-11-12T03:58:38Z

src/test/rmc/DynTrait/vtable_restrictions_fail_fixme.rs

Is this guaranteed to be stable?

No, but there is no safe/stable way to mangle the vtable AFAIK, and the test would fail if it were to change.

danielsn · 2021-11-12T04:00:02Z

scripts/cargo-rmc

.restrictions.json

danielsn · 2021-11-12T04:00:59Z

library/rmc_restrictions/src/lib.rs

InternedString

danielsn · 2021-11-12T15:52:12Z

scripts/rmc.py

Why the new whitespace?

We check python formatting with autopep8 on changed files, it inserted the whitepace

Ah didn't realize quite how copious it was, might need to move some of these to doc comments to make it happy

tedinski · 2021-11-12T20:43:20Z

compiler/rustc_session/src/options.rs

Is there a strong reason to even make this a flag? Can we emit these files unconditionally?

The main reasons are that currently emitting restrictions currently (1) requires wrapper functions at ever vtable call, because CBMC uses fragile naming conventions for specifying the function call site, and (2) the restrictions could be incomplete if the Rust code is doing certain types of casts that we don't handle, meaning the restriction set would be too small.

The 3rd even more transient reason is that the CBMC PR has not landed, so restrictions fail on our minimum required CBMC version.

Could we get that broken into an issue, with e.g. links to CBMC issues or PRs we depend on?

This change is awesome, and I'd like to make sure we have a well-lit path to making it the always-on default. e.g. do we know what the "certain types of casts that we don't handle" are, and can we document that?

(This is obviously not a blocker to merging, I just don't want it accidentally dropped or anything!)

danielsn

Approved with comments

danielsn · 2021-11-17T22:41:48Z

compiler/cbmc/src/irep/serialize.rs

    }
 }

+struct InternedStringVisitor;


This should really go with InternedString itself.

danielsn · 2021-11-17T22:42:05Z

Cargo.lock

+version = "0.1.0"
+dependencies = [
+ "rmc_restrictions",
+ "rustc_data_structures",


What are we using from here?

The compiler's FxHashMap, not strictly necessary/could be replaced with a vanilla HashMap

If easy, could do that here; if not, lets just do that as a cleanup PR

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

compiler/rustc_codegen_rmc/src/compiler_interface.rs

compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

danielsn · 2021-11-17T22:51:18Z

compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

+    ) {
+        assert!(self.emit_vtable_restrictions);
+        let site = CallSite {
+            trait_method: TraitDefinedMethod { trait_name: trait_name, vtable_idx: method },


don't need to say trait_name: trait_name, trait_name would do

danielsn · 2021-11-17T22:52:11Z

compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

+        )
+        .into();
+
+        // We only have the Gotoc type, we need to normalize to match the MIR type.


Is there any risk here if MIR changes?

Less so now that we have the type_map, we are normalizing the MIR on both sides instead of relying on string editing.

danielsn · 2021-11-24T20:15:48Z

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

+                    )
+                    .as_stmt(Location::none());
+
+                // Declare symbol for the single, self parameter


Not for this PR, but this feels like something that would happen often enough to be worth a helper function

danielsn · 2021-11-24T20:19:55Z

compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

+        let key = TraitDefinedMethod { trait_name, vtable_idx: method };
+
+        if let Some(possibilities) = self.possible_methods.get_mut(&key) {
+            possibilities.push(imp);


Is there any reason we might want to keep this list ordered?

Not currently.

danielsn · 2021-11-24T20:20:54Z

compiler/rustc_codegen_rmc/src/context/vtable_ctx.rs

+    }
+
+    /// Add a given call site for a virtual function, incremementing the call
+    /// site index.


Where does it increment the index??

This comment was stale, removed.

compiler/rustc_codegen_rmc/src/compiler_interface.rs

celinval

I haven't finished reviewing this but so far I haven't seen anything critical. Once @danielsn approves this, I'm ok with merging and making the changes as a follow up PR.

Thanks

celinval · 2021-11-22T21:41:52Z

compiler/rustc_codegen_rmc/src/codegen/assumptions.rs

Not sure I understand. Can you please add a comment to the code?

celinval · 2021-11-22T21:43:29Z

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

        if let Some(fn_symbol) = self.symbol_table.lookup(&fn_name) {
+            if self.vtable_ctx.emit_vtable_restrictions {
+                // Add to the possible method names for this trait type
+                self.vtable_ctx.add_possible_method(


I would move the if statement to be inside the add_possible_method() implementation. This will make the code cleaner and less error prone.

celinval · 2021-11-22T21:49:05Z

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

-                .codegen_unimplemented(
-                    format!("drop_in_place for {}", drop_sym_name).as_str(),
-                    Type::empty(),
+            let drop_sym = self.ensure(&drop_sym_name, |ctx, name| {


For the drop case. Would it make more sense for us to replace the function call with the unimplemented assertion instead of generating the function body?

celinval · 2021-11-22T21:51:20Z

compiler/cbmc/src/irep/serialize.rs


+struct InternedStringVisitor;
+
+impl<'de> serde::Deserialize<'de> for InternedString {


Can you please add a unit test for this?

avanhatt · 2021-11-29T18:31:05Z

Will address followups in #671, merging to unblock Ted's linked PR.

Add vtable restriction option, need CBMC PR to use

avanhatt force-pushed the vtable-fn-ptr-restrictions branch from 7f075ae to 400eb8b Compare October 1, 2021 21:02

avanhatt requested a review from danielsn October 1, 2021 21:14

celinval suggested changes Oct 1, 2021

View reviewed changes

avanhatt force-pushed the vtable-fn-ptr-restrictions branch 2 times, most recently from 500fb23 to 9c09cd8 Compare October 20, 2021 17:37

avanhatt marked this pull request as ready for review October 20, 2021 17:38

avanhatt force-pushed the vtable-fn-ptr-restrictions branch from 9c09cd8 to 4b33922 Compare October 29, 2021 16:37

avanhatt force-pushed the vtable-fn-ptr-restrictions branch from fe4fb66 to 4c60685 Compare November 8, 2021 19:42

avanhatt requested a review from a team as a code owner November 11, 2021 15:03

avanhatt force-pushed the vtable-fn-ptr-restrictions branch from ad92aca to 06d823d Compare November 11, 2021 15:10

avanhatt requested a review from celinval November 12, 2021 00:44

danielsn suggested changes Nov 12, 2021

View reviewed changes

danielsn reviewed Nov 12, 2021

View reviewed changes

tedinski reviewed Nov 12, 2021

View reviewed changes

whitespace

19bb530

avanhatt force-pushed the vtable-fn-ptr-restrictions branch from ed04501 to 19bb530 Compare November 17, 2021 18:32

rest of review comments

d55a2be

avanhatt requested a review from danielsn November 17, 2021 20:25

avanhatt added 3 commits November 17, 2021 20:27

Merge branch 'main' into vtable-fn-ptr-restrictions

995322a

whitespace

ed5a30c

typo

91ca00d

danielsn approved these changes Nov 17, 2021

View reviewed changes

avanhatt added 3 commits November 19, 2021 15:48

review comments

0536e87

Merge branch 'main' into vtable-fn-ptr-restrictions

30e1e90

Merge branch 'main' into vtable-fn-ptr-restrictions

fc7ea4d

tedinski mentioned this pull request Nov 24, 2021

Introduce rmc::proof function attribute #668

Merged

4 tasks

danielsn reviewed Nov 24, 2021

View reviewed changes

avanhatt added 2 commits November 29, 2021 16:05

remove stale comment

3c9376a

Merge branch 'main' into vtable-fn-ptr-restrictions

93337d4

celinval reviewed Nov 29, 2021

View reviewed changes

celinval approved these changes Nov 29, 2021

View reviewed changes

avanhatt mentioned this pull request Nov 29, 2021

Update vtable restrictions once CBMC side lands. #671

Open

4 tasks

avanhatt merged commit 7820fa5 into model-checking:main Nov 29, 2021

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022

Add option to restrict vtable function pointers (model-checking#536)

214c431

Add vtable restriction option, need CBMC PR to use

tedinski pushed a commit that referenced this pull request Apr 27, 2022

Add option to restrict vtable function pointers (#536)

6be24b9

Add vtable restriction option, need CBMC PR to use


		struct InternedStringVisitor;

		impl<'de> serde::Deserialize<'de> for InternedString {

Add option to restrict vtable function pointers #536

Add option to restrict vtable function pointers #536

Uh oh!

Conversation

avanhatt commented Oct 1, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

avanhatt commented Oct 1, 2021

Uh oh!

celinval commented Oct 4, 2021

Uh oh!

avanhatt commented Nov 12, 2021

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

avanhatt commented Oct 1, 2021 •

edited

Loading