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

[Mark R. Tuttle]

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 --------------
HTML attachment scrubbed and removed