SAT solvers recently have increasingly been used in many applications, including AI, planning, verification, security, and cryptography. Our goal is to enhance SAT solvers for cryptanalysis tasks. Most of the previous SAT-based cryptanalysis works use SAT solvers as black-box, where the problem is encoded into SAT and given to an off-the-shelf SAT solver. The main research question that we work on in this project is how to use a SAT solver in a white-box fashion, i.e. how to tailor the internal components to improve the performance of the solver on the cryptographic instances.
We target the reasoning components of the modern CDCL SAT solvers as well as search heuristic components.
In this work, inspired by the CDCL(T) paradigm, we followed a programmatic SAT approach and extended reasoning components of a CDCL SAT solver (namely propagation and conflict analysis), to improve its runtime in solving cryptographic tasks. We call our framework CDCL(Crypto) (replacing the T in the CDCL(T) with a custom cryptographic reasoning component). The programmatic callbacks in our framework, guide the search in the underlying Boolean domain using higher level information about the problem being solved.
We used this framework in two attacks on cryptographic hash functions. First, we mounted an algebraic fault attack on hardware implementation of SHA-1 and SHA-256 with a programmatic version of MapleSAT and improved state-of-the-art by reducing number of required faults and improving the runtime. Second, we improved the SAT-based differential cryptanalysis of round-reduced versions of SHA-256.
In the context of divide-and-conquer parallel SAT solvers, splitting heuristic is the routine that picks variables and splits the input formula into several smaller sub-formulas. We have developed a machine learning based splitting heuristic using a pairwise ranking method. We extended the divide-and-conquer framework of PaInleSS parallel SAT solver and implemented our heuristic on top of it, and making a tool that we call MaplePainless.
[Paper: CP 2020] [Code]
In this part, we tackled the search heuristic initialization problem, which is how to setup the initial preferred polarity and activity scores for the variables in a Boolean formula. In other words, how to initialize the branching (variable selection + value selection). It is well-known that search initialization can have a big impact on the performance of the solver. We used a Bayesian moment matching based formulation of SAT to derive an initial variable order and value setting that most likely satisfies most of the clauses. Our implementation on top of MapleSAT, MapleCOMSPS, and Glucose, shows promising improvements in solving cryptographic instances.
[Paper: ICML 2020] [Code]
We developed an adaptive restart policy that chooses between uniform, luby and geometric restart policies, in a multi-armed bandit setting, with the target of maximizing the average LBD of the learnt clauses. We implemented our approach on top of MapleSAT and showed considerable improvement in solving SHA-1 preimage instances.