Regarding the issue of testing binary for kernel symbolization.

34 views
Skip to first unread message

Jay Ironman

unread,
Nov 19, 2024, 8:38:16 AM11/19/24
to S2E Developer Forum
Hello

  I can now use S2E to tokenize different versions of the Linux kernel, but I have a question that seems more like a consultation:

  What should I do if I want to use S2E for symbolic execution of certain specific content? For example, for all I/O device modules. Of course, I am aware that I need to write a test binary, call the target I/O device, and tokenize its parameters.

  The key to the problem lies here, how to automate the writing of test binary to perform symbolic execution on all I/O device modules?

  I think I should have described it clearly. If I could get your answer, I would be extremely grateful.

thank you

Vitaly Chipounov

unread,
Nov 24, 2024, 1:44:15 PM11/24/24
to s2e...@googlegroups.com, Jay Ironman

Hi,

You will need to provide a test harness yourself. S2E cannot automate that. Perhaps you could give AI a try to automate writing one.

Vitaly

--
You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/s2e-dev/ec89ca62-4c53-40c3-8b2c-d41cd1a8dce7n%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages