Another invalid memory accesses in some ldv benchmarks

[mchalupa]

The benchmark ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--penmount.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c contains multiple invalid dereferences. On this link you can find a witness for one of the errors (invalid dereference on line 2852, due to the fact that dev_get_drvdata is undefined): https://gist.github.com/mchalupa/d1a01facc40d21662a28a5de5d0aec75 . I was able to verify the witness with this command:

scripts/cpa.sh -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -64 -witness ~/src/symbiotic-dbg/install/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const ~/src/sv-benchmarks/c/ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--penmount.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c -spec ~/Downloads/PropertyMemSafety.prp    

(CPAchecker is also able to find this error itself if set up to search for memory safety errors).

Another problem with this benchmark is that the function input_allocate_device is undefined. If we assume that it can return any pointer, there is an invalid dereference on the line 3030 (in the witness file, change the tmp___0 == 2 assumption to tmp___0 == 0).

The same problems are also in these benchmarks:

ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--touchright.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--pcf8591.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--hwmon--pcf8591.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
ldv-linux-3.4-simple/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--mtouch.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
ldv-linux-3.4-simple/43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--input--touchscreen--touchright.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c

For the undefined input_allocate_device function there should be quite an easy fix, but I'm not sure what to do with the dev_get_drvdata.

[dbeyer]

@mchalupa, could you please make it more concrete by creating a pull request?

[mchalupa]

I don't know if in all these benchmarks modified in #556 the input_allocate_device was problematic, but at least in the five mentioned above, it was.

[mutilin]

@mchalupa
For checking the witness you are using -spec ~/Downloads/PropertyMemSafety.prp which is not related to the property mentioned in benchmark unreach-call. So you found the violation of valid-deref, but not unreach-call.

[tautschnig]

If they were false-unreach-call then I'd say "ok, needs to be added to #480". But claiming the call is truly unreachable in presence of undefined behaviour is much harder. Please provide a proof that, despite the undefined behaviour, it remains impossible to reach this call. At bare minimum you'll have to prove that it is impossible to craft a stack-based buffer overflow (as such could be used to manipulate the return address to point to __VERIFIER_error).

[mchalupa]

@mutilin : Yes, that is what am I reporting -- an invalid access to memory.

[mutilin]

Please provide a proof that, despite the undefined behaviour, it remains impossible to reach this call.

In such settings the tool which reports false-valid-deref should provide an exploit which allows to call __VERIFIER_error

But claiming the call is truly unreachable in presence of undefined behaviour is much harder.

For the competition I think we should require that the state violating memsafety property terminates the path. It will allow to eliminate undefined behaviour from consideration in unreach-call.

[mutilin]

@mchalupa

@mutilin : Yes, that is what am I reporting -- an invalid access to memory.

but the property to check is unreach-call

[tautschnig]

If you are asking for exploits, we might just keep it simple. Just link the following against the benchmarks:

void ldv_initialize()
{
  __VERIFIER_error();
}

That's me making use of undefined behaviour without even resorting to memory errors.

For the competition I think we should require that the state violating memsafety property terminates the path.

Could you please elaborate? I don't understand what this means.

[mutilin]

That's me making use of undefined behaviour without even resorting to memory errors.

So use this, but do not refer to memory errors!

Could you please elaborate? I don't understand what this means.

All paths which violate some property are aborted and can not be used as a prefix for violation of any other property.

[mchalupa]

That's me making use of undefined behaviour without even resorting to memory errors.

So use this, but do not refer to memory errors!

Memory errors are undefined behavior...

All paths which violate some property are aborted and can not be used as a prefix for violation of any other property.

This could be a nice assumption for the multi-property category which has been discussed for some time, but so far in the rules we have that exactly one property is violated in a benchmark. Invalid dereference is undefined behavior and as such you can not assume that the program is just killed there (although it is a common case). You can not, in fact, assume anything and that is the problem.

@mutilin : Yes, that is what am I reporting -- an invalid access to memory.

but the property to check is unreach-call

I thought the general consensus is that if a benchmark violates false-valid-deref (and at least these five benchmarks do), then it should not contain any other label. So if nothing else, these benchmarks are mislabeled.

[mutilin]

That's me making use of undefined behaviour without even resorting to memory errors.

so far in the rules we have that exactly one property is violated in a benchmark

I do not see such requirement in the rules. You can even see examples like list-ext_flag_false-unreach-call_false-valid-deref.c, list_and_tree_cnstr_false-unreach-call_false-termination.c, sll-queue_false-unreach-call_false-valid-memcleanup.c ...

So use this, but do not refer to memory errors!

Memory errors are undefined behavior...

Well, not all memsafety properties. Even valid-deref which is undefined, but not always exploitable.

I thought the general consensus is that if a benchmark violates false-valid-deref (and at least these five benchmarks do), then it should not contain any other label.

There is no general consensus

There are examples like list-ext_false-unreach-call_false-valid-deref.c, dll-rb-cnstr_1_false-unreach-call_false-valid-deref.c, tree_false-unreach-call_false-valid-deref.c ...

[mutilin]

Regarding benchmarks contained in the directory ldv-linux-3.4-simple my position is still the same as in #466. They were prepared with very naive environment model

[mchalupa]

I do not see such requirement in the rules.

Yes, my bad, I formulated it incorrectly, what I said holds only for MemSafety category. The rest of the sentence, however, still holds. What I meant to say is that some lables are quite incompatible, like false-valid-deref and anything else.

(btw. I also do not see a rule that says that "the state violating memsafety property terminates the path".)

There is no general consensus

OK, so fast I could find only these two links, which may not be very convincing: #480 #485 (comment)

[mchalupa]

Anyway, I think that the conversation is starting diverging from the original topic, which is that the reported benchmarks contain invalid memory accesses (whatever it means for the unreach-call label).

[Heizmann]

I cannot understand the original witness that was posted here. It seems to end at the statement tmp___0 == 2 which is clearly not related to an invalid memory dereference.

I was able to run a recent version of UAutomizer on the program. Our tool claims that the program is not valid-deref, witness attached.

However after look at this more carefully, I found out that our tool complains about a cast from a pointer to a long which is then incremented by 16 and cast back to a pointer. This is not undefined behaviour but implementation defined.
32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--penmount.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c-witness.graphml.txt

[mchalupa]

I cannot understand the original witness that was posted here. It seems to end at the statement tmp___0 == 2 which is clearly not related to an invalid memory dereference.

The witness describes just a prefix of the error path.