Hacker News Reader

I found two remotely exploitable 0days in the Erlang VM with the use of a SAT solver.

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.

View on HN

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.

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.

That's really neat, do you have a writeup?

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 .

What I really want is scanning my own codebase for problems.

Reply on news.ycombinator.com