--- layout: fc_discuss_archives title: Message 114 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C on Linux Kernel



I am a PhD student actually, and I am now planning to work on a project of
analyzing TCP protocol in Linux kernel with static taint analysis. I think
it needs sound static analysis technique. I tried Clang+LLVM analyzer, but
it cannot handle GNU extensions.... So now I am considering Frama-C.
I think I have enough time to delve into it. Do you have any
suggestions/links for a starter? Thank you sooooo much!!
Alfred


On Mon, Nov 18, 2013 at 5:54 PM, Pascal Cuoq <pascal.cuoq at gmail.com> wrote:

> Hello,
>
> On Mon, Nov 18, 2013 at 11:34 PM, Qi Alfred Chen <alfchen at umich.edu>wrote:
>
>> Hi, I am new in Frama-C, and before getting my hands dirty, I want to
>> make sure that Frama-C is the best tool I need. My target is to do static
>> analysis like static taint analysis, data flow analysis, etc. on Linux
>> kernel code, so can anyone tell me that whether Frama-C can be successfully
>> used to analyse Linux kernel code? It should be difficult due to various
>> GNU extension, not sure whether Frama-C can handle that...
>>
>
> Several Linux modules have already been analyzed or are being analyzed in
> Frama-C.
> Indeed, Linux uses many GCCisms. Since the work on Linux modules is
> recent, you would encounter some of the same bugs and limitations that have
> already been encountered and fixed in the development version of Frama-C.
> You would also encounter new bugs and limitations, because you wouldn't be
> doing exactly the same thing that has already been done.
>
> I should however temper the above moderate optimism by a warning: you
> cannot analyze even a well-delimited Linux module as your first Frama-C
> project. Even if you are familiar with Linux, you would need to have
> practiced Frama-C with C programs of increasing difficulty and learned how
> to use each of the available plug-ins, and how to tackle the various
> difficulties that can present themselves. The good news is that while you
> would be doing that, a new version would probably arrive, fixing at least
> the bugs and limitations that have already been encountered.
>
> How much time do you have to get to the point where you will be ready to
> analyze (a bit of) the Linux kernel? What alternatives do you have? Do you
> really need a sound static analyzer for what you ultimately intend to do,
> or would it make more sense to use less demanding techniques?
>
> Best regards,
>
> Pascal
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>



-- 
Kind regards,
Qi Alfred Chen
PhD Student,
Department of Electrical Engineering and Computer Science,
University of Michigan - Ann Arbor, 48105
Tel: 1-734-834-2916
Alt. Email: adios737 at gmail.com
Homepage: www.eecs.umich.edu/~alfchen
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131118/1da8ee18/attachment-0001.html>