Opaque Predicates

Several transformations rely on boolean and integer expressions that have a known value, known as opaque predicates and expressions. To construct these, data structures with precise invariants are added to the code.

At a minimum, you must create one or more opaque invariant data structures:

OptionArgumentsDescription
--Transform InitOpaque Add opaque initialization code. This initialization code has to be added to a function that gets called before any uses of opaque predicates, usually, but not necessarily, to main.
--InitOpaqueStructs Deprecated spelling of --InitOpaqueInvariantKinds Kept for compatibility. Replace --InitOpaqueStructs=list,array with --InitOpaqueInvariantKinds=structure_state. Replace --InitOpaqueStructs=env with --InitOpaqueInvariantKinds=environment. The input kind was removed in 4.1. Default=none.
--InitOpaqueInvariantKinds identity, modular, mba, structure_state, scalar_state, environment, plugin, * Comma-separated list of the kinds of opaque invariant to set up, named by the hardness family they rest on. These become the default set for any transformation that asks for an opaque without naming kinds of its own. From version 4.1 Default=none.
  • identity = Universally-true arithmetic identities.
  • modular = Residue and modular-arithmetic facts.
  • mba = Mixed boolean-arithmetic.
  • structure_state = A data structure that maintains an invariant as the program runs and is then queried structurally. Replaces pre-4.1 list and array.
  • scalar_state = Evolving scalar state.
  • environment = Opaque expressions from entropy. Requires --InitEntropy. Replaces env.
  • plugin = Invariants supplied by a user plugin.
  • * = Same as identity,modular,mba,structure_state,scalar_state,environment,plugin
--InitOpaqueInvariantResilience trivial, local, global, interprocedural, inter_process, * Comma-separated list of the resilience levels to set up: the scope of analysis an attacker must run to decide the invariant. This is orthogonal to the kind -- a modular fact may be trivial or not, and either way it is still modular.

The default is every level except trivial. Trivial invariants are the ones a C compiler folds to a constant at -O2 Use for educational purposes only. From version 4.1 Default=local,global,interprocedural,inter_process.

  • trivial = One expression decides it, AND a stock compiler at -O2 folds it to a constant.
  • local = One expression decides it, but -O2 does not fold it.
  • global = Deciding it needs analysis of the whole procedure.
  • interprocedural = Deciding it needs whole-program analysis.
  • inter_process = Deciding it needs reasoning about concurrent interleavings. Reserved -- no invariant is at this level yet.
  • * = Every level, trivial included.
--InitOpaqueMaxSize INTSPEC The largest number of sub-opaques a single opaque may be composed of, for any transformation that does not set a --<Transform>MaxSize of its own. See --AddOpaqueMaxSize for what composition buys. From version 4.1 Default=1.
--InitOpaqueList BOOL Print the whole opaque-invariant database -- every invariant's name, kind and resilience -- and continue. Useful for finding the exact names to pass to --<Transform>Select. Refused unless the deity key is supplied with --DeityMode. From version 4.1 Default=false.
--InitOpaqueCount INTSPEC How many opaque data structures (lists or arrays) to add to the program. They will be split roughly evenly between the different declared opaque structures. Default=1.
--InitOpaqueTrace update, use, check Trace opaque structures and values as they are generated during execution. This used to be a boolean, but from version 3.3, it can take on multiple values. Default=NONE.
  • update = Print the generated structure
  • use = Print every use of an opaque value
  • check = Print only if an opaque value is wrong
--InitOpaqueDebug BOOLSPEC If true, then we store all opaque values in a temporary variable. This can help with debugging when looking at the generated code. For example, if you see a variable named _OPAQUE_Array_42_expected_128, it means: 1)this is opaque expression number 42; 2) it is computed based on an Array opaque kind; and 3) it should always have the value 128. Default=FALSE.
--InitOpaqueObfuscate BOOLSPEC Apply some light obfucation to the initialization of opaque state variables. Default=TRUE.
--InitOpaqueSize INTSPEC Size of opaque arrays. Default=30.

To frustrate analysis, updates that maintain the invariants should be sprinkled throughout the program. This is done by the --Transform=UpdateOpaque option:

OptionArgumentsDescription
--Transform UpdateOpaque Add code that makes updates to opaque predicates.
--UpdateOpaqueCount INTSPEC How many updates to opaque data structures to add to the function. Default=1.
--UpdateOpaqueTrace BOOLSPEC Print the updated structure. Default=false.
--UpdateOpaqueDebug BOOLSPEC If true, then we store all opaque values in a temporary variable that reveals its expected value. Default=FALSE.
--UpdateOpaqueObfuscate BOOLSPEC Apply some light obfucation to opaque updates. Default=TRUE.
--UpdateOpaqueAllowAddNodes bool Is it safe to malloc new nodes for the opaque data structure in this function? Only set to true if the function is called sparingly. Default=false.

Note: In --Transform=InitOpaque --Functions=foo, the function foo must execute before any use of an opaque expression. Easiest is to set --Transform=InitOpaque --Functions=main but this is best avoided since it is very obvious.

 

Issues

Tigress will generate copious numbers of extra local variables and statements of the form _*__BARRIER_* = 1, _*__BEGIN_* = 1, _*__END_* = 1. They will be removed by any competent compiler, or by the --Transform=CleanUp --CleanUpKinds=annotations transformation.

 

References