[klee-dev] Using KLEE to analyze (complex) data structures

[Jens Van den Broeck]

Hello klee-dev members,

I'm doing research on software protection techniques for compiled
programs. To assess the strength of one of my techniques, I want to know
whether KLEE can be used to analyze my protection. Conceptually, I
protect programs with "flexible opaque predicates", a form of
context-sensitive opaque predicates. Instead of encoding a TRUE or FALSE
value in a (complex) computation, I manipulate the state of some
(complex) data structure.

As an example, consider the following simplified program in which a hash
table is used to encode a flexible opaque predicate. Concretely, I want
to know whether or not there is a way for KLEE to indicate under what
conditions the TRUE and FALSE paths of the flexible opaque predicate
(label "flexible_opaque_predicate" in the example) implemented in
'protected_function' can be taken. Ideally, this would be some valid
state for the protection data structure ("protection_ds" in the example).

I tried marking the entire data structure as symbolic, but got no useful
results from KLEE so far: klee_make_symbolic(protection_ds,
sizeof(t_hashtable), "protection_ds"). But maybe there is another way?
Or it is not possible?

char *protection_key = "some_string";
t_hashtable *protection_ds = NULL;

// some implemented hash table operations
void hashtable_remove_entry(t_hashtable *table, void *key) {
  ... // hash key with function 'table->hash_func_ptr' and remove bucket
}
void hashtable_set_entry(t_hashtable *table, void *key, void *value) {
  ... // hash key with function 'table->hash_func_ptr' and store value
in bucket
}
bool hashtable_contains_entry(t_hashtable *table, void *key) {
  ... // hash key with function 'table->hash_func_ptr' and return TRUE
if bucket exists
}

void protected_function() {
  ...
  // set predicate to TRUE
  hashtable_set_entry(protection_ds, protection_key, (void *)42);
  ...
flexible_opaque_predicate:
  if (hashtable_contains_entry(protection_ds, protection_key) {
    ... // executed when the predicate is set to 'TRUE' (see higher)
  }
  else {
    ... // executed when the predicate is set to 'FALSE' (see below)
    goto finalize;
  }
  ...
  // set predicate to FALSE
  hashtable_remove_entry(protection_ds, protection_key);
  ...
  goto flexible_opaque_predicate;
finalize:
  ...
}

int main(int argc, char** argv) {
  protection_ds = create_hashtable(hash_func_ptr); //'hash_func_ptr' is
a pointer to a hash function
  ... // do some work
  protected_function();
  ... // do more work
}

Thanks in advance,
Jens

-- 
Jens Van den Broeck

Computer Systems Lab
Electronics and Information Systems department
Ghent University