Audit Vtable generation for dynamic traits

model-checking / kani

Kani Rust Verifier

https://model-checking.github.io/kani

Apache License 2.0

2.22k stars 89 forks source link

Audit Vtable generation for dynamic traits #299

Open danielsn opened 3 years ago

danielsn commented 3 years ago

RMC handles dynamic traits by making a vtable for each trait, which maps virtual calls to the function pointer that implements the call. As of 2021-09-01, our implementation of dynamic traits has no known soundness issues.

Likelihood:

Due to the complexity of this feature, there may be currently-unknown soundness issues.

Mitigation:

The default flags RMC passes to CBMC now include --pointer-check, so incorrect codegen of functions is now more likely to be found a verification time.
We have added 40+ regression tests for dynamic traits.

avanhatt commented 3 years ago

Updated description to match current state.

adpaco-aws commented 3 years ago

RMC is now using --pointer-check by default (#263)

avanhatt commented 3 years ago

Updated to reflect that --pointer-check is used by default and that for closures we only fail for boxed closures.

avanhatt commented 3 years ago

Updated to reflect that all known cases of boxed closures now work.

avanhatt commented 3 years ago

As of 2021-09-01, all known soundness issues specific to dynamic traits objects and vtables have been resolved.

However, two issues to note:

In certain cases of trait objects nested automatic reference counted objects, we generate invalid calls to the drop destructor. For now, we maintain soundness here by codegening an unimplemented block, which would cause code that relies on this behavior to fail at verification time: https://github.com/model-checking/rmc/issues/426
We have some test cases with print statements that fail verification, which is likely due to unrelated issues with how we handle print: https://github.com/model-checking/rmc/issues/194