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

[Cristian Cadar]

Hi,

You say that you "got no useful results from KLEE so far" but it's 
difficult to help without more info and a self-contained program which 
reproduces the problem.

Most likely though, you are hitting the challenge described in this 
paper, which offers a solution (and an extension of KLEE) which can deal 
better with complex data structures such as hashtables:
https://srg.doc.ic.ac.uk/projects/klee-segmem/

Best,
Cristian

On 12/03/2021 10:53, Jens Van den Broeck wrote:
> 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
>