Hi Jeroen,

Thank you very much for this question.

The problem is mainly a time issue. Somebody needs to port the changes to the 
newer version of KLEE,
adds test cases and open a PR. Another aspect to keep in mind are potential 
license issues.
>From an engineering perspective, nothing should be a major issue.

Those extensions are absolutely useful.
It would be nice to find the upstreamed.

I hope that answers your question.


On 1. Dec 2021, at 11:24, Jeroen Robben 
<jer...@robben.io<mailto:jer...@robben.io>> wrote:


Hi all,

Some variant(s) of this question was asked before but I couldn't find a 
fulfilling answer in the mailing list nor Github issues archive.

Is there some effort being done to extend the current KLEE POSIX runtime model 
to add support for testing network interactions / sockets, e.g. to be able to 
insert symbolic packets? I've found some research projects which make use of 
KLEE (e.g. Cloud9, SymbexNet, Zesti), claiming to have done this.
Is there at the current moment a specific reason support for networking was not 
yet added or backported to the main KLEE project or is it just a case of 'not 
implemented yet'?

Thanks!

Jeroen

_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk<mailto: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

Reply via email to