If researcher found satisfiability in any software, this is a threat to security? If answer - "Yes", how can attacker to use SAT?
-
1What 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 ♦Commented Aug 22, 2018 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?– 69 420 1970Commented Aug 22, 2018 at 8:45
Add a comment
|
1 Answer
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.
