jasongross

What does "out of bounds" mean at the ISA level? By the time you have a binary, you've lost all the information about which memory is which.

But you're right that don't need ASan at all if you've encoded semantically meaningful properties. E.g., if you assert(decompress(compress(x)) == x), proving that you don't crash requires proving that compression round-trips. (Similarly if you have a reference implementation.)

The upshot is that the spec doesn't need to be written in a proof assistant and can instead be encoded as an end-to-end test.

Especially when "this one weird special case" pulls in the entire binary layout because your code has a hole that allows an attacker to jump to a specified address

Yes, but usually the thing that comes out of this process is having less rich types and separating proofs from computation. (Example: working with length-indexed lists in https://github.com/mit-plv/fiat-crypto was a lot more painful for writing cryptographic algorithms than using plain lists and proving length-preservation separately with tactics. Probably because the length is not an inherent part of the algorithm.)

Model: https://github.com/theorem-labs/rocq-linux-process-semantics based on https://github.com/mit-plv/riscv-coq and Sail Binaries are split into sections with a Python script and imported into Rocq with rocq-read-file Workflow: https://theorem.dev/oss-verify/ , https://github.com/theorem-labs/oss-verify , https://github.com/theorem-labs/oss-verify-proofs

You make a compelling argument, but, empirically, when you optimize code for performance, you end up with an unreadable mess that breaks all abstractions; but every time I've substantially optimized a proof for performance [of proof checking], I've ended up with better abstractions and more modularity.

The difference between math and software verification: in math, the convex hull hypothesis implies that you don't go far beyond human capability, because the bottleneck is out of distribution generalization. In software verification, you can verify just about all the software that exists despite the convex hull hypothesis, because the bottleneck is just scale.

There is a tradeoff between the compute required to generate a proof and the compute required to check it. Fully generic methods such as SMT solvers require compute exponential in the number of variables in scope and lines of code in a single function. Breaking the exponential requires (and is perhaps equivalent to) understanding the code in sufficient detail (cf https://arxiv.org/abs/2406.11779). In practice, the computational cost of semi-automated proof generation is a significant bottleneck, cf https://dspace.mit.edu/handle/1721.1/130763?show=full and https://jasongross.github.io/papers/2022-superlinear-slownes... .