From 6e94cd550d87a39e24dcf1ff1915a9369a67caff Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 2 Dec 2020 23:03:03 +0100
Subject: [PATCH] [basic-cwe-examples] add another CWE20 example
---
basic-cwe-examples/.frama-c/GNUmakefile | 15 ++-
.../.frama-c/cwe20-2-precise.eva/alarms.csv | 3 +
.../.frama-c/cwe20-2-precise.eva/metrics.log | 11 ++
.../.frama-c/cwe20-2-precise.eva/nonterm.log | 0
.../.frama-c/cwe20-2-precise.eva/warnings.log | 2 +
.../.frama-c/cwe20-2-precise.parse/framac.ast | 112 ++++++++++++++++++
.../cwe20-2-precise.parse/metrics.log | 34 ++++++
.../cwe20-2-precise.parse/warnings.log | 0
.../.frama-c/cwe20-2.eva/alarms.csv | 4 +
.../.frama-c/cwe20-2.eva/metrics.log | 11 ++
.../.frama-c/cwe20-2.eva/nonterm.log | 0
.../.frama-c/cwe20-2.eva/warnings.log | 0
.../.frama-c/cwe20-2.parse/framac.ast | 112 ++++++++++++++++++
.../.frama-c/cwe20-2.parse/metrics.log | 34 ++++++
.../.frama-c/cwe20-2.parse/warnings.log | 0
basic-cwe-examples/Makefile | 2 +-
basic-cwe-examples/cwe20-2.c | 38 ++++++
17 files changed, 371 insertions(+), 7 deletions(-)
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2-precise.eva/alarms.csv
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2-precise.eva/metrics.log
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2-precise.eva/nonterm.log
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2-precise.eva/warnings.log
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2-precise.parse/framac.ast
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2-precise.parse/metrics.log
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2-precise.parse/warnings.log
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2.eva/alarms.csv
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2.eva/metrics.log
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2.eva/nonterm.log
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2.eva/warnings.log
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2.parse/framac.ast
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2.parse/metrics.log
create mode 100644 basic-cwe-examples/.frama-c/cwe20-2.parse/warnings.log
create mode 100644 basic-cwe-examples/cwe20-2.c
diff --git a/basic-cwe-examples/.frama-c/GNUmakefile b/basic-cwe-examples/.frama-c/GNUmakefile
index 787ebe0b5..841b65441 100644
--- a/basic-cwe-examples/.frama-c/GNUmakefile
+++ b/basic-cwe-examples/.frama-c/GNUmakefile
@@ -25,7 +25,7 @@ EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
## Analysis targets (suffixed with .eva)
-IMPRECISE_TARGETS = cwe20.eva cwe119.eva cwe190.eva cwe416.eva cwe787.eva
+IMPRECISE_TARGETS = cwe20.eva cwe20-2.eva cwe119.eva cwe190.eva cwe416.eva cwe787.eva
PRECISE_TARGETS = $(subst .eva,-precise.eva,$(IMPRECISE_TARGETS))
@@ -33,22 +33,25 @@ TARGETS = $(IMPRECISE_TARGETS) $(PRECISE_TARGETS)
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
cwe20.parse: ../cwe20.c
+cwe20-2.parse: ../cwe20-2.c
cwe119.parse: ../cwe119.c
cwe190.parse: ../cwe190.c
cwe416.parse: ../cwe416.c
cwe787.parse: ../cwe787.c
cwe20-precise.parse: ../cwe20.c
+cwe20-2-precise.parse: ../cwe20-2.c
cwe119-precise.parse: ../cwe119.c
cwe190-precise.parse: ../cwe190.c
cwe416-precise.parse: ../cwe416.c
cwe787-precise.parse: ../cwe787.c
-cwe20-precise.eva: EVAFLAGS +=
-cwe119-precise.eva: EVAFLAGS +=
-cwe190-precise.eva: EVAFLAGS += -warn-unsigned-overflow
-cwe416-precise.eva: EVAFLAGS +=
-cwe787-precise.eva: EVAFLAGS += -eva-precision 2
+cwe20-precise.eva: EVAFLAGS +=
+cwe20-2-precise.eva: EVAFLAGS += -eva-precision 5
+cwe119-precise.eva: EVAFLAGS +=
+cwe190-precise.eva: EVAFLAGS += -warn-unsigned-overflow
+cwe416-precise.eva: EVAFLAGS +=
+cwe787-precise.eva: EVAFLAGS += -eva-precision 2
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
diff --git a/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/alarms.csv
new file mode 100644
index 000000000..098937465
--- /dev/null
+++ b/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/alarms.csv
@@ -0,0 +1,3 @@
+directory file line function property kind status property
+. cwe20-2.c 32 main index_bound Unknown 0 ≤ stack_top
+. cwe20-2.c 35 main signed_overflow Unknown account_balance - (int)((int)(amount / 100) * 100) ≤ 2147483647
diff --git a/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/metrics.log
new file mode 100644
index 000000000..b64cce750
--- /dev/null
+++ b/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/metrics.log
@@ -0,0 +1,11 @@
+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 1 (out of 1)
+Semantically reached functions = 1
+Coverage estimation = 100.0%
+[metrics] References to non-analyzed functions
+------------------------------------
+[metrics] Statements analyzed by Eva
+--------------------------
+30 stmts in analyzed functions, 30 stmts analyzed (100.0%)
+main: 30 stmts out of 30 (100.0%)
diff --git a/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/nonterm.log
new file mode 100644
index 000000000..e69de29bb
diff --git a/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/warnings.log b/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/warnings.log
new file mode 100644
index 000000000..4be9b3750
--- /dev/null
+++ b/basic-cwe-examples/.frama-c/cwe20-2-precise.eva/warnings.log
@@ -0,0 +1,2 @@
+cwe20-2.c:32:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
+stack: main
diff --git a/basic-cwe-examples/.frama-c/cwe20-2-precise.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe20-2-precise.parse/framac.ast
new file mode 100644
index 000000000..b45710d0f
--- /dev/null
+++ b/basic-cwe-examples/.frama-c/cwe20-2-precise.parse/framac.ast
@@ -0,0 +1,112 @@
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+#include "stdlib.h"
+int account_balance = 1000;
+int bill_stack[100];
+int stack_top;
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ (indirect: __fc_stdout->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns __fc_stdout->__fc_FILE_data
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_1(char const * __restrict format);
+
+/*@ requires valid_read_string(format);
+ requires \valid(param0);
+ ensures \initialized(param0);
+ assigns \result, __fc_stdin->__fc_FILE_data, *param0;
+ assigns \result
+ \from (indirect: __fc_stdin->__fc_FILE_id),
+ (indirect: __fc_stdin->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns __fc_stdin->__fc_FILE_data
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ assigns *param0
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ */
+int scanf_va_1(char const * __restrict format, int *param0);
+
+/*@ requires valid_read_string(format);
+ assigns \result, stream->__fc_FILE_data;
+ assigns \result
+ \from (indirect: stream->__fc_FILE_id),
+ (indirect: stream->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns stream->__fc_FILE_data
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
+
+/*@ requires valid_read_string(format);
+ assigns \result, stream->__fc_FILE_data;
+ assigns \result
+ \from (indirect: stream->__fc_FILE_id),
+ (indirect: stream->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns stream->__fc_FILE_data
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
+
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ (indirect: __fc_stdout->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param1),
+ (indirect: param0);
+ assigns __fc_stdout->__fc_FILE_data
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+ param1, param0;
+ */
+int printf_va_2(char const * __restrict format, int param0, int param1);
+
+int main(void)
+{
+ int __retres;
+ int error;
+ int amount;
+ {
+ int i = 0;
+ while (i < 100) {
+ bill_stack[i] = 100;
+ i ++;
+ }
+ }
+ stack_top = 100;
+ printf("Please specify the amount to withdraw: \n"); /* printf_va_1 */
+ error = scanf("%d",& amount); /* scanf_va_1 */
+ if (-1 == error) {
+ fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_1 */
+ exit(1);
+ }
+ if (amount > account_balance) {
+ fprintf(__fc_stderr,"Value too large: Die evil hacker!\n"); /* fprintf_va_2 */
+ exit(1);
+ }
+ int withdraw_bills = amount / 100;
+ while (withdraw_bills) {
+ stack_top --;
+ bill_stack[stack_top] = 0;
+ withdraw_bills --;
+ }
+ account_balance -= (amount / 100) * 100;
+ printf("Withdrew $%d, balance: $%d\n",amount,account_balance); /* printf_va_2 */
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/basic-cwe-examples/.frama-c/cwe20-2-precise.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe20-2-precise.parse/metrics.log
new file mode 100644
index 000000000..e8cc33d00
--- /dev/null
+++ b/basic-cwe-examples/.frama-c/cwe20-2-precise.parse/metrics.log
@@ -0,0 +1,34 @@
+[metrics] Defined functions (1)
+=====================
+ main (0 call);
+
+Specified-only functions (0)
+============================
+
+
+Undefined and unspecified functions (0)
+=======================================
+
+
+'Extern' global variables (0)
+=============================
+
+
+Potential entry points (1)
+==========================
+ main;
+
+Global metrics
+==============
+Sloc = 30
+Decision point = 4
+Global variables = 3
+If = 4
+Loop = 2
+Goto = 0
+Assignment = 11
+Exit point = 1
+Function = 1
+Function call = 7
+Pointer dereferencing = 0
+Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe20-2-precise.parse/warnings.log b/basic-cwe-examples/.frama-c/cwe20-2-precise.parse/warnings.log
new file mode 100644
index 000000000..e69de29bb
diff --git a/basic-cwe-examples/.frama-c/cwe20-2.eva/alarms.csv b/basic-cwe-examples/.frama-c/cwe20-2.eva/alarms.csv
new file mode 100644
index 000000000..76b8a04d7
--- /dev/null
+++ b/basic-cwe-examples/.frama-c/cwe20-2.eva/alarms.csv
@@ -0,0 +1,4 @@
+directory file line function property kind status property
+. cwe20-2.c 32 main index_bound Unknown 0 ≤ stack_top
+. cwe20-2.c 33 main signed_overflow Unknown -2147483648 ≤ withdraw_bills - 1
+. cwe20-2.c 35 main signed_overflow Unknown account_balance - (int)((int)(amount / 100) * 100) ≤ 2147483647
diff --git a/basic-cwe-examples/.frama-c/cwe20-2.eva/metrics.log b/basic-cwe-examples/.frama-c/cwe20-2.eva/metrics.log
new file mode 100644
index 000000000..b64cce750
--- /dev/null
+++ b/basic-cwe-examples/.frama-c/cwe20-2.eva/metrics.log
@@ -0,0 +1,11 @@
+[metrics] Eva coverage statistics
+=======================
+Syntactically reachable functions = 1 (out of 1)
+Semantically reached functions = 1
+Coverage estimation = 100.0%
+[metrics] References to non-analyzed functions
+------------------------------------
+[metrics] Statements analyzed by Eva
+--------------------------
+30 stmts in analyzed functions, 30 stmts analyzed (100.0%)
+main: 30 stmts out of 30 (100.0%)
diff --git a/basic-cwe-examples/.frama-c/cwe20-2.eva/nonterm.log b/basic-cwe-examples/.frama-c/cwe20-2.eva/nonterm.log
new file mode 100644
index 000000000..e69de29bb
diff --git a/basic-cwe-examples/.frama-c/cwe20-2.eva/warnings.log b/basic-cwe-examples/.frama-c/cwe20-2.eva/warnings.log
new file mode 100644
index 000000000..e69de29bb
diff --git a/basic-cwe-examples/.frama-c/cwe20-2.parse/framac.ast b/basic-cwe-examples/.frama-c/cwe20-2.parse/framac.ast
new file mode 100644
index 000000000..b45710d0f
--- /dev/null
+++ b/basic-cwe-examples/.frama-c/cwe20-2.parse/framac.ast
@@ -0,0 +1,112 @@
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+#include "stdlib.h"
+int account_balance = 1000;
+int bill_stack[100];
+int stack_top;
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ (indirect: __fc_stdout->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns __fc_stdout->__fc_FILE_data
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
+ */
+int printf_va_1(char const * __restrict format);
+
+/*@ requires valid_read_string(format);
+ requires \valid(param0);
+ ensures \initialized(param0);
+ assigns \result, __fc_stdin->__fc_FILE_data, *param0;
+ assigns \result
+ \from (indirect: __fc_stdin->__fc_FILE_id),
+ (indirect: __fc_stdin->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns __fc_stdin->__fc_FILE_data
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ assigns *param0
+ \from (indirect: __fc_stdin->__fc_FILE_id), __fc_stdin->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ */
+int scanf_va_1(char const * __restrict format, int *param0);
+
+/*@ requires valid_read_string(format);
+ assigns \result, stream->__fc_FILE_data;
+ assigns \result
+ \from (indirect: stream->__fc_FILE_id),
+ (indirect: stream->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns stream->__fc_FILE_data
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_1(FILE * __restrict stream, char const * __restrict format);
+
+/*@ requires valid_read_string(format);
+ assigns \result, stream->__fc_FILE_data;
+ assigns \result
+ \from (indirect: stream->__fc_FILE_id),
+ (indirect: stream->__fc_FILE_data),
+ (indirect: *(format + (0 ..)));
+ assigns stream->__fc_FILE_data
+ \from (indirect: stream->__fc_FILE_id), stream->__fc_FILE_data,
+ (indirect: *(format + (0 ..)));
+ */
+int fprintf_va_2(FILE * __restrict stream, char const * __restrict format);
+
+/*@ requires valid_read_string(format);
+ assigns \result, __fc_stdout->__fc_FILE_data;
+ assigns \result
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ (indirect: __fc_stdout->__fc_FILE_data),
+ (indirect: *(format + (0 ..))), (indirect: param1),
+ (indirect: param0);
+ assigns __fc_stdout->__fc_FILE_data
+ \from (indirect: __fc_stdout->__fc_FILE_id),
+ __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..))),
+ param1, param0;
+ */
+int printf_va_2(char const * __restrict format, int param0, int param1);
+
+int main(void)
+{
+ int __retres;
+ int error;
+ int amount;
+ {
+ int i = 0;
+ while (i < 100) {
+ bill_stack[i] = 100;
+ i ++;
+ }
+ }
+ stack_top = 100;
+ printf("Please specify the amount to withdraw: \n"); /* printf_va_1 */
+ error = scanf("%d",& amount); /* scanf_va_1 */
+ if (-1 == error) {
+ fprintf(__fc_stderr,"No integer passed: Die evil hacker!\n"); /* fprintf_va_1 */
+ exit(1);
+ }
+ if (amount > account_balance) {
+ fprintf(__fc_stderr,"Value too large: Die evil hacker!\n"); /* fprintf_va_2 */
+ exit(1);
+ }
+ int withdraw_bills = amount / 100;
+ while (withdraw_bills) {
+ stack_top --;
+ bill_stack[stack_top] = 0;
+ withdraw_bills --;
+ }
+ account_balance -= (amount / 100) * 100;
+ printf("Withdrew $%d, balance: $%d\n",amount,account_balance); /* printf_va_2 */
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/basic-cwe-examples/.frama-c/cwe20-2.parse/metrics.log b/basic-cwe-examples/.frama-c/cwe20-2.parse/metrics.log
new file mode 100644
index 000000000..e8cc33d00
--- /dev/null
+++ b/basic-cwe-examples/.frama-c/cwe20-2.parse/metrics.log
@@ -0,0 +1,34 @@
+[metrics] Defined functions (1)
+=====================
+ main (0 call);
+
+Specified-only functions (0)
+============================
+
+
+Undefined and unspecified functions (0)
+=======================================
+
+
+'Extern' global variables (0)
+=============================
+
+
+Potential entry points (1)
+==========================
+ main;
+
+Global metrics
+==============
+Sloc = 30
+Decision point = 4
+Global variables = 3
+If = 4
+Loop = 2
+Goto = 0
+Assignment = 11
+Exit point = 1
+Function = 1
+Function call = 7
+Pointer dereferencing = 0
+Cyclomatic complexity = 5
diff --git a/basic-cwe-examples/.frama-c/cwe20-2.parse/warnings.log b/basic-cwe-examples/.frama-c/cwe20-2.parse/warnings.log
new file mode 100644
index 000000000..e69de29bb
diff --git a/basic-cwe-examples/Makefile b/basic-cwe-examples/Makefile
index 824e4eb4e..8062c975b 100644
--- a/basic-cwe-examples/Makefile
+++ b/basic-cwe-examples/Makefile
@@ -1,4 +1,4 @@
-TARGETS=cwe20 cwe119 cwe190 cwe416 cwe787
+TARGETS=cwe20 cwe20-2 cwe119 cwe190 cwe416 cwe787
all: $(TARGETS)
diff --git a/basic-cwe-examples/cwe20-2.c b/basic-cwe-examples/cwe20-2.c
new file mode 100644
index 000000000..8b5e1eafb
--- /dev/null
+++ b/basic-cwe-examples/cwe20-2.c
@@ -0,0 +1,38 @@
+// Inspired by MITRE's CWE-20, demonstrative example 2
+// https://cwe.mitre.org/data/definitions/20.html
+
+#include <stdio.h>
+#include <stdlib.h>
+
+#define die(s) fprintf(stderr, s); exit(1)
+
+int account_balance = 1000;
+#define MAX_BILLS 100
+int bill_stack[MAX_BILLS];
+int stack_top;
+
+int main() {
+ int error, amount;
+
+ for (int i = 0; i < MAX_BILLS; i++) {
+ bill_stack[i] = 100;
+ }
+ stack_top = 100;
+
+ printf("Please specify the amount to withdraw: \n");
+ error = scanf("%d", &amount);
+ if ( EOF == error ){
+ die("No integer passed: Die evil hacker!\n");
+ }
+ if (amount > account_balance) {
+ die("Value too large: Die evil hacker!\n");
+ }
+ int withdraw_bills = amount / 100;
+ while (withdraw_bills) {
+ bill_stack[--stack_top] = 0;
+ withdraw_bills--;
+ }
+ account_balance -= (amount / 100) * 100;
+ printf("Withdrew $%d, balance: $%d\n", amount, account_balance);
+ return 0;
+}
--
GitLab