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

[Jens Van den Broeck]

Hi Cristian,

Thank you for the quick response and the link to your publication. I've
read the article on segmented memory, and tried my use case. Sadly,
still, I am not able to achieve my goal.

I have written a minimal working example (MWE), which is available on
Github: https://github.com/jvdbroeck/mwe-klee. It is a very small
program that only evaluates the opaque predicate, and prints different
output depending on whether the predicate evaluates to "true" or
"false". The predicate is encoded in an instance of a hash table: it is
"true" when a predetermined key is present in the hash table, and
"false" if it is not present. Now I want to use KLEE to test whether or
not it is able to construct a valid state for the hash table so that
each path is triggered. To do this, I tried to:

* Mark the entire memory region allocated to the hash table instance as
symbolic (the call to klee_make_symbolic in init_pred in predicate.c),
but then some required metadata, which must be set correctly for the
hash table helpers to work, is also marked as symbolic. Doing so
triggers, amongst others, assertion failures in the hash table helpers.

* Mark only the buckets allocated to the hash table as symbolic (the
call to klee_make_symbolic in get_pred in predicate.c), which triggers
KLEE to almost immediately finds a state for the "false" path, but not
for the "true" path. Maybe this is because it tries to brute-force the
data in the buckets, which would just take a very long time?

Best regards,

Jens

On 3/15/21 10:45 PM, Cristian Cadar wrote:
> 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
>>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-- 
Jens Van den Broeck

Computer Systems Lab
Electronics and Information Systems department
Ghent University