Closed TodAmon closed 2 years ago
This comment leads me to believe that "state.memory.load" should hit the concrete target:
The underlying memory backend is hooked in a way that all the further memory accesses triggered during symbolic execution are redirected to the concrete process.
Just to clarify, @degrigis and I discovered that only some reads are redirected to the gdb target. A read of a static variable is not redirected. Angr only reads from the gdb target if it is performing a DefaultFillerMixin's default method. For example, if you run concretely and stop after the concrete execution has modified a static variable, and then run symbolically, angr will miss the fact that the static variable was modified. You will get incorrect results.
So, I investigated this quite a bit. It seems to me that the fundamental issue at play here is that Symbion should be willing to load pages from the concrete target. Right now, it only loads individual values using the DefaultFillerMixin. If pages were initialized using memory read from the concrete target, you would not need to do anything special when subsequent writes wrote over those values with new symbolic values (or concrete ones)... as long as the page stays resident, which I think it should.
I played around with various fixes, and ended up with what appears to be an elegant solution, but I would appreciate feedback (I have not submitted a pull request). The fix is quite simple, modify the file
storage/memory_mixins/paged_memory/page_backer_mixins.py
and in the class ClememoryBackerMixin
in the method _initialize_page
, replace the line of code that always fetches data from the backer, with the following:
if self.state.project.concrete_target:
l.debug("Fetching data from concrete target")
data = claripy.BVV(bytearray(
self.state.project.concrete_target.read_memory(pageno*self.page_size, self.page_size)),self.page_size*8)
else:
# Load data from backere
data = self._data_from_backer(addr, backer, backer_start, backer_iter)
@TodAmon the fix seems legit to me and should not impact any other behavior. Do you have any news regarding this? If everything is running smoothly, can you please open a PR? Huge thanks!
(We are also discussing this bug here as it has been re-discovered by @mborgerson)
I don't like the fix because it's a terrible mixing of abstractions - ideally you would create a new backer mixin that would be inserted above the clemory backer and perform this logic. However if for some reason that doesn't work I am (begrudgingly) fine with it as stated.
In fact when I put this fix into our system, I did exactly what @rhelmot suggests -- created a new ConcreteBackerMixin that lives directly in front of the ClememoryBackerMixin (in a new Memory class). I don't have anything else to add -- it appears to work. One concern would be if this will properly support switching back and forth between concrete and symbolic, something I have not explored. Ideally that would be tested as well.
Gotcha @rhelmot. As soon as this doesn't impact the way we flush and re-load pages we should be good. @TodAmon, if you have time to open a PR with the modifications I can try it with some test programs :)
This issue has been marked as stale
because it has no recent activity. Please comment or add the pinned
tag to prevent this issue from being closed.
This issue has been closed due to inactivity.
If I use avatar_gdb.read_memory, I get a value from a concrete execution. But the state obtained using symbion, does not "redirect the read to the target" like I thought it would. E.g., state.memory.load does not result in the target doing a read. Is this expected? Was the memory load modified for the engine, but not for the direct "state.memory.load" method?