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: Christian.Flach at student.hpi.uni-potsdam.de (Flach, Christian)
  • Date: Thu, 30 Apr 2020 12:50:59 +0000
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.


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