Formal verification of your test suite

[jakub-zwolakowski]

Hi, I'm Jakub from TrustInSoft, an advanced source code analyzer publisher for C and C++. I set up TrustInSoft CI on your tests: https://ci.trust-in-soft.com/projects/jakub-zwolakowski/tinycrypt/

I have found some issues in your code. Here you can check out the issues in TrustInSoft CI (first link in each line) and see your source code for reference (second link in each line):

1) Signed overflow (due to implicit integer conversion) in file 'lib/source/aes_encrypt.c' line 86
2) Invalid memory access (out of bounds read, as a consequence of the wrong length given in the test) in file 'lib/source/utils.c' line 44
3) Invalid pointer arithmetic (pointer arithmetic inside object, computing &array[-1]) in file 'lib/source/cmac_mode.c' line 89
4) Another signed overflow (due to implicit integer conversion) in file 'lib/source/ctr_mode.c' line 61
5) Another invalid pointer arithmetic (inside object, computing &array[-1]) in file 'lib/source/ecc.c' line 238
6) Uninitialized memory (read) in file 'lib/source/sha256.c' line 174

Can you let me know if you find those findings interesting? Would you assess them as harmless or dangerous?

TrustInSoft CI is a new tool based on formal methods. We're currently testing it on Open Source projects so any of your feedback will be greatly appreciated.