[x509-parser] add E-ACSL target; add test DER certificate

x509-parser/.frama-c/GNUmakefile

@@ -37,6 +37,32 @@ TARGETS = x509-parser.eva
 x509-parser.parse: \
   ../src/x509-parser.c \
 
+## The following E-ACSL target relies on some errors deliberately introduced
+## in the code, and triggered at runtime. Note that, depending on your
+## configuration, the execution of the non-instrumented code may terminate
+## succesfully, without any indication that a buffer overflow took place.
+eacsl: ../x509-parser.stack.exe ../x509-parser.heap.exe
+
+EACSL_FLAGS = \
+  -M \
+  --rte=mem \
+  -F "-no-annot" \
+  -F "-rte-verbose 0 -variadic-verbose 0" \
+  -c \
+  -E -D__FC_EACSL__ \
+
+EACSL_SCRIPT:=$(shell dirname $(shell which $(FRAMAC)))/e-acsl-gcc.sh
+
+../x509-parser.stack.exe: ../src/x509-parser.c ../src/main.c
+	$(EACSL_SCRIPT) $(EACSL_FLAGS) \
+	-E -DEACSL_STACK_OVERFLOW \
+	$^ -O $@ -o x509-parser.stack.frama.c
+
+../x509-parser.heap.exe: ../src/x509-parser.c ../src/main.c
+	$(EACSL_SCRIPT) $(EACSL_FLAGS) \
+	-E -DEACSL_HEAP_OVERFLOW \
+	$^ -O $@ -o x509-parser.stack.frama.c
+
 ### Epilogue. Do not modify this block. #######################################
 include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/epilogue.mk
 ###############################################################################

x509-parser/.gitignore

+*.exe
+*.exe.e-acsl
+# it would be useful to store the instrumented source, but each version
+# has over 70k lines and 3.5 MB, so for now we ignore them
+.frama-c/*.frama.c

x509-parser/src/main.c

@@ -23,7 +23,21 @@ static void usage(char *argv0)
 
 int main(int argc, char *argv[])
 {
+  // To illustrate E-ACSL on this code, we deliberately change the buffer
+  // declaration to introduce errors during execution
+#ifndef __FC_EACSL__
+	// Original (bug-free) declaration
 	u8 buf[ASN1_MAX_BUFFER_SIZE];
+#else
+# ifdef EACSL_STACK_OVERFLOW
+	// Buffer size too small: a stack overflow will happen
+	u8 buf[ASN1_MAX_BUFFER_SIZE/64];
+# endif
+# ifdef EACSL_HEAP_OVERFLOW
+	// Buffer size too small: a heap overflow will happen
+	u8 *buf = malloc(sizeof(u8) * ASN1_MAX_BUFFER_SIZE/64);
+# endif
+#endif
 	off_t pos, offset = 0;
 	char *path = argv[1];
 	u16 rem, copied, eaten;

x509-parser/src/x509-parser.c

@@ -9222,7 +9222,7 @@ out:
 	return ret;
 }
 
-#if defined(__FRAMAC__)
+#if defined(__FRAMAC__) && !defined(__FC_EACSL__)
 
 /* This dummy main allows testing */