Regarding the issue of symbolic parameters

[Jay Ironman]

Hello
Now there are the following scenarios:
1. Write a kernel module where a branch contains a memory error that triggers when the input parameter length is greater than 64 (after experimentation, there is no problem). The code is as follows:

2. Write a binary (assuming the binary name is "test"), call the kernel module (after experimentation, no problem), and the code is as follows:

3. Use S2E to perform symbolic execution on the binary and tokenize its parameters (in order to trigger memory errors in the kernel module written in the first step). The specific steps are as follows:

4. Then enable symbolization of the kernel, as follows:

5. Then begin symbol execution:

`$ ./launch-s2e.sh`

Actually, the above steps are not a problem, but I encountered a problem during the experiment. Here are two commands for me to create symbol execution projects:
1. `$ s2e new_project --image ubuntu-22.04-x86_64 ~/test/test_mem_error "This is a test for S2E"`
2. `$ sudo ./ test_mem_error "This is a normal situation aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"`

I found that when creating a project, the results produced by tokenizing different length parameters are different
1. Command 1 will not trigger a memory error, and the length of the generated test case is the same as its parameter length (both are 22), and only a few parameter values are mutated from the original parameter length. In summary, it will not enter the branch with memory errors
2. Command 2 will trigger a memory error because its parameter length meets the conditions for triggering a memory error. However, in this case, only a few parameter values are mutated from the original parameter length, and no test cases of other lengths will be generated

So I have a very big question now, what should I do if I want to generate test cases of different lengths and types? Is it not enough to just tokenize the parameters? Because I want to trigger more types of errors, or cover as many paths as possible, or is S2E only capable of doing so much?

This is very important to me, I hope you can answer my question!

[Vitaly Chipounov]

Hi,

Your approach will cause path explosion in strlen. In this case, it's better if you modify your program to call s2e_make_symbolic directly on both the input buffer and the input length. Something like this:

main() {

  char buffer[MAX_LEN];

  int len;

  s2e_make_symbolic(buffer, sizeof(buffer), "buffer");

  s2e_make_symbolic(&len, sizeof(len), "len");

  if (len > MAX_LEN) {

     // This puts a constraint on maximum length.

     return;

  }

  ...

  write(fd, buffer, len);

  ...

}

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 on the web visit https://groups.google.com/d/msgid/s2e-dev/87474206-b89f-4946-a686-cd8dd0896ddfn%40googlegroups.com.

[Jay Ironman]

Okay, I will try, thank you. But I still have a few questions:

1. How to determine if a symbol explosion/loss has occurred

2. How to completely avoid symbol explosion, as I need to perform symbol execution on the kernel

3. I hope that the generated test cases can not only modify values, but also modify lengths. In short, it is best to cover all branches to trigger vulnerabilities

4. To be honest, I don't quite understand the process of symbol execution in S2E. I just read the source code of a few simple commands in S2E (PS, your code is so beautiful). If I want to modify the content about path selection during symbol execution, which part of the code should I modify?

There may be a lot of questions, but this is my current problem that is preventing me from conducting further research. I hope to receive your answer.

[Jay Ironman]

I conducted the experiment according to your method, but was unable to cover the target code (based on code coverage) 'ssize_t bytes_rritten=write (fd, input, len)', thus unable to perform symbolic execution on the target kernel module. Modifying the previous version can actually overwrite the target code, but there are the aforementioned issues.

在2024年8月12日星期一 UTC+8 21:27:56<Vitaly Chipounov> 写道：

[Jay Ironman]

Thank you for your reminder（I overlooked some details before, sorry）. I have successfully completed the experiment now. Thank you again!