search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
454 stars 150 forks source link

Formal Verification Tooling - Proposed Improvements #3108

Closed ana-pantilie closed 8 months ago

ana-pantilie commented 1 year ago

This is not only K related, but I didn't know of a better place to currently add this issue.

If you are an auditor who is working on a formal verification engagement (Lukso/Optimism) or if you've had a chance to try out the current formal verification tooling and have ideas, we're looking for your feedback!

Please think about what you found hard about the tooling, what slowed you down, which parts you found hard to understand/work with.

We'd like to hear your ideas about what you would want from a formal verification tool, they can be both big or small ideas, so feel free to brainstorm away!

ChristianoBraga commented 1 year ago

Maybe think about/apply techniques to bring the output of the prover closer to the semantics? (Not only to K.) A pretty printing of sorts...

ChristianoBraga commented 1 year ago

Think about/organize libraries of lemmas useful to each particular echo system?

lucasmt commented 1 year ago

I think it would be helpful for our KEVM engagements if we had better support for reasoning about bit arrays. In my experience it's common for the prover to get stuck in expressions like

maxUInt224 &Int #asWord ( b"a\x00\xacVK\x80t-\xe2\xbf\x82\xac\xb3c\x00\x00" ++ #buf ( 32 , notMaxUInt96 &Int ( X <<Int 96 ) ) ) [ 4 .. 28 ]

where

a) arithmetic reasoning isn't useful because all the operations occur at the bit level b) you're only reasoning about part of a word at a time (for example, bytes 4 to 28) c) you're constantly switching back-and-forth between an integer and byte-array representation (integer for bitwise operations, byte-array for slicing and concatenating)

Expressions like this are common when verifying EVM bytecode. We can write lemmas to deal with these cases, but this requires thinking about the bit-level representation and often converting between decimal, hex and binary, which is confusing, tedious and error-prone. It's also hard to write these lemmas in a generic way. I think the best option would be if this kind of reasoning could be handled by an SMT solver instead.

PetarMax commented 1 year ago

Branching on function rules.

I think that it is essential for verification to be able to branch on function rules in a controlled way. For example, in the Plutus proofs, which involved a higher degree of logical abstraction than KEVM proofs, I needed to be able to branch on one of these logical abstractions (in particular, to case-split on the structure of a list).

I would ideally like an annotation of some kind on function definitions (like a branch attribute) that would indicate to the symbolic engine that the branching on this function definition is possible.

I would also like this branching to be triggered only heuristically, by need (for example, if an execution branches on one of its parameters), and also not more than once per such branching in case of recursive functions. This is similar in feel to having predicates/abstractions in separation logic, with the ability to unfold/fold them.

Baltoli commented 8 months ago

Closing for now as there's not been a meaningful update in a while; can reopen if we need to.