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

[Jens Van den Broeck]

Apparently the URL in my previous message points wrongly refers to my
Github repository with a "dot" appended. That destination of course does
not exist.

The correct link is https://github.com/jvdbroeck/mwe-klee

Best,

Jens

On 3/16/21 10:43 PM, Jens Van den Broeck wrote:
> 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