[ldv-project] First application of CBMC for driver verification with help of LDV

[Evgeny Novikov]

Dear Daniel,

until recent days I hadn't enough time to look at the report produced by 
our student Vitaly and to discuss it with my colleagues, because of I 
have been finishing my PhD thesis.

After careful analysis of results it became clear that CBMC pointed us 
several bugs in LDV tools, that we are going to fix in near future. So, 
thank you for such the strict checker. At the moment we discovered just 
two deterministic issues in CBMC (svn revision 2982). For several 
drivers we obtained CBMC's assertions. I attached two of these drivers: 
drivers--hid--i2c-hid--i2c-hid.ko.c and drivers--md--dm-mod.ko.c, where 
"/"s were replaced with "--"s. Corresponding commands were:
$ cbmc drivers--hid--i2c-hid--i2c-hid.ko.c --function 
ldv_main0_sequence_infinite_withcheck_stateful --error-label LDV_ERROR 
--unwind 2 --no-unwinding-assertions
and:
$ cbmc drivers--md--dm-mod.ko.c --function 
ldv_main1_sequence_infinite_withcheck_stateful --error-label LDV_ERROR 
--unwind 2 --no-unwinding-assertions --xml-ui
(first driver can be compiled with GCC without any errors, while the 
second one can't be compiled).

Also Vitaly have found few drivers where CBMC works nondeterministically 
on his machine. Sometimes it produces normal results, sometimes 
segmentation faults happen, sometimes CBMC's assertions are violated. On 
my and one another machine we couldn't reproduce this behavior, so I 
didn't attach those drivers. But we are quite interested in whether you 
had something similar before?

We will continue application of CBMC for verification of different 
specifications for Linux drivers and will report you other issues if so. 
And we hope that you will fix these issues.

Now we are investigating Unsafes reported for drivers by CBMC. So, we 
will provide you corresponding results soon, as well as we will ask you 
several questions regarding an information presented in error traces and 
possible CBMC configurations.

Looking ahead, are there any means in CBMC to tune analysis of function 
pointers? Due to we are analyzing incomplete code, not all values of 
function pointers are known, and it is better for us to omit such calls 
at all rather then to call something (and then analyze many false 
positives).

Another question is can we obtain the same information ('function_call' 
and 'function_return' XML elements) for [static] inline functions as for 
non-inline functions? Absence of this information prevents proper 
visualization of error traces and makes analysis of them a bit less 
efficient.

-- 
Best regards, Evgeny Novikov.
Linux Verification Center, ISPRAS
web: http://linuxtesting.org
e-mail: novikov at ispras.ru

-------------- next part --------------
A non-text attachment was scrubbed...
Name: drivers--hid--i2c-hid--i2c-hid.ko.c
Type: text/x-csrc
Size: 213958 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20131010/d3e09301/attachment.c>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: drivers--md--dm-mod.ko.c
Type: text/x-csrc
Size: 746981 bytes
Desc: not available
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20131010/d3e09301/attachment-0001.c>