Is it still meaningful to migrate SymDrive to S2E 2.0?

[Lang Rin]

Hi Vitaly Chipounov，

I am currently conducting research on mining vulnerabilities in Linux drivers using symbolic execution.

 
During my research, I came across the paper "SymDrive: Testing Drivers Without Devices" authored by MJR in 2012. I found it to be an excellent work built upon the excellent S2E framework.  However, I noticed that the code is based on the older version of S2E (s2e-old). Unfortunately, I have been unable to contact MJR directly, but I discovered your commits in the SymDrive repository on GitHub. 

I have two questions  now:

1. Is it meaningful to migrate SymDrive to S2E 2.0?
2. Why have there been no further developments or works based on SymDrive? Are there specific limitations or defects within SymDrive that have hindered additional research and development? 

Understanding these challenges could provide valuable insights for future work in this area.I would greatly appreciate any insights or information you could provide on these questions.   Thank you very much for your time and assistance.

Rinlang

[Vitaly Chipounov]

Hi,

You may test Linux drivers on the latest S2E, basic symbolic execution will work. At a minimum, you need is a test harness to inject symbolic values, e.g., from user space or with kprobes. Here are the limitations:

- You will need to create an empty Linux project with s2e-env and then modify bootstrap.sh yourself in order to load the *.ko files. You won't be able to do "s2e new_project driver.ko" and have everything set up automatically, like for user-space binaries.
- LinuxMonitor does not support drivers, so you won't be able to get code coverage or use most of the analysis plugins out of the box. If you driver is statically linked into vmlinux, it will work ok (with some manual tweaks to config files).

- S2E 2.0 does not support symbolic PCI devices, so you will not be able to analyze those easily. I didn't port it from the old S2E because the new architecture makes it harder to do (S2E is now decoupled from QEMU and that requires extra communication).

I don't have plans to implement any of the above, but I'd be happy to review and merge any contributions. You can start with the s2e-env and LinuxMonitor tooling.

Regarding your two questions below, SymDrive is a research prototype and is most likely abandoned by its author, as it often happens with academic projects. I am sure you can extract useful bits and port them to the latest S2E. The plugin architecture remained more or less the same with a few API tweaks, so porting them should be doable.

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/df9fb6b0-68c6-4c01-b87d-40f56476d1a4n%40googlegroups.com.

[Lang Rin]

Hi  Dr.Vitaly，

Thank you for your insightful guidance in our previous discussion. Over the past few weeks, I have been studying the source code of ​​S2E​​ and ​​SymDrive​​ to better understand their symbolic execution workflows for hardware driver testing. I would greatly appreciate your expertise on the following questions:

1. I’ve noticed that the implementation of the current SymbolicHardware plugin has changed significantly compared to the older version of S2E. I dont know if I was right for the following statements:
In S2E-old, SymbolicHardware is deeply coupled with QEMU, it seems register a fake device in QEMU.
In S2E 2.0,  SymbolicHardware uses SpecialFunctionHandler to hook the  call to  tcg_llvm_trace_port_access and tcg_llvm_trace_mmio_access , then symbolize the  value.
You said "S2E is now decoupled from QEMU and that requires extra communication". SymDrive is mainly based on SymbolicHardware plugin, does it mean that I can still use a coupled way(like adding old code to QEMU) to implement it (just for my own study purpose)？

2.You said “S2E 2.0 does not support symbolic PCI devices”. In my understanding, running a driver needs some inputs from hardware device(by PIO/MMIO/DMA), which have been  symbolized and provided in SymbolicHardwar plugin.Is it  special for PCIe devices and other devices on different buses?

3.What factors currently limit the scope of hardware drivers that S2E can test?

Your insights would be invaluable to my research.Thank you for your time.

Rinlang

[Vitaly Chipounov]

Hi,

Please find my answers below.

On Friday, April 25th, 2025 at 8:11 AM, Lang Rin <Rin...@outlook.com> wrote:

1. I’ve noticed that the implementation of the current SymbolicHardware plugin has changed significantly compared to the older version of S2E. I dont know if I was right for the following statements:
In S2E-old, SymbolicHardware is deeply coupled with QEMU, it seems register a fake device in QEMU.
In S2E 2.0, SymbolicHardware uses SpecialFunctionHandler to hook the call to tcg_llvm_trace_port_access and tcg_llvm_trace_mmio_access , then symbolize the value.

You said "S2E is now decoupled from QEMU and that requires extra communication". SymDrive is mainly based on SymbolicHardware plugin, does it mean that I can still use a coupled way(like adding old code to QEMU) to implement it (just for my own study purpose)？

You will need to write a symbolic virtual hardware device for QEMU and figure out a way how to make it communicate with the S2E plugin. In the old S2E, the coupling made it easy. In the new S2E, there is a KVM layer in between. The virtual hardware device would need to notify the plugin about its configuration so that the plugin can request the S2E engine to make the right ports and MMIO ranges symbolic.

2.You said “S2E 2.0 does not support symbolic PCI devices”. In my understanding, running a driver needs some inputs from hardware device(by PIO/MMIO/DMA), which have been symbolized and provided in SymbolicHardwar plugin.Is it special for PCIe devices and other devices on different buses?

At the moment, SymbolicHardware supports static configuration for IO ports and memory ranges. This works for simple devices that have fixed resource assignments.

It does not support packet-based devices, like USB. It's probably easier to hook those in the guest directly, when the generic USB bus driver sends/receives packets to/from the device. Your fake USB driver would make the required data symbolic. If you have the actual USB device available, you could also use concolic execution to use the real device inputs as seeds.

3.What factors currently limit the scope of hardware drivers that S2E can test?

I don't have time to work on it, that's the major factor. There are no technical issues in general, one would need to look at each device class and think of a suitable design for symbolic data injection, develop the adequate plugins and corresponding tests, and write the documentation.

Vitaly

To view this discussion visit https://groups.google.com/d/msgid/s2e-dev/3f83b98f-88e7-45ac-93e7-ae368dc94cfan%40googlegroups.com.