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
