[ldv-project] [cif of ldv] -- does the cif deal with the system calls or interrupts?

[Evgeny Novikov]

On 12/26/2012 05:44 AM, Jian Liu/ISCAS wrote:
>
>> -----Original Message-----
>> From: Evgeny Novikov [mailto:novikov at ispras.ru]
>> Sent: Tuesday, December 25, 2012 11:42 PM
>> To: 'MA Lele'
>> Cc: liujian at iscas.ac.cn; ldv-project
>> Subject: Re: [cif of ldv] -- does the cif deal with the system calls or interrupts?
>>
>>
>> this is actually the case, LDV does need a Linux operating system model as well as
>> SDV. At the moment we have implemented just a small part of this model. The
>> rest part of the model is considered as undefined. For instance, here
>> (http://linuxtesting.ru/ldv/online?action=detailed_report&trace_id=195&number
>> =22)
>> you can see that call to spi_register_driver isn't actually "executed"
>> inside wl12xx_init. So all possible return values of spi_register_driver are analyzed.
>> The error trace visualized corresponds to the case when spi_register_driver
>> returns 0 that allows to continue driver initialization and following processing.
> Hi Evgeny, Thanks for your good example!
>
> I have several questions about above topic.
>
> 1) What parts of model do you support now? Could you give a brief introduction.
We support models for functions that process errors passed through 
pointers, for some GCC special functions and for some kernel functions.
> 2) Could you point out where is source code of this model in LDV releases. To my knowledge about BLAST, I think there should be a closed program generated for its input before the real static analysis. So, where is code to assemble a target drive function with the model codes to a closed program for BLAST?
These models are in different files inside "kernel-rules" directory. 
They are applied to driver source code during instrumentation as well as 
rule models (they are actually parts of rule models).
> 3) You said now just a small part of this model has been implemented. So, how do you deal with problems if one target drive call some functions outside of your model? I think maybe LDV could not deal with such cases now.
>
We are investigating how to deal with that. At the moment everything 
nondetermined is considered just as nondetermined.
>> Now we are actively investigated an approach to automatically extract Linux
>> operating system model for some of our rules. For instance, this will allow to check
>> might sleep functions in spinlock context. IMHO this is almost impossible to write
>> full Linux operating system model since Linux API isn't stable and it's huge in
>> comparison with the Microsoft Windows one.
> It is very interesting work, though I am not familiar about this topic. If there are some similar work in other team e.g. SDV, could you give us a brief introduction about related work? Thanks again.
>
I think that static verifier developers don't like this since this 
approach looses accuracy. But there is almost impossible to analyze all 
driver/kernel relevant code in a reasonable time. So we have to think 
about some workarounds. As for similar work, I guess that this approach 
is widely used by "lightweight" static analyzers. These tools walk 
through source code of functions and create annotations for them, i.e. 
some description like function may return NULL, etc.
>> As for CIF it just does what it's asked for, i.e. it applies aspects to driver source
>> code. Nevertheless one can use CIF to obtain some knowledge about, say, Linux
>> kernel source code, e.g. about whether a given function is might sleep or not.
> It is similar to counterpart in LDV. Here, what you said a function is sleep means that the function is a orphan code, which cannot be reachable.
>
> Best,
>
>      Jian
>
>


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