Re: [klee-dev] Homebrew Package
Dear Carlo, I just tried installing KLEE via Homebrew and it worked like a charm. I can’t thank you enough for this! For an occasional user like me it simplifies things greatly. Best, Anton > On 12 Mar 2021, at 19:45, Carlo Cabrera > wrote: > > Dear klee-dev, > > I noticed that packaging was listed as an open project on the website. > So, I submitted klee for packaging at Homebrew [1]. > > If you use Homebrew (on macOS or Linux), you can now install klee with > >brew install klee > > It is built with libc++, but without exception handling. EH lead to a > build failure on macOS. > > The Homebrew package has a pre-built binary on macOS. If there is > interest in one for Linux as well, I can look into it. > > Best, > Carlo > > [1] https://brew.sh > > ___ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Re: [klee-dev] Homebrew Package
Hi Carlo, This is great to hear! Thanks for this contribution! We should update the website with this info soon. It would be of course great to have one for Linux too; from what I can tell, many of our users use Ubuntu, although I don't have any stats. Best, Cristian On 12/03/2021 16:45, Carlo Cabrera wrote: Dear klee-dev, I noticed that packaging was listed as an open project on the website. So, I submitted klee for packaging at Homebrew [1]. If you use Homebrew (on macOS or Linux), you can now install klee with brew install klee It is built with libc++, but without exception handling. EH lead to a build failure on macOS. The Homebrew package has a pre-built binary on macOS. If there is interest in one for Linux as well, I can look into it. Best, Carlo [1] https://brew.sh ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Homebrew Package
Dear klee-dev, I noticed that packaging was listed as an open project on the website. So, I submitted klee for packaging at Homebrew [1]. If you use Homebrew (on macOS or Linux), you can now install klee with brew install klee It is built with libc++, but without exception handling. EH lead to a build failure on macOS. The Homebrew package has a pre-built binary on macOS. If there is interest in one for Linux as well, I can look into it. Best, Carlo [1] https://brew.sh ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Using KLEE to analyze (complex) data structures
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
--
Jens Van den Broeck
Computer Systems Lab
Electronics and Information Systems department
Ghent University
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[klee-dev] Using KLEE to obtain Path Constraints from concrete input queries in an Active Learning setting
Dear all, I'm working on (white-box/grey-box) Active Automata Learning for programs with data parameters (i.e., our automata contain data parameters in guards and in i/o). We require that for each concrete query, we can extract data (i.e., path) constraints for that query. For instance, consider that we have a one-element FIFO buffer with two actions: PUSH(p) and POP(p): Given a query of the form ``PUSH(p1=5) POP(p2=3)'' (where p1 and p2 are the "markers"/"names" given to 5 and 3), we want to retrieve the constraint "p1 =/= p2" from the path followed by the program (assuming that the comparison between 5 and 3 actually happens in the program). We're trying to obtain these PC using KLEE. I've been trying to get concrete inputs working with KLEE (latest docker build) and Zesti (docker, from https://github.com/rshariffdeen/zesti), but I guess I'm doing something wrong. For instance, consider the "Tutorial One" example, get_sign, with no changes to the source code. If I run it with klee-zesti, as "klee-zesti -posix-runtime -libc=uclibc get_sign.bc 22", It would expect to explore only one branch, but I somehow end up exploring 10? With Zesti (if anyone has any idea), I still end up exploring all 3 branches of the function. Does anyone have any clues on how to get this working? (Either KLEE or Zesti would be fine :)) Thank you, Regards, Bharat Garhewal, ICIS - SWS, Radboud University ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
