Crypto benchmark and proof orchestration questions

[weaversa]

I translated a Cryptol spec for AES-128 into Rust, being as verbatim as I could (project available here). I also wrote a bunch of concrete tests and Kani proofs(mostly to get a handle on Kani). I found Kani very easy to install and use, so thanks there!

However, Kani fails (takes longer than I'm willing to wait) pretty early on in the suite of proofs necessary to verify functional inversion properties of AES. I've read through the documentation and I'm not seeing any way to assist Kani in solving these proofs. Are there ways for a user to orchestrate the proofs a tad (e.g. switch to a different SAT/SMT solver, serialize the proofs for offline solving, provide hints or reuse work done in previous kani::proof statements (following the hierarchical nature of code) to reduce future kani::proof statements, and so on)?

[zhassan-aws]

Hi @weaversa. Thanks for trying out Kani!

We do not yet have documentation on strategies for addressing non-terminating cases or ones with long run times. But here are a few strategies you can try:

1. You can swap out the default SAT solver (MiniSat) by another one, e.g. Kissat by running Kani with --enable-unstable --cbmc-args --external-sat-solver </path/to/sat-solver-executable>, e.g.

   cargo kani --enable-unstable --cbmc-args --external-sat-solver kissat

2. If your main focus is on proving assertions in your code, you can turn off some of the additional checks by running with --no-memory-safety-checks --no-overflow-checks.
3. You can abstract certain functions that are difficult for the solver to reason about (e.g. ones that heavily use arithmetic) if they're not relevant for the proofs, by replacing them with another version that returns kani::any().
4. You can break up some of the proofs by using case splitting and checking each case individually.

I hope that helps.

[weaversa]

Thank you @zhassan-aws. I tried using kissat to no avail. I'm surprised that this proof is giving you trouble - when proving this property w/ other tools that maintain more structure (SMT (z3) or AIG-based (abc) as opposed to CNF), the proof goes through in seconds. Does your symbolic execution framework extend to other backends (aside from CBMC)?

You can abstract certain functions that are difficult for the solver to reason about (e.g. ones that heavily use arithmetic) if they're not relevant for the proofs, by replacing them with another version that returns kani::any().

While I appreciate the power to hand-rejigger my code to attempt to make a proof go through, if I want to prove a theorem I'd use a theorem prover -- what I want from an assurance tool is to levy invariants (via some CI system) on production code. To that effect, more orchestration capabilities for individual Kani proofs would be appreciated. For instance, I would like to be able to provide a list of function names to uninterpret (EUF) in a particular proof (e.g. kani::uninterpret([function1, function2]), I'd like to be able to choose a solver per proof, rather than globally (kani::cbmc_solve_with("kissat"), and I'd like Kani to be able to use other Kani proofs as lemmas, among many other things.

Do you provide a roadmap of where the project is headed?

[adpaco-aws]

Hi @weaversa, thank you for your input! This is really useful for us.

Unfortunately, we don’t use any other backends at the moment other than CBMC. We’re experimenting now with alternative backends and we may add them in the future (for example, #640), but some work needs to be done before we can enable that. Adding more attributes in order to specify proof attributes (such as the solver) is something we’re also considering.

We don’t have a public roadmap, but we’re starting to move our discussions to GitHub issues (i.e., RFCs). Please don’t hesitate to comment on them.

[weaversa]

@adpaco-aws thanks to you and @zhassan-aws for answering my questions and helping me get a better understanding of your awesome tool. I'll close this issue and follow along as you introduce new features -- are you familiar with Github Discussions? It is (I think) a nicer way than Issues to collect ideas on future directions.

[weaversa]

I tried the same proofs w/ crux-mir and made it two proofs farther than with your kani. I presume this is due to SMT solvers (word-level reasoning) being more powerful than SAT solvers (bit-level reasoning) on this benchmark.

If anything, this experiment is evidence for kani to support more backends -- connections to automated reasoning tools that can exploit word-level operations and hierarchical program structure (such as rewriting logics as well as AIG and SMT-based solvers), among others.