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 >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev -- Jens Van den Broeck Computer Systems Lab Electronics and Information Systems department Ghent University _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
