Invalid memory access in DeviceDriversLinux64

[shaobo-he]

Hi guys,

I found several problematic benchmarks that contain invalid memory access in DeviceDriversLinux64 category. For each benchmark, I will briefly describe the problem and its witness file can be found in a github repo (https://github.com/Guoanshisb/BenchmarksWithInvalidDerefs).

ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--dvb--dvb-usb--dvb-usb-az6007.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c main calls az6007_tuner_attach with an local uninitialized pointer var_group4 as the argument. At line 8295, __cil_tmp27 is dereferenced which is var_group4 plus an offset.

ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--gpu--drm--ttm--ttm.ko-ldv_main5_sequence_infinite_withcheck_stateful.cil.out.c main calls ttm_bo_vm_fault with two local uninitialized pointer var_group1 and var_group2. The first argument is derefenced multiple times in this function. For example, at line 9887, an uninitialized function pointer is dereferenced which can alias to any function with identical signature.

ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--pcmcia--pcmcia.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c pccard_show_cis is called by main with two local uninitialized pointers var_group1 and var_group2 as arugments. pccard_validate_cis is called by pccard_show_cis with a argument which is essentially var_group2 plus an offset. This argument is passed around and dereferenced directly or indirectly.

ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--rtl8150.ko-entry_point_true-unreach-call.cil.out.c main calls rtl8150_probe with global pointer rtl8150_driver_group1 as an argument, which is not assigned to any memory location. rtl8150_probe then calls interface_to_usbdev which dereferences rtl8150_driver_group1.

@zvonimir @MontyCarter @mutilin

[mutilin]

All benchmarks in ldv-consumption directory are using parameters var_groupN which are not initialized. Why only these 3 benchmarks are causing problems?

[shaobo-he]

Hi @mutilin,

Based on my observation, it is because dereferencing some uninitialized function pointers that are reachable from these parameters results in calling functions that lead to assertion failure (let's call them buggy functions). In some benchmarks, buggy functions do not match the signature of these uninitialized function pointers while others do as those that I pointed out in my previous comment. I can show you the location where such function pointer deference happens.

[zvonimir]

@mutilin It could as well be that other benchmarks contain similar problems. It is hard to say why SMACK is not discovering these problems in other benchmarks. Maybe they are in the parts of the code that is irrelevant for a particular property being checked. Maybe SMACK times out on other benchmarks that have this problem. We can certainly not guarantee that SMACK can find all such problems.

Having said that, I think we should certainly try to fix the ones that SMACK does find, such as the ones that @Guoanshisb reported. I hope you agree with that.

Finally, if folks who submitted these benchmarks don't have time to fix them, they we can give it a try. Just let us know ASAP and we will try to propose a patch.

[mutilin]

See #227, #228, #229 for examples N1, N2, N3

[PavelAndrianov]

@Guoanshisb In the benchmark ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--usb--rtl8150.ko-entry_point_true-unreach-call.cil.out.c (the fourth one) rtl8150_probe could not be called before rtl8150_driver_init, which correctly allocates memory for rtl8150_driver_group1

[tautschnig]

@Guoanshisb With @AndrianovPavel's further comment, are all issues covered by either a pull request or that final comment? If so, this issue should be closed.

[shaobo-he]

Hi @mutilin @AndrianovPavel ,

Sorry for the late reply.

SMACK still reports bugs for these benchmarks. For example, in N1, var_group_4 is calloced, so __cil_tmp23 at line 8285 is equal to the return value of calloc + 1600. __cil_tmp24 at line 8286 is the deference of __cil_tmp23 which equals to 0 (calloced memory). __cil_tmp26 at line 8288 will be 360, which is not initialized. __cil_tmp27 at line 8289 is the deference of __cil_tmp26 which can be any value. In line 8295, a function pointer is called which is the deference of __cil_tmp27 . So a function that results in the assertion failure will be called since *__cil_tmp27 could alias with any function.

It seems that you may have to initialize the structure in a complete way.

Please let know if it makes sense.

[shaobo-he]

@AndrianovPavel With respect to the fourth benchmark, rtl8150_driver_group1 got the return value of ldv_zalloc, which can return a NULL pointer.

[PavelAndrianov]

@Guoanshisb Could you check the fix of the fourth issue?

[shaobo-he]

@AndrianovPavel I'm afraid your changes does not fix the issue. Please take a look at the error witness attached. witness.txt

[shaobo-he]

@AndrianovPavel @mutilin May I ask what is your assumption on uninitialized function pointer dispatch?

[mutilin]

CPAchecker witness validator could not confirm the witness.txt in 90 sec. Is there any confirmation from the other validators?

[zvonimir]

Why don't you run it without this 90 seconds time out? This is not the competition, but rather an attempt to fix bugs in SV-COMP benchmarks, and so enforcing this time out makes no sense to me. Also, if CPAChecker cannot find this bug in the first place, then why do you think it would be able to discharge our witness?

[mutilin]

@zvonimir, of course, CPAchecker may fail as any other tool. I just try to understand what is the confedence in correctness of the witness. @Guoanshisb, did commenting of function pointer calls help SMACK to prove true?

[shaobo-he]

@mutilin Yes, it seems so for some benchmarks. For other benchmarks that SMACK reported a false bug, commenting out function pointers does not help. We will look into them.

[PhilippWendler]

@shaobo-he Is this fixed?

[PhilippWendler]

@shaobo-he @mutilin @AndrianovPavel Is this fixed?