Skip to content

Draft: (WIP) tinyDTLS verification

contra-bit requested to merge contra-bit/open-source-case-studies:master into master

tinyDTLS

This is a work in progress of merge request for the verification of tinyDTLS. Which is a DTLS library, which focus on minimal resource usage and is well integrated into the IoT operating systems Contiki-NG and RIOT.

I have started the verification for my thesis at the Universität Bremen, since I work in a DFKI research group for cyber physical systems and focus on software verification and generation of ACSL constraints from OCL and UML. My motivation for my thesis is to show, that software verification frameworks such as frama-c can provide security to IoT systems and for me to learn more about the Eva plugin, since before I only used the WP plugin.

Tasks

These are my current Tasks, please add more if you see the need for any.

  • Generate Gnumakefile, which tries to achieve high coverage
  • Write fc_stubs with include
  • Add ACSL to all public functions
    • dtls.h
  • Generate list of loops requiring annotation
  • Write trivial loop ACSL annotations
  • Improve speed for verification

I falsely started verifying the wrong branch of the upstream (master instead of main). In the old branch Frama-C finished its verification within 2 seconds. After switching to the newer branch, the verification takes very long. Now after removing command line argument parsing and adding ACSL to loops the verification runs barely within 15 minutes.

Log Messages

While the verification time is improving there are a lot of messages about imprecise assignments to values of variables. Such as the following:

[eva] dtls.c:293: 
  Assigning imprecise value to _ha_hashv.
  The imprecision originates from Misaligned
  stack: dtls_add_peer :: dtls.c:3915 <-
         handle_0_verified_client_hello :: dtls.c:4001 <-
         handle_0_client_hello :: dtls.c:4306 <-
         dtls_handle_message :: tests/dtls-server.c:189 <-
         dtls_handle_read :: tests/dtls-server.c:398 <-
         main

Why do I get this message, even if I have added string.c in the GNUmakefile?

  The specification of function 'strerror' is currently not supported by Eva.
  Consider adding 'FRAMAC_SHARE/libc/string.c' to the analyzed source files.

Please help me to reduce the time required for the verification, since I feel like I cannot achieve this alone. My goal for today and tomorrow is to annotate all loops.

Please help me answer the following question:

  • Do you think this verification is going in the correct direction?
  • What features of eva or frama-c am I missing?
  • Should I make a request to change the ecc or sha2 implentation, which uses modern c? This week I added parameter names to the function of sha2/sha2.h, since they where all unnamed.

Please make any other suggestion which seem obvious to you.

References

Sadly my log file is too big to upload to GitLab (42mb), so I have uploaded it here so you can more easily spot errors. Until today, I have been working the tinyDTLS tree which you can find on sourcehut. There are 2 Branches. The new one and the old and fast

I am looking forward from hearing from you, and thank you already for taking your time to read my pull request

Edited by contra-bit

Merge request reports