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 <[email protected]> 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 <[email protected]> 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 > > [email protected] > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
