wasmtime / PR #7165 Skeleton and initial support for proo... · git-wasmtime

Stream: git-wasmtime

Topic: wasmtime / PR #7165 Skeleton and initial support for proo...

Wasmtime GitHub notifications bot (Oct 06 2023 at 00:03):

cfallin opened PR #7165 from cfallin:pcc to bytecodealliance:main:

This PR adds basic support for "facts" to annotate SSA values and VCode VRegs. The idea is that these facts describe properties of the values -- currently, "in a given range" or "points to valid memory of a given size" -- and by validating a chain of facts along the whole derivation of an accessed memory address, we can verify that the memory access is safe.

This is the start of work on the ideas described in #6090. It is a new approach that subsumes/replaces "VeriWasm": it replaces the post-hoc derive-all-facts analysis approach (which is slow and brittle) with a cooperative approach in which the codegen frontend generates a "proof witness" of sorts, we preserve that, and we check that in the machine code (actually the pre-regalloc VCode, and then we can use the regalloc's symbolic checker to obtain the same guarantee).

Right now, this includes (i) the "fact" data structures, (ii) support for parsing these facts in CLIF and dumping them back out, (iii) propagation of facts from CLIF to VCode, when no optimization is enabled, and (iv) validation of a few basic facts in VCode for the AArch64 backend. Everything else is still TODO and will come in further PRs.

Right now, this is sufficient to take the CLIF
test compile
set enable_pcc=true
target aarch64

function %simple1(i64 vmctx, i32) -> i8 {
block0(v0 ! points_to(0x1_0000_0000): i64, v1 ! max(32, 0xffff_ffff): i32):
    v2 ! max(64, 0xffff_ffff) = uextend.i64 v1
    v3 ! points_to(0x1) = iadd.i64 v0, v2
    v4 = load.i8 safe v3
    return v4
}
where the v0 ! fact syntax annotates v0 with a fact, and validate that the load is in fact safe. The safe memory-flag forces this check; if the points_to range is shrunk, or v1 is changed to an i64 and its max range is increased, this code will fail to compile with
 ERROR cranelift_filetests::concurrent > FAIL: compile
FAIL cranelift/filetests/filetests/pcc/simple.clif: compile

Caused by:
    Proof-carrying-code validation error: MissingFact
The idea is to continue further work along these lines:

Add support for validating facts produced by aarch64 add, shift, ... instructions -- whatever is used in basic address generation.

Add support for validating amode usage in x64 as well.

Propagate facts through the egraph layer so they are preserved during optimization.

Add a richer points_to language for facts to describe what they point to, so a load of a memory base address (for example) from vmctx yields another value with an attached fact (points to a region of this size...). These are the "memory capabilities" described in #6090.

Emit facts on vmctx and on memory-access sequences generated by cranelift-wasm, and add the safe flag to loads/stores wherever possible. At this point, we should be able to validate single- and multi-memory Wasm modules with static memory configurations.

Add support for annotations on bounds-check logic. After this, we should be able to validate dynamic memories, and table accesses as well.

Finally, add a "strong enforcing" mode that disallows all non-safe loads/stores, and add whatever memory-capability info is needed so that, e.g., loads of func pointers, VM state, and everything else from vmctx is covered.

After my initial exploration and ideas in #6090, these ideas were further discussed with @fitzgen, @elliottt, @jameysharp, and others; and a large part of this PR was

Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>

Wasmtime GitHub notifications bot (Oct 06 2023 at 00:03):

cfallin requested elliottt for a review on PR #7165.

Wasmtime GitHub notifications bot (Oct 06 2023 at 00:03):

cfallin requested wasmtime-compiler-reviewers for a review on PR #7165.

Wasmtime GitHub notifications bot (Oct 06 2023 at 00:03):

cfallin requested wasmtime-core-reviewers for a review on PR #7165.

Wasmtime GitHub notifications bot (Oct 06 2023 at 00:03):

cfallin requested fitzgen for a review on PR #7165.

Wasmtime GitHub notifications bot (Oct 06 2023 at 00:46):

cfallin updated PR #7165.

Wasmtime GitHub notifications bot (Oct 06 2023 at 16:38):

cfallin updated PR #7165.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen submitted PR review:

Very excited for this! r=me with comments, some of which can be deferred to follow up PRs.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen submitted PR review:

Very excited for this! r=me with comments, some of which can be deferred to follow up PRs.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Function arguments and global values, eventually, since heap bases and bounds and things are typically global values.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

typo: to communicate intent

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

I would assume that if a load is safe, it does not need to be checked, because it is, after all, safe.

Maybe we can rename this to "sandboxed" or something?

It is unfortunate that we already use "trusted" and "untrusted" for something slightly different...

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Would be nice to attach a string to this variant so we know what is unimplemented.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Is this whether self subsumes other or the other way around? Should document.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

I think we might actually be able to avoid this for a while, at the cost of making loading bases and such from the vmctx axiomatic. Heap bases are always global values (that get translated into vmctx accesses when ) and if we allow frontends to attach facts directly to global values, then we don't need a grammar for describing the vmctx layout. So this would mean that loading heap bases out of the vmctx would become trusted and unchecked (note that the vmctx layout itself would always be trusted) but this seems like a fine intermediate stepping stone and actually maybe even a reasonable trade off to keep long term.

Does that make sense? I feel like this description was a little all over the place.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

And otherwise we could set it to bit_width::MAX -- any reason we shouldn't do that and returning None instead is preferred?

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Rather than putting this as a method on Fact, it might be cleaner to factor out a context and put the method there (along with the extend method, check methods, and future methods):

a.binop(b) always reads kinda subpar to me

