Tauchain: CSPs and Finite Domain Constraint Solvers

CSPs are constraint satisfaction problems. This is the sort of problems which can be deifned in such a way that they can be solved by an automated mechanism such as a SAT solver, or SMT solver, or an ASP solver.

These sorts of problems are generally question answer or query or search problems. They are solved by a method which resembles brute force but which is better than brute force because through certain rules and other methods the search space is reduced so that the problem can be solved in less effort. Most probably know the common example of Sudoku solver which is something a finite domain constraint solver can handle.

Ohad chose to go with BDDs (binary decision diagrams) to enable his solver. We have to remember that it will be a desirable property from a cybersecurity perspective to have code which can be "correct by construction". This is possible when you can use a solver to test out all the expected and required finite states you want your program reach and simply avoid the problematic states. So from a security perspective having the capability to define the program in logic and then automatically construct it is a big deal particularly when you can prove mathematically that certain behaviors which hackers may try to exploit will not be possible.

From the perspective of a hacker for example, I could use a solver to generate a fuzzer. I could for example use an SMT solver for automated test generation. In general, we more behaviors we can test for and rule out, the more flaws in the design of the software we can catch. In my opinion this is one of the areas where Tauchain will be state of the art compared to all other similar projects.

References

Hawkins, P., & Stuckey, P. J. (2006, January). A hybrid BDD and SAT finite domain constraint solver. In International Symposium on Practical Aspects of Declarative Languages (pp. 103-117). Springer, Berlin, Heidelberg.