- Funding - 

 - Context -

 

This project is one stream in a larger effort that seeks to leverage

distributed compute infrastructure to drastically improve the runtime

efficiency and scalability of Boolean SAT(isfiability) solving, an in

particular SAT solving for transition system models.

 

 - Our first objective is to develop and showcase novel parallel

   approaches that are demonstrated, both theoretically and

   empirically, to be convincingly faster (walltime) than

   state-of-the-art serial procedures.

 

 - Our second objective is to develop and showcase novel parallel

   approaches that are able to efficiently solve problems whose {\em

   Conjunctive Normal Form} (CNF) is very large -- e.g., billions of

   clauses.

 

We are guided by bottlenecks in SAT solving for the following application domains:

 

 

 - Program analysis via symbolic execution; e.g. [1]

 

 - The cryptanalysis of hash functions; e.g. [2]

 

 - Analysis of security properties, and in particular privacy properties; e.g. [3]

 

 

 - Project : High-Performance Computing Workstream -

 

Our application focus shall be domains where the underlying decision

problems are most naturally modelled as state transition systems. We

expect to achieve our objectives through careful scientific

investigation of high-performance computing technologies for the

efficient and targeted discovery and communication of information

between the processing elements in a distributed search. 

 

 - Background - 

 

There are two paradigms for solving Boolean SAT problems using serial

processing: (i) stochastic local search (SLS), or otherwise (ii) a

backtracking search, such as conflict-driven clause learning (CDCL). Both

have their merits, and we note that the latter is recently considered

to be best suited, in isolation, to solving transition system

problems. Although it is somewhat debatable, most sane researchers

would say these techniques have yet to be coupled nicely.

 

Parallel computation has found a number of uses in solving SAT

problems. Parallelism can be exploited in: (i) the tuning of algorithm

configurations, (ii) search-space splitting, and (iii) portfolio

approaches. Identifying and sharing good constraints is key to

efficient parallelism. We note that bottlenecks have been identified

in the structure of resolution refutations which place hard limits on

parallelism in search-space splitting for CDCL solvers. Finally, once

we start solving bounded model checking (BMC) problems--as we expect

to do in this project--parallelisation is raised as a topic when

considering the search horizon at which to pose queries.

 

A fundamental process in any state-of-the-art symbolic execution tool

is the translation/compilation of queries to decision problems, and

then a call to a satisfiability/decision procedure which is used to

resolve the query. Mayhem and angr use the SAT (Modulo Theory) system

Z3. S2E supports a number of solvers, including Z3, that is to our

knowledge used most frequently for industry-strength solving. We note

that the open source (MIT License) Z3 tool itself implements a bespoke

serial Boolean satisfiability procedure to solve hard decision

problems. The focus of this project shall be on developing efficient

parallelisation strategies, for variable selection, value selection,

and constraint propagation in the decision engine that underlies an

effective symbolic execution toolchain.

 

 - Bibliography - 

 

[1] Baldoni, R., Coppa, E., D’Elia, D. C., Demetrescu, C., & Finocchi, I. (2018). A survey of symbolic execution techniques. ACM Comput. Surv., 51(3).

 

[2] Mironov, I., & Zhang, L. (2006). Applications of sat solvers to cryptanalysis of hash functions. IACR Cryptology ePrint Archive.

 

[3] Cortier, V., Dallon, A., & Delaune, S. (2017). SAT-equiv: An efficient tool for equivalence properties. In 30th IEEE computer security foundations symposium, CSF 2017, santa barbara, ca, usa, august 21-25, 2017 (pp. 481–494).