-1

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?

schroeder
  • 123,438
  • 55
  • 284
  • 319
Santhosh Kumar
  • 25
  • 2
  • 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 '15 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 . – Gilles 'SO- stop being evil' Mar 25 '15 at 17:56
  • Santhosh, please re-read [about] to understand what is on topic here. So far all your questions have been closed. – Rory Alsop Mar 25 '15 at 23:12
  • i know what i am asking https://www.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 – Santhosh Kumar Mar 27 '15 at 16:34

1 Answers1

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.

user2969932
  • 156
  • 4
  • i found this quite good for starters it is too bad people close the question when they no idea what i am asking about http://cacm.acm.org/magazines/2009/8/34498-boolean-satisfiability-from-theoretical-hardness-to-practical-success/fulltext – Santhosh Kumar Mar 27 '15 at 16:38
  • Right. Formal methods are helping to develop secure products, but unfortunately this is not common sense. – user2969932 Mar 30 '15 at 23:54