The task is forcer bitcoin find a nonce which, as part of the bitcoin block header, hashes below a certain value. This is a brute force approach to something-like-a preimage attack on SHA-256. The process of mining consists of finding an input to a cryptographic hash function which hashes below or equal to a fixed target value. In this article I propose an alternative mining algorithm which does not perform a brute force search but instead attacks this problem using a number of tools used in the program verification domain to find bugs or prove properties of programs, see as example .
Namely, a model checker backed by a SAT solver are used to find the correct nonce or prove the absence of a valid nonce. The proposed algorithm potentially gets more efficient with increasing bitcoin difficulty. This is not the first time SAT solvers are used to analyse a cryptographic hash. However, to the best of my knowledge, this is the first description of an application of SAT solving to bitcoin mining.
I do not claim that it is a faster approach than brute force, however it is at least theoretically more appealing. To aid understanding, I will introduce some basic ideas behind SAT solving and model checking. Please see the references for a better introduction to SAT solving and bounded model checking . As easy as it may sound, it is one of the hard, outstanding problems in computer science to efficiently answer this decision problem. There is a large and thriving community around building algorithms which solve this problem for hard formulas. A CNF formula, which is the input to a SAT solver, is made up of literals and clauses.
A literal is simply a variable or its negation. DPLL then consists of a depth-first search of all possible variable assignments by picking an unassigned variable, inferring values of further variables which logically must follow from the current assignment, and resolving potential conflicts in the variable assignments by backtracking. As visible in the figure, the property which should be checked for violations is expressed as an assertion. Bitcoin mining using SAT Solving and Model Checking Using the above tools we can attack the bitcoin mining problem very differently to brute force.
This C file is going to be the input to CBMC. Let’s explain these ideas in more detail. The nonce Instead of a loop that continuously increases the nonce, we declare the nonce as a non-deterministic value. This is a way of abstracting the model. We could do the same and just translate this function straight to CNF, however there is a much better and more declarative solution than that in our case. Instead, we can just assume values which we know are fixed in the output of the hash. It might seem unintuitive to “fix” output variables to certain values, however remember that the code is not executed in a regular fashion but translated as a big formula of constraints.
Assumptions on the outputs will result in restrictions of the input — in our case this means only valid nonces will be considered. This serves three purposes: it encodes the specification of a valid hash, it drives the symbolic execution only along paths which we are actually interested in, and most importantly it cuts down the CNF formula. Again, in comparison, brute force just blindly computes hashes with no way of specifying what we are looking for. The SAT-based solution only computes hashes that comply with the mining specification of a valid hash. The Assertion The most important part is defining the assertion, or the property P as it is called in the section above. The key idea here is that the counterexample produced by the model checker will contain a valid nonce given a clever enough assertion.
A bounded model checker is primarily a bug finding tool. That is why the P above is negated in the formula. Thus, the invariant, our P, is set to “No valid nonce exists”. Which the model checker will encode to its negation as “a valid nonce does exist”, i.