search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 123 forks source link

Bit-size reduction in proofs #1058

Open LeventErkok opened 3 years ago

LeventErkok commented 3 years ago

Just came across this paper:

https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7326550/

which suggests a strategy for proving bit-vector properties of large sizes. The main observation is that the satisfiability of a bit-vector based property surprisingly remains the same even if you alter bit-sizes radically. This can be the basis of tackling Cryptol properties, for instance. (Or even attempt to prove polymorphic bit-vector properties, up-to a given size.)

I wouldn't expect this to work well on things like AES, SHA, etc; where the bit-vector size cannot really be reduced. But everything else that's based on arithmetic might benefit from it.

There's also an "implementation" here: https://github.com/martinjonas/bw-reducing-solver Though I haven't tried it myself; but it might be best to directly support this in the backend solvers. (Or Cryptol can implement its own algorithm based on the paper on top of existing solvers.)

Anyhow, I thought I'd drop this note here as it would be relevant to Cryptol and Sean is either already aware of the paper or might find it interesting otherwise.

weaversa commented 3 years ago

Years ago Bill Legato had an idea for using Newton's p-adic iteration to do proofs of large bit-vectors, and this paper (which I'm just now seeing -- I couldn't attend the SAT conference last year) has some similarities. Thanks for the pointer @LeventErkok , definitely a good technique to consider.