[klee-dev] Current status of KLEE support for networking

[Nowack, Martin]

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 <jeroen at robben.io<mailto:jeroen at 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 at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed