Commit 5126174d authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

[verisec] apply several patches; add Frama-C/Eva analyses

Note: several "ok" tests still contain warnings; in some cases, they seem
inevitable, but others can be improved by adding C stubs, ACSL annotations,
or improving the precision in other ways. They may also contain real bugs
which have not yet been patched.
parent 13d0116f
Pipeline #39681 failed with stage
in 39 minutes and 52 seconds
# Common rules used by all subdirectories
*.sav
*.sav.crash
*.o
*~
config.status
......@@ -14,10 +13,11 @@ stats.txt
flamegraph.txt
*.error
*.break
*#
benchs-value.csv
bench_clone
# .sarif reports are produced as CI artifacts, but we do not want to version
# them, due to their size and the redundancy w.r.t. Eva logs.
# SARIF files are currently not versioned
*.sarif
......@@ -82,6 +82,7 @@ TARGETS=\
solitaire \
tsvc \
tweetnacl-usable \
verisec \
x509-parser \
help::
......
This diff is collapsed.
#include "stubs.h"
// Copied from lib/stubs.c, since these functions are not in
// Frama-C's libc
/*****************************************************************
*
* Functions which are like the functions in libc, but return indexes
* into arrays rather than pointers into arrays. -1 becomes the
* stand-in for NULL, which is hashish and evil in general.
*
****************************************************************/
char *strrand (char *s)
{
int i;
for (i = 0; s[i] != EOS; i++)
if (nondet_int () == 1)
return &s[i];
return NULL;
}
int istrrand (char *s)
{
int i;
for (i = 0; s[i] != EOS; i++)
if (nondet_int () == 1)
return i;
return -1;
}
int istrchr(const char *s, int c)
{
int i;
for (i = 0; s[i] != EOS; i++)
if (s[i] == c)
return i;
return (c == EOS) ? i : -1;
}
int istrrchr(const char *s, int c)
{
int ret = -1;
int i;
for (i = 0; s[i] != EOS; i++)
if (s[i] == c)
ret = i;
if (c == EOS)
return i;
return ret;
}
int istrncmp (const char *s1, int start, const char *s2, size_t n)
{
int i;
int end = start + (n-1);
for (i = start; i < end; i++) {
if (s1[i] == EOS) return 0;
if (s1[i] - s2[i] != 0) return s1[i] - s2[i];
}
assert (i == end); //KK: what's this here for?
return s1[end] - s2[end];
}
int istrstr(const char *haystack, const char *needle)
{
int len;
int i;
int j;
len = 0;
while (needle[len] != EOS) len++;
for (i = 0; haystack[i] != EOS; i++) {
for (j = 0; j < len-1; j++) {
if (haystack[i+j] == EOS) break;
if (haystack[i+j] != needle[j]) break;
}
if (j == len-1 &&
haystack[i+len-1] == needle[len-1])
return i;
}
// Note: the original code returned NULL instead of -1; likely a typo
return -1;
}
../../path.mk
\ No newline at end of file
directory file line function property kind status property
programs/apps/MADWiFi/CVE-2006-6332/encode_ie interproc_bad.c 32 encode_ie mem_access Unknown \valid(p + 1)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 3 (out of 3)
Semantically reached functions = 3
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
35 stmts in analyzed functions, 25 stmts analyzed (71.4%)
giwscan_cb: 5 stmts out of 5 (100.0%)
main: 6 stmts out of 6 (100.0%)
encode_ie: 14 stmts out of 24 (58.3%)
programs/apps/MADWiFi/CVE-2006-6332/encode_ie/interproc_bad.c:20:[nonterm:stmt] warning: non-terminating loop
stack: encode_ie :: programs/apps/MADWiFi/CVE-2006-6332/encode_ie/interproc_bad.c:52 <-
giwscan_cb :: programs/apps/MADWiFi/CVE-2006-6332/encode_ie/interproc_bad.c:71 <-
main
programs/apps/MADWiFi/CVE-2006-6332/encode_ie/interproc_bad.c:32:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: encode_ie :: programs/apps/MADWiFi/CVE-2006-6332/encode_ie/interproc_bad.c:52 <-
giwscan_cb :: programs/apps/MADWiFi/CVE-2006-6332/encode_ie/interproc_bad.c:71 <-
main
/* Generated by Frama-C */
#include "__fc_builtin.h"
#include "assert.h"
#include "ctype.h"
#include "stddef.h"
#include "string.h"
#include "strings.h"
typedef unsigned int u_int;
typedef unsigned char u_int8_t;
struct ieee80211_scan_entry {
u_int8_t *se_rsn_ie ;
};
static u_int encode_ie(void *buf, size_t bufsize, u_int8_t const *ie,
size_t ielen, char const *leader, size_t leader_len)
{
u_int __retres;
u_int8_t *p;
int i;
long tmp;
if (bufsize < leader_len) {
__retres = (unsigned int)0;
goto return_label;
}
p = (u_int8_t *)buf;
memcpy((void *)p,(void const *)leader,leader_len);
bufsize -= leader_len;
p += leader_len;
i = 0;
while (1) {
if ((size_t)i < ielen) {
if (! (bufsize > (size_t)2)) break;
}
else break;
*p = (unsigned char)'x';
*(p + 1) = (unsigned char)'x';
p += 2;
i ++;
}
if ((size_t)i == ielen) tmp = p - (u_int8_t *)buf; else tmp = (long)0;
__retres = (unsigned int)tmp;
return_label: return __retres;
}
static int giwscan_cb(struct ieee80211_scan_entry const *se)
{
int __retres;
u_int8_t buf[(2 + 1) + 2];
char rsn_leader[1];
if (se->se_rsn_ie != (u_int8_t *)0)
if ((int)*(se->se_rsn_ie + 0) == 200) encode_ie((void *)(buf),
sizeof(buf),
(u_int8_t const *)se->se_rsn_ie,
(unsigned long)((int)*(
se->se_rsn_ie + 1) + 2),
(char const *)(rsn_leader),
sizeof(rsn_leader) - (unsigned long)1);
__retres = 0;
return __retres;
}
int main(void)
{
int __retres;
struct ieee80211_scan_entry se;
u_int8_t ie[(((2 + 1) + 2) - 1) + 5];
se.se_rsn_ie = ie;
Frama_C_make_unknown((char *)(ie),(unsigned long)((((2 + 1) + 2) - 1) + 5));
*(se.se_rsn_ie + 1) = (unsigned char)(((((2 + 1) + 2) - 1) + 5) - 2);
giwscan_cb((struct ieee80211_scan_entry const *)(& se));
__retres = 0;
return __retres;
}
[metrics] Defined functions (3)
=====================
encode_ie (1 call); giwscan_cb (1 call); main (0 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (1)
==========================
main;
Global metrics
==============
Sloc = 35
Decision point = 6
Global variables = 0
If = 6
Loop = 1
Goto = 1
Assignment = 16
Exit point = 3
Function = 3
Function call = 4
Pointer dereferencing = 9
Cyclomatic complexity = 9
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 3 (out of 3)
Semantically reached functions = 3
Coverage estimation = 100.0%
[metrics] Statements analyzed by Eva
--------------------------
39 stmts in analyzed functions, 21 stmts analyzed (53.8%)
giwscan_cb: 5 stmts out of 5 (100.0%)
main: 6 stmts out of 6 (100.0%)
encode_ie: 10 stmts out of 28 (35.7%)
/* Generated by Frama-C */
#include "__fc_builtin.h"
#include "assert.h"
#include "ctype.h"
#include "stddef.h"
#include "string.h"
#include "strings.h"
typedef unsigned int u_int;
typedef unsigned char u_int8_t;
struct ieee80211_scan_entry {
u_int8_t *se_rsn_ie ;
};
static u_int encode_ie(void *buf, size_t bufsize, u_int8_t const *ie,
size_t ielen, char const *leader, size_t leader_len)
{
u_int __retres;
u_int8_t *p;
int i;
long tmp;
if (bufsize < leader_len) {
__retres = (unsigned int)0;
goto return_label;
}
p = (u_int8_t *)buf;
memcpy((void *)p,(void const *)leader,leader_len);
bufsize -= leader_len;
p += leader_len;
if (bufsize < ielen) {
__retres = (unsigned int)0;
goto return_label;
}
i = 0;
while (1) {
if ((size_t)i < ielen) {
if (! (bufsize > (size_t)2)) break;
}
else break;
*p = (unsigned char)'x';
*(p + 1) = (unsigned char)'x';
p += 2;
i ++;
}
if ((size_t)i == ielen) tmp = p - (u_int8_t *)buf; else tmp = (long)0;
__retres = (unsigned int)tmp;
return_label: return __retres;
}
static int giwscan_cb(struct ieee80211_scan_entry const *se)
{
int __retres;
u_int8_t buf[(2 + 1) + 2];
char rsn_leader[1];
if (se->se_rsn_ie != (u_int8_t *)0)
if ((int)*(se->se_rsn_ie + 0) == 200) encode_ie((void *)(buf),
sizeof(buf),
(u_int8_t const *)se->se_rsn_ie,
(unsigned long)((int)*(
se->se_rsn_ie + 1) + 2),
(char const *)(rsn_leader),
sizeof(rsn_leader) - (unsigned long)1);
__retres = 0;
return __retres;
}
int main(void)
{
int __retres;
struct ieee80211_scan_entry se;
u_int8_t ie[(((2 + 1) + 2) - 1) + 5];
se.se_rsn_ie = ie;
Frama_C_make_unknown((char *)(ie),(unsigned long)((((2 + 1) + 2) - 1) + 5));
*(se.se_rsn_ie + 1) = (unsigned char)(((((2 + 1) + 2) - 1) + 5) - 2);
giwscan_cb((struct ieee80211_scan_entry const *)(& se));
__retres = 0;
return __retres;
}
[metrics] Defined functions (3)
=====================
encode_ie (1 call); giwscan_cb (1 call); main (0 call);
Specified-only functions (0)
============================
Undefined and unspecified functions (0)
=======================================
'Extern' global variables (0)
=============================
Potential entry points (1)
==========================
main;
Global metrics
==============
Sloc = 39
Decision point = 7
Global variables = 0
If = 7
Loop = 1
Goto = 2
Assignment = 17
Exit point = 3
Function = 3
Function call = 4
Pointer dereferencing = 9
Cyclomatic complexity = 10
directory file line function property kind status property
programs/apps/MADWiFi/CVE-2006-6332/encode_ie no_sprintf_bad.c 30 encode_ie mem_access Unknown \valid(p)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment