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] Issues with analyzing the nginx webserver using the eva plugin

  • Subject: [Frama-c-discuss] Issues with analyzing the nginx webserver using the eva plugin
  • From: David.MENTRE at bentobako.org (David MENTRÉ)
  • Date: Sun, 3 May 2020 18:28:26 +0200
  • In-reply-to: <41c953e4459b4169bf2c3270395c06cd@student.hpi.uni-potsdam.de>
  • References: <41c953e4459b4169bf2c3270395c06cd@student.hpi.uni-potsdam.de>
Hello Christian,

In short, you are starting with a very complex project : nginx is big
and complex code and EVA is not designed to analyze such kind of code
(EVA target is safety critical embedded code, with very few library
calls, no dynamic memory allocation and no recursion). You might be able
to analyze and get result on some parts of nginx, although due to the
use of many library calls it might not be that easy.

Nonetheless, here are some hints:

  * At any time, you can stop an analysis using "kill -USR1
    pid-of-frama-c-process". It saves the intermediate result in
    analyzed.sav.errors file and you can then use "frama-c-gui -load
    analyzed.sav.errors" to load the analyze and try to see what is
    going on (not analyzed code appear as red unreachable code and the
    degeneration points appear as yellow & orange)
  * When you are seeing message like "Assigning imprecise value to ...",
    it means EVA is losing precision on the way the program is doing
    memory copies. Most of the time, it means that EVA has completely
    lost track of what the program is doing and you won't get any
    meaningful result afterwards
  * In the same way, if EVA runs more than a few hours, most of the time
    you won't get much of it
  * As far as I know, the default parameters make the quickest analysis,
    at the expense of lack of precision. You probably won't get better
    than that
  * EVA is inherently single core application. The only way to use
    multiple core is to cut your program into smaller parts and analyze
    separately each part

If nginx has some parts of code that does not do dynamic memory
allocation and do not manipulate too much pointers, maybe you can use
EVA on them.


Best regards,
david


Le 30/04/2020 à 14:50, Flach, Christian a écrit :
> Hello everyone,
>
> I am trying to use Frama-C for analyzing the nginx webserver. I have
> not used Frama-C before.
>
> My goal is to be able to answer questions like "why would the
> webserver respond with status code 200, given an incoming request and
> the webserver configuration?". On a C-level, that would mean questions
> like: "what configuration struct fields will lead to the status field
> of the response struct being set to 200?" or "which configuration
> struct fields influence the response header field in the response struct".
>
> I would hope to be able to answer these questions by using static
> analysis of nginx. Frama-C (and its eva plugin) should be able to
> answer these questions, if I'm not mistaken.
>
> I was able to successfully parse the source code with Frama-C. I got
> most of it working by following this blog post [1] and copied the
> other necessary parts from header files on my system.
>
> I am stuck with running the eva plugin. I was able to successfully run
> it when I parsed only a subset of nginx's source files. Running eva
> took less than 3 hours and seemed to work. However, when I try to run
> the eva plugin after parsing a bigger set of nginx source files, it
> never finishes:
>
> I have let eva run for 40 hours on a 4,4GHz CPU and it didn't finish.
> While I see lot's of logging happening in the first ~3 hours, there is
> a gap between log messages of 15-60 minutes after that.
>
> My issue is that I have no idea
> - whether the analysis is actually ongoing when running it that long
> or stuck in some sort of loop
> - how close the analysis is to finishing / how much progress has been made
> - whether there is anything I can configure to make the analysis
> finish faster or run on more than one core
>
> For reference, this is how I parse the code and execute the eva plugin
> [2]. I also see hundreds, of lines like this [3]. Maybe Frama-C is
> choking on nginx's heavy use of dynamic allocations and memory pooling?
>
> Do you have any advice for running eva on a big project like nginx?
> Are there command line options that I am missing that might help with
> figuring out if something is wrong? Are there any additional options
> to make the analysis faster by giving up some precision? I also want
> to make clear that I am not trying to proof or verify any nginx
> properties; approximations are fine to some degree.
>
>
> Best
> Christian
> (apologies if you received this email twice - it appears like I first
> used the wrong email address)
>
>
> [1]
> http://blog.frama-c.com/index.php?post/2018/07/06/Parsing-realistic-code-bases-with-Frama-C
>
>
> [2]
>
> export FRAMA_C_MEMORY_FOOTPRINT=10
>
> # Parsing
>
> CPP_EXTRA_ARGS="-include../ext-include/__fc_stubs.h -I ../ext-include
> -I src/core -I src/event -I src/event/modules -I src/os/unix -I objs
> -I src/http -I src/http/modules -DNGX_HAVE_GMTOFF=0
> -DNGX_HAVE_O_PATH=0 -DNGX_ZLIB=0 -DNGX_HAVE_TCP_INFO=0
> -DNGX_HAVE_MEMALIGN=0 -DNGX_HAVE_POSIX_MEMALIGN=0
> -DNGX_HAVE_IP_PKTINFO=0 -DNGX_HAVE_GNU_CRYPT_R=0 -DNGX_HAVE_EPOLL=0
> -DNGX_HAVE_EPOLLEXCLUSIVE=0 -DNGX_HAVE_ACCEPT4=0"
>
> frama-c -metrics -cpp-extra-args="$CPP_EXTRA_ARGS" \
>         -kernel-warn-key annot:missing-spec=abort \
>         -kernel-warn-key typing:implicit-function-declaration=abort \
>         -save=$OUTPATH/parsed.sav $FILES | tee $OUTPATH/parse.log
>
> # EVA
>
> frama-c -load $OUTPATH/parsed.sav \
>         -main main \
>         -eva \
>         -eva-ignore-recursive-calls \
>         -eva-use-spec=ngx_log_error_core \
>         -eva-warn-key builtins:missing-spec=abort \
>         -eva-warn-key alarm=inactive \
>         -save=$OUTPATH/analyzed.sav | tee $OUTPATH/analyze.log
>
> [3]
>
> [eva] src/core/ngx_string.c:273: 
> Assigning imprecise value to *tmp_4
>   (pointing to ngx_errlog_module with offsets [0..792],0%8;
>   ngx_core_module with offsets [0..792],0%8;
>   init_cycle with offsets [0..2488],0%8;
>   ngx_conf_module with offsets [0..792],0%8;
>   ngx_http_header_filter_module with offsets [0..792],0%8;
>   ngx_debug_points with offsets [0..280],0%8;
>   ngx_core_commands with offsets [0..3800],0%8;
>   ngx_core_module_ctx with offsets [0..120],0%8;
>   ngx_errlog_commands with offsets [0..440],0%8;
>   ngx_errlog_module_ctx with offsets [0..120],0%8;
>   ngx_log with offsets [0..312],0%8; ngx_log_file with offsets
> [0..152],0%8;
>   ngx_conf_commands with offsets [0..440],0%8;
>   ngx_syslog_dummy_log with offsets [0..312],0%8;
>   ngx_syslog_dummy_event with offsets [0..408],0%8;
>   ngx_http_header_filter_module_ctx with offsets [0..248],0%8;
>   __malloc_ngx_alloc_l22 with offsets [0..8184];
>   __malloc_ngx_alloc_l22_2 with offsets [0..408];
>
>    ... 100s to 1000s more malloc lines go here ...
>
>   __malloc_ngx_alloc_l22_7196; __malloc_ngx_alloc_l22_7197;
>   __malloc_w_ngx_alloc_l22_7198; __malloc_w_ngx_alloc_l22_7199;
>   __malloc_w_ngx_alloc_l22_7200}
>   because of Misaligned.
>
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200503/47bc03bf/attachment-0001.html>