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

[Kuchta, Tomasz]

Hi Mark,

What I had in mind was to add a new KLEE intrinsic, which would unfortunately result in instrumenting also the tested application with the calls to the intrinsic.
With regard to state explosion problem - as far as I understand, if you would handle the checks inside executeMemoryOperation, you could only report errors for possible
overflows and just continue for all the other accesses, without spawning additional execution states. These checks will affect the performance, but I’m not sure how much.

If you were to perform instrumentation with a sanitiser, as you mentioned, I think that potentially new states will be created at every branch point that involves symbolic data and for which both
sides of the branch are feasible. Again, I’m not sure how much that would affect the performance - I guess this also depends on how much of symbolic data you would like to have. I think that forking will only
be possible if there is symbolic data involved at the given branch point.

Best regards,
Tomek


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

> Thank you, Tomasz.
> 
> 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?
> 
> You are correct.  I want to demonstrate that something like an interrupt handler reads and writes only from a safe region of memory.  My plan was to compile the code with clang to LLVM byte code as usual, then use the LLVM API to instrument the byte code to check the address of every load and store, and then to run KLEE on the instrumented code as a black box.  Among other things, I'm concerned that this plan to insert a conditional at every load and store will double the number of states for KLEE to explore and destroy the performance of KLEE.
> 
> But KLEE has in its API klee.h some methods like klee_define_fixed_object and klee_mark_global and klee_check_memory_access, and clang has the ability to add runtime checks like the UBSAN Undefined Behavior Sanitizer, and I'm wondering if I'm missing a much easier solution.
> 
> When you write "an additional intrinsic" are you talking about adding a KLEE intrinsic or an LLVM intrinsic?  I am reluctant to adopt a solution that requires manual modification or instrumentation of the source code, because I want the solution to be as push-button as possible, but I'd like to hear a bit more about your proposal.
> 
> Thanks,
> Mark
> 
> 
> On Sat, Nov 22, 2014 at 6:48 AM, Kuchta, Tomasz <t.kuchta12 at imperial.ac.uk> wrote:
> 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: 6197 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20141122/fc54551f/attachment.bin>