Re:Modern SAT solvers: fast, neat and underused
by bloomer on Sunday May 19, 2019 @11:22PM
(#19957301)
DO you have a quick explanation or any reference on using SAT solver to find equivalent bit-wise functions? I can see how you could easily verify equivalence, but I am struggling to see how you could use SAT solver to generate alternate functions using bit-wise operators.
Re:Modern SAT solvers: fast, neat and underused
by ZephyrP on Monday May 20, 2019 @01:05AM
(#19957681)
When considering a small number of possible operations, I've found the optimum way to work this is to simply enumerate all binary expression trees of increasing length and determine if some valid assignment exists for any of them.
Re:Modern SAT solvers: fast, neat and underused
by im3w1l on Sunday May 19, 2019 @06:17PM
(#19955888)
That's really neat, do you have a writeup?
Re:Modern SAT solvers: fast, neat and underused
by ZephyrP on Sunday May 19, 2019 @06:31PM
(#19955959)
This is a description of what lead to it: https://www.reddit.com/r/ReverseEngineering/comments/5h23u3/...
If you want more information about the vulnerability and mechanisms of exploiting it, project members assigned it CVE-2016-10253 .
They can trivially break lots of hash algorithms. You can also find bitwise equivalents to functions which you wouldn't naturally expect to be easily definable in terms of bitwise operations. You can extend existing concepts with a lot of extraordinary new functionality.