Commit 6e94cd55 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

[basic-cwe-examples] add another CWE20 example

parent aa2a71da
......@@ -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
......
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
[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%)
cwe20-2.c:32:[kernel] warning: all target addresses were invalid. This path is assumed to be dead.
stack: main
/* 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;
}
[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
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
[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%)
/* 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;
}
[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
TARGETS=cwe20 cwe119 cwe190 cwe416 cwe787
TARGETS=cwe20 cwe20-2 cwe119 cwe190 cwe416 cwe787
all: $(TARGETS)
......
// 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;
}
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