[klee-dev] Restrict memory access to a memory region

[Kuchta, Tomasz]

Hi Mark,
 
I’m not sure if I understood the question correctly. My understanding was that you would like to define a safe region for the application and then treat all the memory accesses falling outside of that region as invalid - is that correct?
One idea might be to do that with an additional intrinsic. That would, however, mean introducing instrumentation into the source code of the tested application.
In the intrinsic you would say, e.g., that addresses 0xABCD - 0xEFFF are valid and then you would check inside the executeMemoryOperation method, whether the address being accessed falls into this
valid range. 
Things probably will be more complicated for these addresses that are symbolic. I guess for these, one would need to request a concrete value from the SMT solver. I can imagine a situation in which
the valid range for the pointer expression only partially overlaps with the defined valid memory region, so I think that probably the solver query should also include range constraints for our defined valid memory region (in order to avoid 
false positives resulting from the fact that the solver just happened to return a value falling into the valid range).
Please note that KLEE runs in the same address space as the interpreted program.

Hope that helps,
Tomek 

On 22 Nov 2014, at 10:31, Mark R. Tuttle <tuttle at acm.org> wrote:

> How would you define a region of memory and assert that a pointer should never point outside of that region?
> 
> To assert that all reads and writes should access only memory within that region?
> 
> Thanks,
> Mark
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 4713 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20141122/d4865cb7/attachment.bin>