--- layout: fc_discuss_archives title: Message 114 from Frama-C-discuss on November 2013 ---
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>