Maybe I am too old school, but I can't understand how all these fancy 'constraint solvers' (and in another solution, definitions akin to genes and chromosomes (hair raising) https://news.ycombinator.com/item?id=11474613) are helping to write a standard brute-forcer for the flawed algorithm? Are these solvers doing anything more intelligent??
Solvers don't do brute force at all. Otherwise you wouldn't come up with ways to crack crypto. Solvers work with SAT and SMT languages, which means purely logical and extended to simple words and bitarrays, and the solvers mentioned there (cbmc is also in this league), can solve normal programming logic backwards.
Means you assert a result on a variable at the end, specify which variables and states will affect the wanted result, and the framework and solver will efficiently backtrack all the possible solutions of input variables to come up to your desired endstate, by filtering out impossible paths and values. Like in a game.
Z3 is very popular, because you can write your problem in python.
Ages ago lisp was very popular, and some of the very first lisp programs from the 60ies were such solvers (general planner) leading to AI.
And recently with the implementation of efficient simple open-source SMT solvers (minisat, ...) implemented within gcc or llvm you can now even use normal C programs and backtrack results, optimize and check types, do bounds checking, generate tests from bugs and so on. This is not comparable to simple fuzzing or brute-forcing, it knows the program flow, and works the flow backwards.
Thanks for explaining! I just can't understand how such 'solvers' can help with crypto, when strong crypto-algos are not reversible and hence there is no point to approach them backwards?
If any algorithm can be weakened by such 'problem solvers', it wouldn't be considered strong? For instance, can SHA256 be reversed (i.e. collision found) faster with such a solver? I guess not..
I realize that with crypto, solvers can optimize the flow of the algorithm, make it more efficient and omit repeating some code parts, but a good bruteforcer written in assembly can be as optimized..?
SAT solvers can solve logical problems much faster than brute force. They take advantage of heuristics, and they use certain mathematical techniques to rule out parts of the search space and narrow it down significantly.
In general most crypto can't be broken by solvers. The solvers might be faster than brute force, but still take exponential amounts of time to solve it. However if the crypto was designed badly, there can be weaknesses in it that the solvers can find and exploit.
It's basically like those logic puzzles that are sometimes asked to kids. I don't have a specific example handy, but they go like "Fred won't sit next to Bill. Bill wants to sit next to Mary. Mary wants to sit in the same table as Ned..." And then they ask you to find a seating arrangement that satisfies all these constraints.
You can try every possibility, and there are exponentially many as you add more people. But if you are clever, you can realize certain constraints rule out large portions of the search space. Like you know the answer must have Mary in the same table as Ned, so you don't even try any possibilities where that's not true. There are many other clever tricks SAT solvers use to shrink the search space.
Crypto algorithms are deterministic, and therefore reversible. Solvers would work with any crypto, it's just that with normal crypto your computer would degrade to dust before they had time to finish. This was breakable because the Salsa algorithm was processing 16 bits instead of 32, which makes the set of possible earlier states astronomically smaller.
A "properly" implemented 16 bit Salsa20 would have 64/128 bits of key, which would still take a very long time to break. The reason _this_ implementation was broken (assuming the referenced snippet [1] is accurate) is the rotl function and the rotation values. The shifts are being calculated for 32 bits but are being used with 16 bit values. Instead of all 16 bits being rotated and used, half the shifts result in 0 while the others affect only a handful of high bits, which means there is very little diffusion going on.
I think the misunderstanding is just definitional, if you're searching on a constrained-space it wouldn't be called brute-force, though by all means you are still enumerating possible solutions.
> Brute force search should not be confused with backtracking, where large sets of solutions can be discarded without being explicitly enumerated *
> solver will efficiently backtrack all the possible solutions of input variables to come up to your desired endstate, by filtering out impossible paths and values
That seems to be a contradiction, because Back-Tracking uses Brute-Force. The efficiency comes from heuristics that can fail, which is kind of important to note. SAT problems are in principle np-complete with all the uncertainty that implies.
>And recently with the implementation of efficient simple open-source SMT solvers (minisat, ...) implemented within gcc or llvm you can now even use normal C programs and backtrack results, optimize and check types, do bounds checking, generate tests from bugs and so on.
coq: https://coq.inria.fr/a-short-introduction-to-coq
the real beast out there. easy to install. but hardly usable for normal hackers, because of their mathematical notation.
but it's using plain c, and you can verify c with various solvers.
for crypto https://srlabs.de/minisat-intro/ has some explanation how to break weak ciphers or hashes, knowing the weakness beforehand. but the various hackers posting on their blogs usually have better practical explanations.
