what is the practical uses of this (or SMT in general)? i've read the referenced Wikipedia but still don't understand.
back
7 comments
Solvers are somewhat popular in software security, both for automatically uncovering invariants (and exploitable lack of invariants), and also for modeling program binaries and solving for collections of basic blocks that can executed during a memory corruption attack to accomplish attacker goals.
Things like automatic exploit generation[1] and exploit hardening[2] in particular rely on SMT solvers to accomplish their goals. They allow for some truly remarkable things to be done. Expect skynet to utilize them heavily in its distributed automatic exploit generation (global autopwn) tooling!
1. http://security.ece.cmu.edu/aeg/ 2. http://users.ece.cmu.edu/~ejschwar/bib/schwartz_2011_rop-abs...
Are you familiar on how you can use SAT solvers to solve a wide variety of constraint problems?
https://github.com/hugomg/hexiom
SMT solvers basically extend SAT solvers to allow you to work directly with other theories (linear inequalities, bit arrays, etc) without being forced to encode this as the booloean formulas that basic SAT understand. The idea is that dealing with the higher level details directly instead of having to convert tihngs to a commo low level makes it simpler to express things and can also allow for custumized optimizations and algorithms?
I have only made light contact with SMTs in my explorations but SMT solvers have massive applicability. They're used in theorem proving - verification, dependent typing, contracts - scheduling, planning, and for understanding/modelling cell regulatory networks in biology.
Satisfiability stuff is interesting because it shows that just because something is NP-complete doesn't mean that it is unapproachable or 'hard' (just as linear programming shows just cause something is in P doesn't mean it is 'easy' - for large values of easy). To ground the concept you can roughly categorize it with logic programming, answer set programming, constraint satisfaction and integer programming. I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.
> I've made use of answer set programming for certain planning problems as a kind of better prolog but SMT is a 'bit' more flexible.
I suppose it depends on what you mean by flexible. I would say that ASP is more flexible as a modeling language—you can specify all sorts of logic and constraints in it in a fairly expressive logical formalism, with both generative (Prolog-like) and constraint-oriented (CSP-like) language constructs. Particularly with the extensions the Potassco people have been making in their version: http://potassco.sourceforge.net/
However, current ASP solvers ground to variable-free (propositional) programs before solving, which means they blow up on large-ish integer domains, since you end up propositionalizing the whole integer range. I've had some examples where just grounding out the problem takes ages, but then it's nearly instant to solve once the grounding is done. SMT avoids that by providing a way to ground "modulo" a domain theory, rather than fully grounding, with a theory of integers being a common example.
Awesome response thanks. The increased ease of use for modeling is part of why I decided on it rather than an SMT solver. One should prefer ASP wherever the assumptions hold. I use(d) DLV-Complex but will check your link.
But right, by more flexible I meant the availability of quantifiers in SMT solvers.
They can be used for program synthesis. That is, given some high-level specification, you can use an SMT solver to generate code fitting that specification. You can also use them to verify that some code does fit a specification and, if it doesn't, to find the part of the code causing the actual problem (the minimal unsat core).
A particular example would be to take some existing code with holes (just parts left out) and some assertions about the code's behavior, encode both as logic formulas and try to find a satisfying assignment for the holes. When you have a possible assignment, you can verify it with the same encoding. You can then use the satisfying assignment to fill in the holes in the initial program, which are ideally very tedious to code by hand.
Planning problems can be encoded as SAT problems, for instance.
another example: package dependencies resolution on Linux distributions.
This can far more easily be done by topological sorting.
That's not actually sufficient when you consider version requirements; for example requiring a specific range of libc or the like.
Various forms of program analysis/verification. Some examples of applications where SMT is heavily used are automated theorem provers, symbolic execution engines, model checking tools.