5 ms·

SAT solving SHA256 is a dead end - I was researching this for the purpose of Bitcoin mining (before this article came out), along with many others, for profit.

SAT solving SHA256 is a dead end - I was researching this for the purpose of Bitcoin mining (before this article came out), along with many others, for profit. SAT solving typically relies on reducing a function down to boolean expressions where clauses are minimally connected with AND operations (a.k.a. Conjunctive Normal Form). The math basis for this is that in GF2 (Galois Field 2 - a number system with only 2 values): AND is equivalent to Multiply (1 * 1 = 1; 1 * 0 = 0, etc.) XOR is equivalent to Addition (1 + 1 = 0; 0 + 1 = 1, etc.) This is useful because we can re-express a boolean function as multiplication and addition for complexity analysis. The difficulty comes when you mix AND and XORs; take the Ch function within SHA256 - Ch(E, F, G) == (E & F) | (~E & G) Which can be rewritten as: Ch(E, F, G) == (((F ^ G) & E) ^ F) Rewritten in GF2 it is equivalent to: Ch(E, F, G) == ((F + G) * E) + F Because of distributive laws, we know there is zero way to simplify this further. Its trivial to see that to work backwards, you have to "consider" way more input combinations for every known output. Even if the output is 0 (which you want when Bitcoin mining), you have this problem where there are 4 possible input combinations. Now unroll the entire SHA256d function Bitcoin uses and you realize the effort to work backwards is far more than the effort to brute-force the input keyspace. This explosion in complexity comes from the fact that the whole function feeds forward, so there is little that can be done to "resolve out" intermediate values as there are no cyclic value dependencies. SHA256d is effectively a giant rat's nest of multiplies and adds, all stacked on top of each other, that cannot be reduced, due to distributive laws.

ITwitchToo 12y ago
I would like to respectfully disagree. I think you're simplifying the reason too much. I don't think it's the Ch function itself (and the rest of the compression function) that causes problems for the SAT solver. I think it's the combination of the compression function and the message schedule that does it. If the message schedule had just been free variables (or simple repetitions of the message), I'm pretty sure the SAT solver would be able to unwind the compression function just fine. The problem is the interaction between the message schedule and the compression function; once you commit to a value in some round of the compression function, you actually impose a set of constraints on the message schedule for all the other rounds simultaneously. So in a way, committing to a value in some round of the compression function means you're also indirectly influencing the possible values in every other round too. It creates this weird sort of dependency between the rounds which wouldn't exist if you only had a long series of Ch functions.
- optimiz3 12y ago
  This only works when feeding the data forward. When SAT-solving (i.e. working backwards), each clause has multiple possible inputs, meaning there is nothing to resolve away.
  - ITwitchToo 12y ago
    When you say "clause", do you mean a disjunction of literals in propositional logic? Because if so, I don't understand what you mean. Clauses don't have inputs. And when you say "resolve away", do you mean applying the resolution rule?
a-dub 12y ago
I recently (naively) dug into it to try and understand where it's magic comes from. I was under the impression that it also gets strength by flipping back and forth between F2 and Z+. Where AND and XOR are linear in F2, they're nonsense in Z+, where addition in Z+ is nonsense in F2 (not to forget the whole mod 2^32 part). Is that actually true or did I just bs myself?
- pbsd 12y ago
  You are correct: overlapping those two incompatible algebras is the main source of nonlinearity in SHA-256.
- optimiz3 12y ago
  Yes, we don't have good ways to unify the flipping between GF32 and GF2 beyond down-converting to GF2 (which yields a massive increase in clause-complexity). GF32 addition in GF2 basically looks like a giant ripple-carry-adder.
  - zvrba 12y ago
    > GF32 addition in GF2 basically looks like a giant ripple-carry-adder. I tried to implement addition in GF32 through Kogge-Stone adder because the dependency chain has length 5 instead of 32. No success. The intermediate variables got so complex that the BDD library I used at the time couldn't even synthesize the expression for a 32-bit adder.

ITwitchToo 12y ago

I would like to respectfully disagree. I think you're simplifying the reason too much. I don't think it's the Ch function itself (and the rest of the compression function) that causes problems for the SAT solver. I think it's the combination of the compression function and the message schedule that does it. If the message schedule had just been free variables (or simple repetitions of the message), I'm pretty sure the SAT solver would be able to unwind the compression function just fine. The problem is the interaction between the message schedule and the compression function; once you commit to a value in some round of the compression function, you actually impose a set of constraints on the message schedule for all the other rounds simultaneously. So in a way, committing to a value in some round of the compression function means you're also indirectly influencing the possible values in every other round too. It creates this weird sort of dependency between the rounds which wouldn't exist if you only had a long series of Ch functions.

optimiz3 12y ago
This only works when feeding the data forward. When SAT-solving (i.e. working backwards), each clause has multiple possible inputs, meaning there is nothing to resolve away.
- ITwitchToo 12y ago
  When you say "clause", do you mean a disjunction of literals in propositional logic? Because if so, I don't understand what you mean. Clauses don't have inputs. And when you say "resolve away", do you mean applying the resolution rule?

a-dub 12y ago

I recently (naively) dug into it to try and understand where it's magic comes from. I was under the impression that it also gets strength by flipping back and forth between F2 and Z+. Where AND and XOR are linear in F2, they're nonsense in Z+, where addition in Z+ is nonsense in F2 (not to forget the whole mod 2^32 part). Is that actually true or did I just bs myself?

pbsd 12y ago
You are correct: overlapping those two incompatible algebras is the main source of nonlinearity in SHA-256.
optimiz3 12y ago
Yes, we don't have good ways to unify the flipping between GF32 and GF2 beyond down-converting to GF2 (which yields a massive increase in clause-complexity). GF32 addition in GF2 basically looks like a giant ripple-carry-adder.
- zvrba 12y ago
  > GF32 addition in GF2 basically looks like a giant ripple-carry-adder. I tried to implement addition in GF32 through Kogge-Stone adder because the dependency chain has length 5 instead of 32. No success. The intermediate variables got so complex that the BDD library I used at the time couldn't even synthesize the expression for a 32-bit adder.