Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>