Commit 6f9d83d2 authored by Dario Pinto's avatar Dario Pinto
Browse files

add WordCompletion

parent dc74d1ee
# Makefile template for Frama-C/Eva case studies.
# For details and usage information, see the Frama-C User Manual.
### Prologue. Do not modify this block. #######################################
-include path.mk
FRAMAC ?= frama-c
include $(shell $(FRAMAC)-config -scripts)/prologue.mk
###############################################################################
# Edit below as needed. MACHDEP is mandatory. Suggested flags are optional.
MACHDEP = x86_32
## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS += \
-DPATCHED \
-D__FC_PATCHED \
-I../../lib \
-I../src \
## General flags
FCFLAGS += \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
-absolute-valid-range 0x4347C000-0x4347FFFF \
-c11 \
## Eva-specific flags
EVAFLAGS += \
-eva-warn-key builtins:missing-spec=abort \
-eva-slevel 120 \
-eva-precision 4 \
## GUI-only flags
FCGUIFLAGS += \
-add-symbolic-path=.:..,CGC_LIB:../../lib \
## Analysis targets (suffixed with .eva)
TARGETS = WordCompletion.eva
### Each target <t>.eva needs a rule <t>.parse with source files as prerequisites
WordCompletion.parse: \
../../lib/common.c \
../../lib/libcgc.c \
../src/main.c \
### Epilogue. Do not modify this block. #######################################
include $(shell $(FRAMAC)-config -scripts)/epilogue.mk
###############################################################################
directory file line function property kind status property
CGC_LIB libcgc.c 28 cgc_transmit precondition of write Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
FRAMAC_SHARE/libc string.h 137 strcmp precondition Unknown valid_string_s1: valid_read_string(s1)
FRAMAC_SHARE/libc unistd.h 1133 write precondition Unknown buf_has_room: \valid_read((char *)buf + (0 .. count - 1))
src main.c 107 cgc_readline mem_access Unknown \valid(buf + count)
src main.c 327 cgc_scramble mem_access Unknown \valid_read(src + i)
src main.c 403 main precondition of strcmp Unknown valid_string_s1: valid_read_string(s1)
src main.c 427 main precondition of strcmp Unknown valid_string_s1: valid_read_string(s1)
[metrics] Eva coverage statistics
=======================
Syntactically reachable functions = 15 (out of 48)
Semantically reached functions = 15
Coverage estimation = 100.0%
[metrics] References to non-analyzed functions
------------------------------------
[metrics] Statements analyzed by Eva
--------------------------
295 stmts in analyzed functions, 267 stmts analyzed (90.5%)
cgc_RANDOM: 2 stmts out of 2 (100.0%)
cgc_allocate: 9 stmts out of 9 (100.0%)
cgc_my_srand: 2 stmts out of 2 (100.0%)
cgc_receive: 9 stmts out of 9 (100.0%)
cgc_toInt: 22 stmts out of 22 (100.0%)
cgc_transmit: 9 stmts out of 9 (100.0%)
cgc_transmit_str: 3 stmts out of 3 (100.0%)
main: 61 stmts out of 65 (93.8%)
cgc_init: 42 stmts out of 45 (93.3%)
cgc_readline: 21 stmts out of 24 (87.5%)
cgc_rotN: 21 stmts out of 24 (87.5%)
cgc_scramble: 35 stmts out of 41 (85.4%)
cgc_transmit_all_zPcz: 17 stmts out of 20 (85.0%)
cgc_strrotcpy: 13 stmts out of 18 (72.2%)
cgc__terminate: 1 stmts out of 2 (50.0%)
CGC_LIB/libcgc.c:23:[nonterm] warning: unreachable implicit return
[metrics] Defined functions (40)
======================
calloc_Pvz (0 call); cgc_RANDOM (2 calls); cgc__terminate (7 calls);
cgc_allocate (2 calls); cgc_check_timeout (1 call);
cgc_copy_cgc_fd_set (2 calls); cgc_copy_os_fd_set (2 calls);
cgc_deallocate (0 call); cgc_fdwait (0 call); cgc_fill_buffer (1 call);
cgc_get_char (1 call); cgc_init (1 call); cgc_my_srand (1 call);
cgc_random (0 call); cgc_read_n_bytes (0 call);
cgc_read_until_delim_or_n (1 call); cgc_readline (4 calls);
cgc_receive (5 calls); cgc_receive_all (0 call); cgc_recv (0 call);
cgc_rotN (1 call); cgc_scramble (2 calls); cgc_sendall (1 call);
cgc_sendline (0 call); cgc_strrotcpy (1 call); cgc_toInt (2 calls);
cgc_transmit (4 calls); cgc_transmit_all (0 call);
cgc_transmit_all_zPcz (3 calls); cgc_transmit_str (9 calls);
cgc_try_init_prng (1 call); int2str_dPcdd (0 call); main (0 call);
receive_bytes_iPcz (0 call); str2int_dPc (0 call); str2uint_ud32Pc (0 call);
strcpy_zPcPc (0 call); strncpy_zPcPcz (0 call); strtok_PcPcc (0 call);
uint2str_dPcdud32 (0 call);
Undefined functions (8)
=======================
cgc_aes_get_bytes (1 call); cgc_init_prng (1 call);
cgc_initialize_flag_page (0 call); cgc_prng (0 call); cgc_recvline (0 call);
cgc_recvuntil (0 call); cgc_streq (0 call); seed_prng (0 call);
'Extern' global variables (0)
=============================
Potential entry points (18)
===========================
calloc_Pvz; cgc_deallocate; cgc_fdwait; cgc_random; cgc_read_n_bytes;
cgc_receive_all; cgc_recv; cgc_sendline; cgc_transmit_all; int2str_dPcdd;
main; receive_bytes_iPcz; str2int_dPc; str2uint_ud32Pc; strcpy_zPcPc;
strncpy_zPcPcz; strtok_PcPcc; uint2str_dPcdud32;
Global metrics
==============
Sloc = 786
Decision point = 140
Global variables = 8
If = 140
Loop = 25
Goto = 74
Assignment = 316
Exit point = 40
Function = 48
Function call = 81
Pointer dereferencing = 62
Cyclomatic complexity = 180
../../frama-c-cgc-path.mk
\ No newline at end of file
# WordCompletion
@Author: Lok Yan <Lok.Yan@us.af.mil>
@Group: AFRL
## Description:
This is a word completion game with 10 initial rounds and a final round. During each round, the user is given an occluded word. The user then needs to provide the full word in order to pass. Once the user completes 10 of these word completion tasks, they will be presented with a final word that must also be solved.
## Vulnerability Class:
The vulnerability is an [CWE-125: Out of Bounds Read](http://cwe.mitre.org/data/definitions/125.html) on an array.
## Additional Notes:
This CB is designed to help CRSes determine how well they handle dynamically generated data. That is the word completion list is created dynamically using a static list of words that are provided as part of the program itself.
//#The following is a list of quotes from the American Film Institute's 100 Years... 100 Movie Quotes. The quotes were retrieved from Wikipedia <http://en.wikipedia.org/wiki/AFI's_100_Years...100_Movie_Quotes>. A few truncations were made so the sentences fit into 64 characters. Also we only used the first 50 quotes in reverse chronological order.
char* gSeedWords[] = {
"My precious.",
"I see dead people.",
"I'm the kind of the world!",
"Show me the money!",
"You had me at hello.",
"Houston, we have a problem.",
"Mama always said life was like a box of chocolates.",
"You can't handle the truth!",
"There's no crying in baseball!",
"A census taker once tried to test me.",
"Hasta la vista, baby.",
"I'll have what she's having.",
"If you build it, he will come.",
"Carpe diem. Seize the day, boys.",
"Greed, for lack of a better word, is good.",
"Snap out of it!",
"Nobody puts Baby in a corner.",
"I feel the need-the need for speed!",
"I'll be back.",
"Go ahead, make my day.",
"Say hello to my little friend!",
"E.T. phone home.",
"They're here!",
"No wire hangers, ever!",
"Listen to me, mister. You're my knight in shining armor.",
"Here's Johnny!",
"I am serious...and don't call me Shirley.",
"Cinderella story. Outta nowhere.",
"I love the smell of napalm in the morning.",
"Toga! Toga!",
"May the Force be with you.",
"La-dee-da, la-dee-da.",
"You talkin' to me?",
"I'm as mad as hell, and I'm not going to take this anymore!",
"Is it safe?",
"Yo, Adrian!",
"You're gonna need a bigger boat.",
"Attica! Attica!",
"Keep your friends close, but your enemies closer.",
"Forget it, Jake, it's Chinatown.",
"Soylent Green is people!",
"I'm going to make him an offer he can't refuse.",
"You've got to ask yourself one question: 'Do I feel lucky?'",
"Love means never having to say you're sorry",
"I'm walking here! I'am walking here!",
"Get your stinking paws off me, you damned dirty ape.",
"Open the pod bay doors please, HAL.",
"Hello, gorgeous.",
"What we've got here is failure to communicate.",
"They call me Mister Tibbs!",
"We rob banks.",
};
#include "libcgc.h"
#include "common.h"
#include "cgc_words.h"
typedef unsigned int uint32_t;
#define PAGE_SIZE 4096
char gValidChars[] = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789";
#define VALID_CHARS_LEN (sizeof(gValidChars) - 1)
#define IS_VALID_CHAR(_c) ( ((_c >= 'a') && (_c <= 'z')) || ((_c >= 'A') && (_c <= 'Z')) || ((_c >= '0') && (_c <= '9')) )
#define NUM_WORDS (sizeof(gSeedWords) / sizeof(char*))
#define NUM_ROUNDS 10
#define ENTER_NUM_MSG "Please Enter a 2 Digit Number\n"
#define WORD_MSG "Word: "
#define LOSE_MSG "You Lose\n"
#define WIN_MSG "You Win!\n"
#define NEXT_WORD_MSG "Next Word: "
#define FINAL_RND_MSG "Final Round. Chose another 2 digit number\n"
/*
size_t strlen(char* str)
{
size_t ret = 0;
if (str == NULL)
{
return (0);
}
for (ret = 0; str[ret] != '\0'; ret++)
{
}
return (ret);
}
*/
size_t cgc_transmit_all_zPcz(char* buf, size_t size)
{
size_t rx_bytes = 0;
size_t total = 0;
int ret = 0;
if (buf == NULL)
{
return (0);
}
do
{
ret = cgc_transmit(STDOUT, buf, size - total, &rx_bytes);
if ( (ret != 0) || (rx_bytes == 0) )
{
cgc__terminate(1);
}
total += rx_bytes;
}
while (total < size);
return (size);
}
size_t cgc_transmit_str(char* buf)
{
size_t len = strlen(buf);
return (cgc_transmit_all_zPcz(buf, len));
}
size_t cgc_receive_all(char* buf, size_t size)
{
size_t rx_bytes = 0;
size_t total = 0;
int ret = 0;
if (buf == NULL)
{
return (0);
}
do
{
ret = cgc_receive(STDIN, buf, size-total, &rx_bytes);
if ( (ret != 0) || (rx_bytes == 0) )
{
cgc__terminate(1);
}
total += rx_bytes;
}
while (total < size);
return (size);
}
size_t cgc_readline(char* buf, size_t len)
{
if (buf == NULL)
{
return (0);
}
size_t count = 0;
int ret = 0;
char c = 0;
size_t rx_bytes = 0;
do
{
ret = cgc_receive(STDIN, &c, 1, &rx_bytes);
if ( (ret != 0) || (rx_bytes == 0) )
{
cgc__terminate(1);
}
buf[count] = c;
count++;
} while ( (c != '\n') && (count < len) );
return (count);
}
char cgc_rotN(char c, int n)
{
int temp = 0;
n = n % VALID_CHARS_LEN;
if ( (c >= 'a') && (c <= 'z') )
{
temp = c - 'a'; //temp is the offset
}
else if ( (c >= 'A') && (c <= 'Z') )
{
temp = c - 'A' + 26;
}
else if ( (c >= '0') && (c <= '9') )
{
temp = c - '0' + 52;
}
else
{
return (c); //no rotation
}
temp += n;
temp = temp % VALID_CHARS_LEN;
return (gValidChars[temp]);
}
size_t cgc_strrotcpy(char* dst, char* src, int rot)
{
if ( (src == NULL) || (dst == NULL) )
{
return (0);
}
size_t ret = 0;
for (ret = 0; src[ret] != '\0'; ret++)
{
dst[ret] = cgc_rotN(src[ret], rot);
}
dst[ret] = '\0';
return (ret);
}
char** cgc_gWords = NULL;
char* cgc_gWordData = NULL;
int cgc_init(int rot)
{
int ret = 0;
size_t numWords = NUM_WORDS;
//first allocate enough space for the wordlist
ret = cgc_allocate( sizeof(gSeedWords), 0, (void**)(&cgc_gWords));
if (ret != 0)
{
return (ret);
}
//now calculate how many bytes we need to store the words themselves
size_t total = 0;
int i = 0;
for (i = 0; i < numWords; i++)
{
total += strlen(gSeedWords[i]);
total += 1; //for the NULL character
}
ret = cgc_allocate(total, 0, (void**)(&cgc_gWordData));
if (ret != 0)
{
return (ret);
}
//now that we have both we can fill in the data
size_t temp = 0;
char* pTemp = cgc_gWordData;
for (i = 0; i < numWords; i++)
{
cgc_gWords[i] = pTemp;
pTemp += cgc_strrotcpy(pTemp, gSeedWords[i], rot);
pTemp += 1; //for the NULL character
}
#ifdef __FC_PATCHED
for ( ; i < (sizeof(gSeedWords) / sizeof(char*)); i++)
{
cgc_gWords[i] = 0;
}
#else
for ( ; i < (PAGE_SIZE / sizeof(char*)); i++)
{
cgc_gWords[i] = 0;
}
#endif
return (0);
}
int cgc_toInt(char c1, char c2)
{
int ret = 0;
if ( (c1 >= '0') && (c1 <= '9') )
{
ret = c1 - '0';
if ( (c2 >= '0') && (c2 <= '9') )
{
ret *= 10;
ret += c2 - '0';
return (ret);
}
else if (c2 != '\0')
{
return (ret);
}
else
{
return (0);
}
}
return (0);
}
/** This LFSR pesudo random number generator is from Bruce Schneier's
* 1992 article in Dr. Dobbs www.schneier.com/paper-pseudorandom-sequence.html
* As the article says, this is not a very good generator. But it is good
* enough for our purposes
* Instead of just returning the last bit, we return the whole uint32
**/
static uint32_t gRandRegister = 0xDA2bAC9C;
uint32_t cgc_RANDOM()
{
gRandRegister = ((((gRandRegister >> 31)
^ (gRandRegister >> 6)
^ (gRandRegister >> 4)
^ (gRandRegister >> 2)
^ (gRandRegister >> 1)
^ gRandRegister)
& 0x00000001)
<< 31)
| (gRandRegister >> 1);
return (gRandRegister);
}
/*
int strcmp(char* s1, char* s2)
{
if (s1 == NULL)
{
if (s2 == NULL)
{
return (0);
}
else
{
return (-1);
}
}
if (s2 == NULL)
{
return (1);
}
int i = 0;
while (s1[i] != '\0')
{
if (s2[i] == '\0')
{
return (1);
}
if (s1[i] < s2[i])
{
return (-1);
}
else if (s1[i] > s2[i])
{
return (1);
}
i++;
}
if (s2[i] == '\0')
{
return (0);
}
return (-1);
}
*/
void cgc_my_srand(uint32_t seed)
{
gRandRegister = seed;
}
void cgc_scramble(char* dst, char* src, size_t len)
{
#if PATCHED
if ( (dst == NULL) || (src == NULL) )
{
return;
}
#endif
#ifdef __FC_PATCHED
int len_src = strlen(src);
#endif
int i = 0;
uint32_t r = (cgc_RANDOM() % 3) + 2;
#ifdef __FC_PATCHED
while ( (src[i] != '\0') && (i < len) && (i < len_src) )
#else
while ( (src[i] != '\0') && (i < len) )
#endif
{
if (IS_VALID_CHAR(src[i]))
{
if (i % r)
{
dst[i] = src[i];
}
else
{
dst[i] = '_';
}
}
else
{
dst[i] = src[i];
}
i++;
}
#ifdef __FC_PATCHED
dst[len - 1] = '\0';
#else
dst[i] = '\0';
#endif
}
int main(int cgc_argc, char *cgc_argv[])
{
#define BUF_SIZE 64
#define READLINE(_buf, _len) do { sret = cgc_readline(_buf, _len); if (sret == 0) { cgc__terminate(1); } } while (0)
#ifdef __FC_PATCHED
char buf[BUF_SIZE] = {0};
#else
char buf[BUF_SIZE] = {};
#endif
int i = 0;
int ret = 0;
int temp = 0;
size_t sret = 0;
char c = '\n';
cgc_transmit_str(ENTER_NUM_MSG);
READLINE(buf, BUF_SIZE);
i = cgc_toInt(buf[0], buf[1]);
if (cgc_init(i+1) != 0)
{
return (-1);
}
//initialize the LFSR
cgc_my_srand(*((int*)buf));
for (i = 0; i < NUM_ROUNDS; i++)
{
if (i == 0)
{
cgc_transmit_str(WORD_MSG);
}
else