I saw the term of opaque predicates several times in obfuscation papers. As far as I understand it, it refers to predicates that are hard to evaluate in an automated manner. Placing it at strategical points of the program (jmp, test, ...) can mislead the analysis of a program by automatic tools.My definition is lacking of precision and, moreover, I have no idea on how to estimate the opacity of such a predicate (its efficiency). So, can somebody give a proper definition and maybe a few examples ?
What is an opaque predicate?
obfuscation
The answers already in this thread are good ones.  In a nutshell, an opaque predicate is something that a program analysis might miss, if the program analysis is not sophisticated enough.  Denis' example was based on the inverse of constant propagation, and served as an anti-checksum mechanism.  Joxean's SetErrorMode example was an environment-based opaque predicate that was used for dynamic anti-emulation.  Two of Ange's answers were also dynamic anti-emulation; based upon the environment, and based upon uncommon platform features.  Ange's other example was more like an anti-disassembly trick via indirect addressing.In the academic literature, an opaque predicate is referred to as a branch that always executes in one direction, which is known to the creator of the program, and which is unknown a priori to the analyzer.  The notion of hardness of an opaque predicate is deliberately omitted from this definition.  Academic predicates are often based upon number-theoretic constructions, aliasing relationships, recursive data structures; basically anything that is commonly understood by program analysis researchers to cause problems for a program analysis tool.  My favorite researcher Mila Dalla Preda has shown that the ability for an abstract interpreter to break a given category of opaque predicate is related to the completeness of the domain with respect to the property tested by the predicate.  She demonstrates by using mod-k-based opaque predicates, and elicits a family of domains that are complete (i.e. incur no abstract precision loss) for mod-k with respect to common transformers (addition, multiplication, etc).  Then she explores the use of obscure theoretical constructions such as completeness refinement to automatically construct a domain for breaking a certain category of predicate.  See this paper for more details.