From 9a114edfdc9c152ec8df20f36b5d33b64fd96b4a Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 17 Dec 2018 18:46:37 +0100
Subject: [PATCH] example
---
src/plugins/markdown-report/examples/cwe126.c | 90 ++++++
.../examples/cwe126.remarks-sample.md | 266 ++++++++++++++++++
2 files changed, 356 insertions(+)
create mode 100644 src/plugins/markdown-report/examples/cwe126.c
create mode 100644 src/plugins/markdown-report/examples/cwe126.remarks-sample.md
diff --git a/src/plugins/markdown-report/examples/cwe126.c b/src/plugins/markdown-report/examples/cwe126.c
new file mode 100644
index 00000000000..ac01cb2b4ae
--- /dev/null
+++ b/src/plugins/markdown-report/examples/cwe126.c
@@ -0,0 +1,90 @@
+/* extracted from Juliet test suite v1.3 for C
+ https://samate.nist.gov/SRD/view_testcase.php?tID=76270
+*/
+
+#include <stdlib.h>
+#include <string.h>
+
+void CWE126_Buffer_Overread__malloc_char_loop_64b_badSink(void * dataVoidPtr)
+{
+ /* cast void pointer to a pointer of the appropriate type */
+ char * * dataPtr = (char * *)dataVoidPtr;
+ /* dereference dataPtr into data */
+ char * data = (*dataPtr);
+ {
+ size_t i, destLen;
+ char dest[100];
+ memset(dest, 'C', 100-1);
+ dest[100-1] = '\0'; /* null terminate */
+ destLen = strlen(dest);
+ /* POTENTIAL FLAW: using length of the dest where data
+ * could be smaller than dest causing buffer overread */
+ for (i = 0; i < destLen; i++)
+ {
+ dest[i] = data[i];
+ }
+ dest[100-1] = '\0';
+ free(data);
+ }
+}
+
+void CWE126_Buffer_Overread__malloc_char_loop_64_bad()
+{
+ char * data;
+ data = NULL;
+ /* FLAW: Use a small buffer */
+ data = (char *)malloc(50*sizeof(char));
+ if (data == NULL) {exit(-1);}
+ memset(data, 'A', 50-1); /* fill with 'A's */
+ data[50-1] = '\0'; /* null terminate */
+ CWE126_Buffer_Overread__malloc_char_loop_64b_badSink(&data);
+}
+
+/* goodG2B uses the GoodSource with the BadSink */
+void CWE126_Buffer_Overread__malloc_char_loop_64b_goodG2BSink(void * dataVoidPtr)
+{
+ /* cast void pointer to a pointer of the appropriate type */
+ char * * dataPtr = (char * *)dataVoidPtr;
+ /* dereference dataPtr into data */
+ char * data = (*dataPtr);
+ {
+ size_t i, destLen;
+ char dest[100];
+ memset(dest, 'C', 100-1);
+ dest[100-1] = '\0'; /* null terminate */
+ destLen = strlen(dest);
+ /* POTENTIAL FLAW: using length of the dest where data
+ * could be smaller than dest causing buffer overread */
+ for (i = 0; i < destLen; i++)
+ {
+ dest[i] = data[i];
+ }
+ dest[100-1] = '\0';
+ free(data);
+ }
+}
+
+static void goodG2B()
+{
+ char * data;
+ data = NULL;
+ /* FIX: Use a large buffer */
+ data = (char *)malloc(100*sizeof(char));
+ if (data == NULL) {exit(-1);}
+ memset(data, 'A', 100-1); /* fill with 'A's */
+ data[100-1] = '\0'; /* null terminate */
+ CWE126_Buffer_Overread__malloc_char_loop_64b_goodG2BSink(&data);
+}
+
+void CWE126_Buffer_Overread__malloc_char_loop_64_good()
+{
+ goodG2B();
+}
+
+int main(int argc, char * argv[])
+{
+ CWE126_Buffer_Overread__malloc_char_loop_64_good();
+ CWE126_Buffer_Overread__malloc_char_loop_64_bad();
+ return 0;
+}
+
diff --git a/src/plugins/markdown-report/examples/cwe126.remarks-sample.md b/src/plugins/markdown-report/examples/cwe126.remarks-sample.md
new file mode 100644
index 00000000000..b008643d0ee
--- /dev/null
+++ b/src/plugins/markdown-report/examples/cwe126.remarks-sample.md
@@ -0,0 +1,266 @@
+---
+title: Draft report
+author:
+date: 2018-12-13
+...
+
+\let\underscore\_
+\renewcommand{\_}{\discretionary{\underscore}{}{\underscore}}
+
+<!-- This file contains additional remarks that will be added to
+ automatically generated content by Frama-C's Markdown-report plugin. For
+ any section of the document, you can write pandoc markdown content
+ between the BEGIN and END comments. In addition, the plug-in will
+ consider any \<!-- INCLUDE file.md --\> comment (without backslashes) as
+ a directive to include the content of file.md in the corresponding
+ section. Please don't alter the structure of the document as it is used
+ by the plugin to associate content to the relevant section.
+-->
+
+# Introduction {#intro}
+
+<!-- You can add here some overall introduction to the analysis -->
+
+<!-- BEGIN_REMARK -->
+This is a test from the Juliet test suite showing an example of buffer
+overflow (CWE126). The `good` functions should not trigger any alarm, while
+the `bad` ones have indeed an error.
+<!-- END_REMARK -->
+
+# Context of the analysis {#context}
+
+## Input files {#c-input}
+
+<!-- You can add here some remarks about the set of files that is considered
+ by Frama-C
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+The C source files (not including the headers `.h` files)
+that have been considered during the analysis are the following:
+
+* `cwe126.c`
+
+
+
+## Configuration {#options}
+
+<!-- You can add here some remarks about the options used for the analysis
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+### EVA Domains {#domains}
+
+<!-- You can give more information about the choice of EVA domains -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+### Stubbed Functions {#stubs}
+
+<!-- You can add here general comments about the stubs that have been used
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+<!-- You can add here general comments about the stubs that have been used
+-->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `char_equal_ignore_case` {#char_equal_ignore_case}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `memrchr` {#memrchr}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strcasecmp` {#strcasecmp}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strndup` {#strndup}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strdup` {#strdup}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strncat` {#strncat}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strcat` {#strcat}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strncpy` {#strncpy}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strcpy` {#strcpy}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strerror` {#strerror}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strstr` {#strstr}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strrchr` {#strrchr}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strchr` {#strchr}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strncmp` {#strncmp}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strcmp` {#strcmp}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strnlen` {#strnlen}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `strlen` {#strlen}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `memset` {#memset}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `memmove` {#memmove}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `memcpy` {#memcpy}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `memchr` {#memchr}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+#### `memcmp` {#memcmp}
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Coverage {#coverage}
+
+There are 6 function definitions that are not stubbed. They represent 50 statements, of which 43 are potentially reachable through EVA, resulting in a **statement coverage of 86.0%** with respect to the entire application.
+
+
+There were potentially 6 functions syntactically reachable from main.
+These functions contain 50 statements, of which 43 are potentially reachable according to EVA, resulting in a **statement coverage of 86.0%** with respect to the perimeter set by this entry point.
+
+
+<!-- You can comment on the coverage obtained by EVA -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Warnings {#warnings}
+
+<!-- you can comment on each individual error -->
+
+## Warning 0 (cwe126.c:24) {#warn-0}
+
+message text is
+
+out of bounds read. assert \valid_read(data + i);
+
+
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
+# Results of the analysis {#alarms}
+
+## Alarm 0 at cwe126.c:24 {#Alarm-0}
+
+```acsl
+assert mem_access: \valid_read(data + i);
+```
+
+
+<!-- BEGIN_REMARK -->
+This alarm is real: Eva correctly identified the issue and did not report
+any spurious alarm anywhere else.
+<!-- END_REMARK -->
+
+# Conclusion {#conclusion}
+
+<!-- You can put here some concluding remarks -->
+
+<!-- BEGIN_REMARK -->
+
+<!-- END_REMARK -->
+
--
GitLab