I came across this term called "Satisfiability Modulo Theories", which when I Googled it, was something that is related to various theories on low level languages. How does this help in discovering 0-days? I also saw people using something called "Z3 solver" could somebody give a shorter explanation of what this is?

  • Is that theory supposed to help discover 0-days? You do not provide context to your question. Also, I found no reference to "Z3 solver". Could you provide links to sources talking about your topics?
    – schroeder
    Mar 25, 2015 at 17:33
  • 1
    Satisfiability modulo is a CS concept which has nothing to do with 0-days or anything else in security. Z3 is a sat solver which includes some support for modulo theories @schroeder . Mar 25, 2015 at 17:56
  • Santhosh, please re-read tour to understand what is on topic here. So far all your questions have been closed.
    – Rory Alsop
    Mar 25, 2015 at 23:12
  • i know what i am asking syscan.org/index.php/sg/training/details/2015/sys_15_08 This clearly mention something about REIL/VEIX what i needed is a simpler understanding of What is SAT how they can be related to Security Mar 27, 2015 at 16:34

1 Answer 1


Satisfiability Modulo Theories (SMT) are mathematical concepts that looks at how something can be computed. These theories relates to things that you will find in many programming languages like real and integer numbers, lists, etc and which are essential to computers.

SMT solvers (like Z3) are computer programs that automatically generate proofs for related mathematical problems. So, if you have a problem statement (a theorem) that you can encode in the input language for such a solver, the solver will return a proof, if possible.

An application area for SMT solvers is an approach called 'symbolic execution'. In symbolic execution, you are less interested in the actual execution run of a computer program, but to explore what are general executions under different inputs. For example, in an actual computation, you would be interested to get a number as a definitive output. In symbolic execution you would be more interested in more general things like what is the type of the output.

Symbolic execution can be used to perform security analyses like taint checking, i.e., trace an input throughout the execution of a program. This helps to discover all kind of vulnerabilities, including zero-day exploits.

  • i found this quite good for starters it is too bad people close the question when they no idea what i am asking about cacm.acm.org/magazines/2009/8/… Mar 27, 2015 at 16:38
  • Right. Formal methods are helping to develop secure products, but unfortunately this is not common sense. Mar 30, 2015 at 23:54

Not the answer you're looking for? Browse other questions tagged .