If researcher found satisfiability in any software, this is a threat to security? If answer - "Yes", how can attacker to use SAT?

  • 1
    What quality of SAT suggests that it could be a threat to security? I'm afraid that I do not understand the basis for the question. Can you expand on it? – schroeder Aug 22 '18 at 8:37
  • @schroeder KLEE (klee.github.io/tutorials/testing-function) using black-magic for testing bytecode to symbolic execution + SAT solve, yeah? I not understand - is it just test or what? No security risk? – D1553CT10N Aug 22 '18 at 8:45

The symbolic execution technique, as used in KLEE, is just a way to ask a SAT-solver to validate/invalidate possible runs in the software without executing it for real. It allows to focus on feasible paths only.

So, this will not be a security threat if you can run a SAT-solver and validate/invalidate the paths of your software. I will just mean that you will be able to explore all its execution paths for sure (exhaustively).

It also means that the internal of your software can be fully explored, which might be a problem if you want to hide something (a patented algorithm, a cryptographic key, ...). In such case, people tends to use specific obfuscation techniques (usually specific opaque predicates to defeat SAT-solvers) to render the exploration of all the executable paths more difficult.

Hope this help you to better understand the whole thing.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.