the context can hold constant-for-the-extent-of-fact-checking data like pointer width, so we are threading less arguments everywhere

This would essentially give us
// old
let c = a.add(b, add_width, pointer_width)

// new
let c = ctx.add(a, b, add_width);
which I think looks a lot nicer.

Doesn't need to happen in this PR of course, but I just point it out since you refactored this method to be an instance method rather than a static method and I don't think that is actually nicer. Hopefully we both like the context version better :)

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Stylistic nitpick: I'd personally either name computed_region just region so we can use short-hand struct literal syntax for the field, or even inline the variable into the struct literal field.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

It is sort of already defined by the fact we are using a u64 for max, but it might be good to reiterate that we are interpreting values as unsigned here.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Ditto regarding unsignedness.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

This is essentially add but with a signed offset, right? Can we name it accordingly and/or have it call out to add after the check for negative offsets?

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Wait why is it okay to unwrap here? Shouldn't this use ? to propagate?

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Ditto regarding unwrap.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Integer conversions a tricky and as can be a footgun; let's future proof:
                let max = max.checked_mul(u64::from(factor))?;

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Maybe name this check_vcode_facts to leave the door open for check_clif_facts as well?

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

At the top of this function is where we would create the PccContext thing I mentioned earlier that factors out pointer width (and eventually other stuff) and has the add method etc...

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

On this topic: it might be worth drawing out a diagram of our lattice in the docs for Fact or something and a note about what our representation is for the things where it isn't obvious (top/bottom). Something like:
///                None
///               /     \
///              /       \
///             /         \
///     Some(ValueMax)  Some(PointsTo)
///             \         /
///              \       /
///               \     /
///            Err(PccError)
///
/// * The top of the lattice, representing any value, is `None`.
///
/// * The bottom of the lattice, representing the lack of any (valid)
///   value, is an error.
///
/// * The intermediate values are either a maximum bound on the value,
///   or that the value is a pointer to a memory region. Various
///   arithmetic operations are valid on various combinations of these
///   facts. Adding two `MaxValue`s will produce a new `MaxValue` with
///   a maximum of the sum of the parts' maximums. Adding a `MaxValue`
///   to a `PointsTo` will produce a new `PointsTo` that is pointing
///   to a smaller memory region. Etc...
Although, now that I think about it, I don't think this is even really a lattic? Maybe a semi-lattice. I don't think we have both a bottom and a top... I guess the real bottom would be "no value" for dead code, but we don't really have that given that we aren't propagating facts ourselves, merely checking them.

And I guess I would expect None to represent "no value" rather than "any value" so maybe that is why I am hung up on this None stuff.

I don't know, again this comment is all over the place and rambly and doesn't have a real concrete suggestion.

What do you think?

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:49):

fitzgen created PR review comment:

Again: is it better to return None than to do a saturating multiplication? I honestly don't know. But if we are using None for "any value" then this essentially means that we have two representations for "any value": None and Some(Fact::ValueMax { max: u64::MAX }).

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:50):

fitzgen submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 19:50):

fitzgen created PR review comment:

Checked vs unchecked maybe? So you set the unchecked bitflag to opt out of PCC checking.

Wasmtime GitHub notifications bot (Oct 06 2023 at 20:47):

jameysharp submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 20:47):

jameysharp created PR review comment:

I too had wondered if we could making global-value assertions axiomatic to avoid a richer assertion language so I'm glad you asked. I can definitely see downsides but it seems nice as a starting point.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:02):

cfallin updated PR #7165.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:03):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:03):

cfallin created PR review comment:

Ah, yeah, I like the "checked" terminology. I'll go with checked for now (with "unchecked" being the default) for backwards compatibility.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin updated PR #7165.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Added!

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Fixed!

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

I've thought about this for a bit too; I think I'd still like to try actually describing memory layout (and I have some thoughts on how to do it while keeping Fact cheap with shared "memcaps" that are shared across the func). The basic reason is to avoid growing the trusted base. If we provide an axiom on what the loaded value from vmctx is, then we're trusting that load to match what we've stated; but the load-generation machinery is exactly what we're trying to verify with all of this in the first place. Now, arbitrary program logic may create more complex conditions / isel cases than a controlled vmctx case, but maybe not; in either case, I'd rather have the machine load instructions actually verified.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

I opted to split it out into UnimplementedBackend and UnimplementedInst -- slight preference for programmatic errors rather than strings (which preclude any sort of parsing and make test asserts harder). Hopefully that gets the spirit of this at least, noting what's unimplemented :-)

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Made doc comment clearer!

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Done!

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Done!

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Yep, good point, added.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Done!

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Done!

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Done; this method will return a Some(..) in any case we have a ValueMax, and at worst return the range of the given bitwidth.

Re: None -- I guess the way I think about it is that "we have no fact" (in the same way that the facts attached to values are an array of Option<Fact>) -- we just can't say/derive anything. I'm not sure I want to describe this in terms of a (semi-)lattice as we don't have a meet-operation anywhere, and that's pretty intentional -- we aren't doing any fixpoint analysis or inference, we just check what's given. (I guess subsumption technically induces a partial order and a least-upper-bound might exist, but...)

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

Good point; now this returns the "minimal fact" (the range of the whole bitwidth) instead if this overflows.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin submitted PR review.

Wasmtime GitHub notifications bot (Oct 06 2023 at 21:42):

cfallin created PR review comment:

I had thought of that initially, but the difference here is that it's an add-with-constant, and we don't have a Const (known exact value) in our facts (yet?). I didn't want to complicate things by adding that and working out all the details. I agree this would be a nice simplification if we do go there eventually!