First steps with klee to confirm the contract for the underlaying functions that receive the messages and process them

.gitignore

@@ -11,3 +11,5 @@ gnatprove/
 libs/
 prove-loc.xml
 codepeer/
+*.bc
+klee-*

klee/Makefile

@@ -0,0 +1,9 @@
+TOPTARGETS := all clean
+
+SUBDIRS := $(wildcard */.)
+
+$(TOPTARGETS): $(SUBDIRS)
+$(SUBDIRS):
+	$(MAKE) -C $@ $(MAKECMDGOALS)
+
+.PHONY: $(TOPTARGETS) $(SUBDIRS)

klee/close_wait/Makefile

@@ -0,0 +1,48 @@
+CFILES = \
+	$(wildcard *.c) \
+	../model.c \
+	../../src/cyclone_tcp/core/net.c \
+	../../src/cyclone_tcp/core/tcp.c \
+	../../src/common/os_port_none.c \
+	../../src/cyclone_tcp/core/socket.c \
+	../../src/cyclone_tcp/core/nic.c \
+	../../src/cyclone_tcp/ipv4/arp.c \
+	../../src/cyclone_tcp/ipv4/ipv4_frag.c \
+	../../src/cyclone_tcp/ipv4/igmp.c \
+	../../src/cyclone_tcp/dhcp/dhcp_client.c \
+	../../src/cyclone_tcp/ipv6/ipv6_frag.c \
+	../../src/cyclone_tcp/ipv6/mld.c \
+	../../src/cyclone_tcp/ipv6/ndp.c \
+	../../src/cyclone_tcp/dns/dns_cache.c \
+	../../src/cyclone_tcp/ipv6/ipv6.c \
+	../../src/cyclone_tcp/core/ethernet.c \
+	../../src/cyclone_tcp/core/net_misc.c \
+	../../src/cyclone_tcp/core/tcp_misc.c \
+	../../src/cyclone_tcp/core/ip.c \
+	../../src/cyclone_tcp/core/net_mem.c \
+	../../src/common/cpu_endian.c \
+	../../src/cyclone_tcp/ipv4/ipv4.c
+
+BCFILES = $(patsubst %.c, %.bc, $(CFILES))
+
+PATH_TO_KLEE = /home/cluzel/klee/klee/include/
+
+INCLUDES = \
+	-I../ \
+	-I../../src/cyclone_tcp/ \
+	-I../../src/common/ \
+	-I $(PATH_TO_KLEE)
+
+all: program.bc
+	klee -warnings-only-to-file $<
+
+%.bc: %.c
+	clang-6.0 -c -g -O0 -emit-llvm $(INCLUDES) $< -o $@
+
+program.bc: $(BCFILES)
+	llvm-link-6.0 $(BCFILES) -o $@
+
+.PHONY: clean all
+
+clean:
+	rm -rf $(BCFILES) klee-* program.bc

klee/close_wait/close_wait.c

@@ -0,0 +1,107 @@
+#include "core/socket.h"
+#include "klee/klee.h"
+#include "core/tcp_misc.h"
+#include <assert.h>
+#include <stdlib.h>
+#include "model.h"
+
+
+void tcpStateCloseWait(Socket *socket, TcpHeader *segment, size_t length)
+{
+   uint_t flags = 0;
+
+   //Debug message
+   // TRACE_DEBUG("TCP FSM: CLOSE-WAIT state\r\n");
+
+   //First check sequence number
+   if(tcpCheckSequenceNumber(socket, segment, length))
+      return;
+
+   //Check the RST bit
+   if(segment->flags & TCP_FLAG_RST)
+   {
+      //Switch to the CLOSED state
+      tcpChangeState(socket, TCP_STATE_CLOSED);
+
+      //Number of times TCP connections have made a direct transition to the
+      //CLOSED state from either the ESTABLISHED state or the CLOSE-WAIT state
+    //   MIB2_INC_COUNTER32(tcpGroup.tcpEstabResets, 1);
+    //   TCP_MIB_INC_COUNTER32(tcpEstabResets, 1);
+
+      //Return immediately
+      return;
+   }
+
+   //Check the SYN bit
+   if(tcpCheckSyn(socket, segment, length))
+      return;
+   //Check the ACK field
+   if(tcpCheckAck(socket, segment, length))
+      return;
+
+#if (TCP_CONGEST_CONTROL_SUPPORT == ENABLED)
+   //Duplicate AK received?
+   if(socket->dupAckCount > 0)
+      flags = SOCKET_FLAG_NO_DELAY;
+#endif
+
+   //The Nagle algorithm should be implemented to coalesce
+   //short segments (refer to RFC 1122 4.2.3.4)
+   tcpNagleAlgo(socket, flags);
+}
+
+int main() {
+    // Initialisation
+    socketInit();
+
+    Socket* socket;
+    TcpHeader *segment;
+    size_t length;
+    uint32_t ackNum, seqNum;
+    uint8_t flags;
+    uint16_t checksum;
+    struct socketModel* sModel;
+
+    segment = malloc(sizeof(TcpHeader));
+
+    // creation of a TCP socket
+    socket = socketOpen(SOCKET_TYPE_STREAM, SOCKET_IP_PROTO_TCP);
+
+    // TODO: See if it is the correct way to process.
+    // Maybe open the connection by following the real call of the function
+    // is a better way to do.
+    tcpChangeState(socket, TCP_STATE_CLOSE_WAIT);
+
+    klee_assert(socket->state == TCP_STATE_CLOSE_WAIT);
+
+    klee_make_symbolic(&ackNum, sizeof(ackNum), "ackNum");
+    klee_make_symbolic(&seqNum, sizeof(seqNum), "seqNum");
+    klee_make_symbolic(&flags, sizeof(flags), "flags");
+    klee_assume(flags >= 0 && flags <= 31);
+    klee_make_symbolic(&checksum, sizeof(checksum), "checksum");
+
+    segment->srcPort = 80;
+    segment->destPort = socket->localPort;
+    segment->seqNum = seqNum;
+    segment->ackNum = ackNum;
+    segment->reserved1 = 0;
+    segment->dataOffset = 6; // Normalement sans importance
+    segment->flags = flags;
+    segment->reserved2 = 0;
+    segment->window = 26883; // Voir ce que c'est exactement
+    segment->checksum = checksum;
+    segment->urgentPointer = 0;
+
+    klee_make_symbolic(&length, sizeof(length), "length");
+
+    // We make a hard copy of the struct to check if the fields have
+    // changed after the call to the function
+    sModel = toSockModel(socket);
+
+    tcpStateCloseWait(socket, segment, length);
+
+    klee_assert(equalSocketModel(socket, sModel) &&
+                (socket->state == TCP_STATE_CLOSE_WAIT ||
+                (socket->state == TCP_STATE_CLOSED &&
+                 socket->resetFlag)));
+}

klee/closed_state/Makefile

@@ -0,0 +1,48 @@
+CFILES = \
+	$(wildcard *.c) \
+	../model.c \
+	../../src/cyclone_tcp/core/net.c \
+	../../src/cyclone_tcp/core/tcp.c \
+	../../src/common/os_port_none.c \
+	../../src/cyclone_tcp/core/socket.c \
+	../../src/cyclone_tcp/core/nic.c \
+	../../src/cyclone_tcp/ipv4/arp.c \
+	../../src/cyclone_tcp/ipv4/ipv4_frag.c \
+	../../src/cyclone_tcp/ipv4/igmp.c \
+	../../src/cyclone_tcp/dhcp/dhcp_client.c \
+	../../src/cyclone_tcp/ipv6/ipv6_frag.c \
+	../../src/cyclone_tcp/ipv6/mld.c \
+	../../src/cyclone_tcp/ipv6/ndp.c \
+	../../src/cyclone_tcp/dns/dns_cache.c \
+	../../src/cyclone_tcp/ipv6/ipv6.c \
+	../../src/cyclone_tcp/core/ethernet.c \
+	../../src/cyclone_tcp/core/net_misc.c \
+	../../src/cyclone_tcp/core/tcp_misc.c \
+	../../src/cyclone_tcp/core/ip.c \
+	../../src/cyclone_tcp/core/net_mem.c \
+	../../src/common/cpu_endian.c \
+	../../src/cyclone_tcp/ipv4/ipv4.c
+
+BCFILES = $(patsubst %.c, %.bc, $(CFILES))
+
+PATH_TO_KLEE = /home/cluzel/klee/klee/include/
+
+INCLUDES = \
+	-I../ \
+	-I../../src/cyclone_tcp/ \
+	-I../../src/common/ \
+	-I $(PATH_TO_KLEE)
+
+all: program.bc
+	klee -warnings-only-to-file $<
+
+%.bc: %.c
+	clang-6.0 -c -g -emit-llvm $(INCLUDES) $< -o $@
+
+program.bc: $(BCFILES)
+	llvm-link-6.0 $(BCFILES) -o $@
+
+.PHONY: clean all
+
+clean:
+	rm -rf $(BCFILES) klee-* program.bc

klee/closed_state/closed_state.c

@@ -0,0 +1,207 @@
+#include "core/socket.h"
+#include "klee/klee.h"
+#include <assert.h>
+// #include "core/tcp_fsm.h"
+#include <stdlib.h>
+
+error_t tcpSendResetSegmentBis(NetInterface *interface,
+   IpPseudoHeader *pseudoHeader, TcpHeader *segment, size_t length)
+{
+   error_t error;
+   size_t offset;
+   uint8_t flags;
+   uint32_t seqNum;
+   uint32_t ackNum;
+   NetBuffer *buffer;
+   TcpHeader *segment2;
+   IpPseudoHeader pseudoHeader2;
+
+   //Check whether the ACK bit is set
+   if(segment->flags & TCP_FLAG_ACK)
+   {
+      //If the incoming segment has an ACK field, the reset takes
+      //its sequence number from the ACK field of the segment
+      flags = TCP_FLAG_RST;
+      seqNum = segment->ackNum;
+      ackNum = 0;
+   }
+   else
+   {
+      //Otherwise the reset has sequence number zero and the ACK field is set to
+      //the sum of the sequence number and segment length of the incoming segment
+      flags = TCP_FLAG_RST | TCP_FLAG_ACK;
+      seqNum = 0;
+      ackNum = segment->seqNum + length;
+
+      //Advance the acknowledgment number over the SYN or the FIN
+      if(segment->flags & TCP_FLAG_SYN)
+         ackNum++;
+      if(segment->flags & TCP_FLAG_FIN)
+         ackNum++;
+   }
+
+   //Allocate a memory buffer to hold the reset segment
+   buffer = ipAllocBuffer(sizeof(TcpHeader), &offset);
+   //Failed to allocate memory?
+   if(buffer == NULL)
+      return ERROR_OUT_OF_MEMORY;
+
+   //Point to the beginning of the TCP segment
+   segment2 = netBufferAt(buffer, offset);
+
+   //Format TCP header
+   segment2->srcPort = htons(segment->destPort);
+   segment2->destPort = htons(segment->srcPort);
+   segment2->seqNum = htonl(seqNum);
+   segment2->ackNum = htonl(ackNum);
+   segment2->reserved1 = 0;
+   segment2->dataOffset = 5;
+   segment2->flags = flags;
+   segment2->reserved2 = 0;
+   segment2->window = 0;
+   segment2->checksum = 0;
+   segment2->urgentPointer = 0;
+
+#if (IPV4_SUPPORT == ENABLED)
+   //Destination address is an IPv4 address?
+   if(pseudoHeader->length == sizeof(Ipv4PseudoHeader))
+   {
+      //Format IPv4 pseudo header
+      pseudoHeader2.length = sizeof(Ipv4PseudoHeader);
+      pseudoHeader2.ipv4Data.srcAddr = pseudoHeader->ipv4Data.destAddr;
+      pseudoHeader2.ipv4Data.destAddr = pseudoHeader->ipv4Data.srcAddr;
+      pseudoHeader2.ipv4Data.reserved = 0;
+      pseudoHeader2.ipv4Data.protocol = IPV4_PROTOCOL_TCP;
+      pseudoHeader2.ipv4Data.length = HTONS(sizeof(TcpHeader));
+
+      //Calculate TCP header checksum
+      segment2->checksum = ipCalcUpperLayerChecksumEx(&pseudoHeader2.ipv4Data,
+         sizeof(Ipv4PseudoHeader), buffer, offset, sizeof(TcpHeader));
+   }
+   else
+#endif
+#if (IPV6_SUPPORT == ENABLED)
+   //Destination address is an IPv6 address?
+   if(pseudoHeader->length == sizeof(Ipv6PseudoHeader))
+   {
+      //Format IPv6 pseudo header
+      pseudoHeader2.length = sizeof(Ipv6PseudoHeader);
+      pseudoHeader2.ipv6Data.srcAddr = pseudoHeader->ipv6Data.destAddr;
+      pseudoHeader2.ipv6Data.destAddr = pseudoHeader->ipv6Data.srcAddr;
+      pseudoHeader2.ipv6Data.length = HTONL(sizeof(TcpHeader));
+      pseudoHeader2.ipv6Data.reserved = 0;
+      pseudoHeader2.ipv6Data.nextHeader = IPV6_TCP_HEADER;
+
+      //Calculate TCP header checksum
+      segment2->checksum = ipCalcUpperLayerChecksumEx(&pseudoHeader2.ipv6Data,
+         sizeof(Ipv6PseudoHeader), buffer, offset, sizeof(TcpHeader));
+   }
+   else
+#endif
+   //Destination address is not valid?
+   {
+      //Free previously allocated memory
+      netBufferFree(buffer);
+      //This should never occur...
+      return ERROR_INVALID_ADDRESS;
+   }
+
+   //Total number of segments sent
+   // MIB2_INC_COUNTER32(tcpGroup.tcpOutSegs, 1);
+   // TCP_MIB_INC_COUNTER32(tcpOutSegs, 1);
+   // TCP_MIB_INC_COUNTER64(tcpHCOutSegs, 1);
+
+   // //Number of TCP segments sent containing the RST flag
+   // MIB2_INC_COUNTER32(tcpGroup.tcpOutRsts, 1);
+   // TCP_MIB_INC_COUNTER32(tcpOutRsts, 1);
+
+   //Debug message
+   // TRACE_DEBUG("%s: Sending TCP reset segment...\r\n",
+   //    formatSystemTime(osGetSystemTime(), NULL));
+   //Dump TCP header contents for debugging purpose
+   // tcpDumpHeader(segment2, length, 0, 0);
+
+   //Send TCP segment
+   // error = ipSendDatagram(interface, &pseudoHeader2, buffer, offset,
+   //    &NET_DEFAULT_ANCILLARY_DATA);
+
+   //Free previously allocated memory
+   netBufferFree(buffer);
+
+   //Return error code
+   return error;
+}
+
+void tcpStateClosed(NetInterface *interface,
+   IpPseudoHeader *pseudoHeader, TcpHeader *segment, size_t length)
+{
+   //Debug message
+   // TRACE_DEBUG("TCP FSM: CLOSED state\r\n");
+
+   //An incoming segment not containing a RST causes
+   //a reset to be sent in response
+   if(!(segment->flags & TCP_FLAG_RST))
+      tcpSendResetSegmentBis(interface, pseudoHeader, segment, length);
+}
+
+int main() {
+   // Initialisation
+   socketInit();
+   
+   Socket* socket;
+   IpPseudoHeader *pseudoHeader;
+   TcpHeader *segment;
+   size_t length;
+   uint32_t ackNum, seqNum;
+   uint8_t flags;
+   uint16_t checksum;
+
+   pseudoHeader = malloc(sizeof(IpPseudoHeader));
+   segment = malloc(sizeof(TcpHeader));
+
+   // Creation of a TCP socket
+   socket = socketOpen(SOCKET_TYPE_STREAM, SOCKET_IP_PROTO_TCP);
+
+   // We should already be in the desired state after the opening
+   // of the connection
+   klee_assert(socket->state == TCP_STATE_CLOSED);
+
+   // Creation of a "random" incomming package
+   pseudoHeader->length = 12;
+   pseudoHeader->ipv4Data.srcAddr = 1584454659;
+   pseudoHeader->ipv4Data.destAddr = 3430877706;
+   pseudoHeader->ipv4Data.reserved = 0;
+   pseudoHeader->ipv4Data.protocol = 6; // TCP protocol
+   pseudoHeader->ipv4Data.length = 6144;
+   pseudoHeader->data[0] = 3;
+   pseudoHeader->data[1] = 220;
+   pseudoHeader->data[2] = 112;
+   pseudoHeader->data[3] = 94;
+
+   klee_make_symbolic(&ackNum, sizeof(ackNum), "ackNum");
+   klee_make_symbolic(&seqNum, sizeof(seqNum), "seqNum");
+   klee_make_symbolic(&flags, sizeof(flags), "flags");
+   klee_assume(flags >= 0 && flags <= 31);
+   klee_make_symbolic(&checksum, sizeof(checksum), "checksum");
+
+   segment->srcPort = 80;
+   segment->destPort = socket->localPort;
+   segment->seqNum = seqNum;
+   segment->ackNum = ackNum;
+   segment->reserved1 = 0;
+   segment->dataOffset = 6; // Normalement sans importance
+   segment->flags = flags;
+   segment->reserved2 = 0;
+   segment->window = 26883; // Voir ce que c'est exactement
+   segment->checksum = checksum;
+   segment->urgentPointer = 0;
+
+   // it's the length of the data received. We can assume it's something random
+   length = 0;
+
+   tcpStateClosed(socket->interface, pseudoHeader, segment, length);
+
+   klee_assert(socket->state == TCP_STATE_CLOSED);
+   
+   return 0;
+}

klee/closing/Makefile

@@ -0,0 +1,49 @@
+CFILES = \
+	$(wildcard *.c) \
+	../model.c \
+	../../src/cyclone_tcp/core/net.c \
+	../../src/cyclone_tcp/core/tcp.c \
+	../../src/common/os_port_none.c \
+	../../src/cyclone_tcp/core/socket.c \
+	../../src/cyclone_tcp/core/nic.c \
+	../../src/cyclone_tcp/ipv4/arp.c \
+	../../src/cyclone_tcp/ipv4/ipv4_frag.c \
+	../../src/cyclone_tcp/ipv4/igmp.c \
+	../../src/cyclone_tcp/dhcp/dhcp_client.c \
+	../../src/cyclone_tcp/ipv6/ipv6_frag.c \
+	../../src/cyclone_tcp/ipv6/mld.c \
+	../../src/cyclone_tcp/ipv6/ndp.c \
+	../../src/cyclone_tcp/dns/dns_cache.c \
+	../../src/cyclone_tcp/ipv6/ipv6.c \
+	../../src/cyclone_tcp/core/ethernet.c \
+	../../src/cyclone_tcp/core/net_misc.c \
+	../../src/cyclone_tcp/core/tcp_misc.c \
+	../../src/cyclone_tcp/core/ip.c \
+	../../src/cyclone_tcp/core/net_mem.c \
+	../../src/common/cpu_endian.c \
+	../../src/cyclone_tcp/ipv4/ipv4.c \
+	../../src/cyclone_tcp/core/tcp_timer.c
+
+BCFILES = $(patsubst %.c, %.bc, $(CFILES))
+
+PATH_TO_KLEE = /home/cluzel/klee/klee/include/
+
+INCLUDES = \
+	-I../ \
+	-I../../src/cyclone_tcp/ \
+	-I../../src/common/ \
+	-I $(PATH_TO_KLEE)
+
+all: program.bc
+	klee -warnings-only-to-file $<
+
+%.bc: %.c
+	clang-6.0 -c -g -O0 -emit-llvm $(INCLUDES) $< -o $@
+
+program.bc: $(BCFILES)
+	llvm-link-6.0 $(BCFILES) -o $@
+
+.PHONY: clean all
+
+clean:
+	rm -rf $(BCFILES) klee-* program.bc

klee/closing/closing.c

@@ -0,0 +1,105 @@
+#include "core/socket.h"
+#include "klee/klee.h"
+#include "core/tcp_misc.h"
+#include <assert.h>
+#include <stdlib.h>
+#include "model.h"
+#include "core/tcp_timer.h"
+
+void tcpStateClosing(Socket *socket, TcpHeader *segment, size_t length)
+{
+    //Debug message
+    // TRACE_DEBUG("TCP FSM: CLOSING state\r\n");
+
+    //First check sequence number
+    if (tcpCheckSequenceNumber(socket, segment, length))
+        return;
+
+    //Check the RST bit
+    if (segment->flags & TCP_FLAG_RST)
+    {
+        //Enter CLOSED state
+        tcpChangeState(socket, TCP_STATE_CLOSED);
+        //Return immediately
+        return;
+    }
+
+    //Check the SYN bit
+    if (tcpCheckSyn(socket, segment, length))
+        return;
+    //Check the ACK field
+    if (tcpCheckAck(socket, segment, length))
+        return;
+
+    //If the ACK acknowledges our FIN then enter the TIME-WAIT
+    //state, otherwise ignore the segment
+    if (segment->ackNum == socket->sndNxt)
+    {
+        //Release previously allocated resources
+        tcpDeleteControlBlock(socket);
+        //Start the 2MSL timer
+        tcpTimerStart(&socket->timeWaitTimer, TCP_2MSL_TIMER);
+        //Switch to the TIME-WAIT state
+        tcpChangeState(socket, TCP_STATE_TIME_WAIT);
+    }
+}
+
+int main()
+{
+    // Initialisation
+    socketInit();
+
+    Socket *socket;
+    TcpHeader *segment;
+    size_t length;
+    uint32_t ackNum, seqNum;
+    uint8_t flags, dataOffset;
+    uint16_t checksum;
+    struct socketModel *sModel;
+
+    segment = malloc(sizeof(TcpHeader));
+
+    // creation of a TCP socket
+    socket = socketOpen(SOCKET_TYPE_STREAM, SOCKET_IP_PROTO_TCP);
+
+    // TODO: See if it is the correct way to process.
+    // Maybe open the connection by following the real call of the function
+    // is a better way to do.
+    tcpChangeState(socket, TCP_STATE_CLOSING);
+
+    klee_make_symbolic(&ackNum, sizeof(ackNum), "ackNum");
+    klee_make_symbolic(&seqNum, sizeof(seqNum), "seqNum");
+    klee_make_symbolic(&flags, sizeof(flags), "flags");
+    klee_assume(flags >= 0 && flags <= 31);
+    klee_make_symbolic(&checksum, sizeof(checksum), "checksum");
+    klee_make_symbolic(&dataOffset, sizeof(dataOffset), "dataOffset");
+    klee_assume(0 <= dataOffset && dataOffset <= 15);
+
+    segment->srcPort = 80;
+    segment->destPort = socket->localPort;
+    segment->seqNum = seqNum;
+    segment->ackNum = ackNum;
+    segment->reserved1 = 0;
+    segment->dataOffset = dataOffset;
+    segment->flags = flags;
+    segment->reserved2 = 0;
+    segment->window = 26883; // Voir ce que c'est exactement
+    segment->checksum = checksum;
+    segment->urgentPointer = 0;
+
+    klee_make_symbolic(&length, sizeof(length), "length");
+
+    // We make a hard copy of the struct to check if the fields have
+    // changed after the call to the function
+    sModel = toSockModel(socket);
+
+    klee_assert(socket->state == TCP_STATE_CLOSING);
+
+    tcpStateClosing(socket, segment, length);
+
+    klee_assert(equalSocketModel(socket, sModel) &&
+                (socket->state == TCP_STATE_CLOSING ||
+                 socket->state == TCP_STATE_TIME_WAIT ||
+                 (socket->state == TCP_STATE_CLOSED &&
+                  socket->resetFlag)));
+}

klee/fin_wait_1/Makefile

@@ -0,0 +1,49 @@
+CFILES = \
+	$(wildcard *.c) \
+	../model.c \
+	../../src/cyclone_tcp/core/net.c \
+	../../src/cyclone_tcp/core/tcp.c \
+	../../src/common/os_port_none.c \
+	../../src/cyclone_tcp/core/socket.c \
+	../../src/cyclone_tcp/core/nic.c \
+	../../src/cyclone_tcp/ipv4/arp.c \
+	../../src/cyclone_tcp/ipv4/ipv4_frag.c \
+	../../src/cyclone_tcp/ipv4/igmp.c \
+	../../src/cyclone_tcp/dhcp/dhcp_client.c \
+	../../src/cyclone_tcp/ipv6/ipv6_frag.c \
+	../../src/cyclone_tcp/ipv6/mld.c \
+	../../src/cyclone_tcp/ipv6/ndp.c \
+	../../src/cyclone_tcp/dns/dns_cache.c \
+	../../src/cyclone_tcp/ipv6/ipv6.c \
+	../../src/cyclone_tcp/core/ethernet.c \
+	../../src/cyclone_tcp/core/net_misc.c \
+	../../src/cyclone_tcp/core/tcp_misc.c \
+	../../src/cyclone_tcp/core/ip.c \
+	../../src/cyclone_tcp/core/net_mem.c \
+	../../src/common/cpu_endian.c \
+	../../src/cyclone_tcp/ipv4/ipv4.c \
+	../../src/cyclone_tcp/core/tcp_timer.c
+
+BCFILES = $(patsubst %.c, %.bc, $(CFILES))
+
+PATH_TO_KLEE = /home/cluzel/klee/klee/include/
+
+INCLUDES = \
+	-I../ \
+	-I../../src/cyclone_tcp/ \
+	-I../../src/common/ \
+	-I $(PATH_TO_KLEE)
+
+all: program.bc
+	klee -warnings-only-to-file $<
+
+%.bc: %.c
+	clang-6.0 -c -g -O0 -emit-llvm $(INCLUDES) $< -o $@
+
+program.bc: $(BCFILES)
+	llvm-link-6.0 $(BCFILES) -o $@
+
+.PHONY: clean all
+
+clean:
+	rm -rf $(BCFILES) klee-* program.bc

klee/fin_wait_1/fin_wait_1.c

@@ -0,0 +1,144 @@
+#include "core/socket.h"
+#include "klee/klee.h"
+#include "core/tcp_misc.h"
+#include <assert.h>
+#include <stdlib.h>
+#include "model.h"
+#include "core/tcp_timer.h"
+
+void tcpStateFinWait1(Socket *socket, TcpHeader *segment,
+                      const NetBuffer *buffer, size_t offset, size_t length)
+{
+    //Debug message
+    // TRACE_DEBUG("TCP FSM: FIN-WAIT-1 state\r\n");
+
+    //First check sequence number
+    if (tcpCheckSequenceNumber(socket, segment, length))
+        return;
+
+    //Check the RST bit
+    if (segment->flags & TCP_FLAG_RST)
+    {
+        //Switch to the CLOSED state
+        tcpChangeState(socket, TCP_STATE_CLOSED);
+        //Return immediately
+        return;
+    }
+
+    //Check the SYN bit
+    if (tcpCheckSyn(socket, segment, length))
+        return;
+    //Check the ACK field
+    if (tcpCheckAck(socket, segment, length))
+        return;
+
+    //Check whether our FIN is now acknowledged
+    if (segment->ackNum == socket->sndNxt)
+    {
+        //Start the FIN-WAIT-2 timer to prevent the connection
+        //from staying in the FIN-WAIT-2 state forever
+        tcpTimerStart(&socket->finWait2Timer, TCP_FIN_WAIT_2_TIMER);
+        //enter FIN-WAIT-2 and continue processing in that state
+        tcpChangeState(socket, TCP_STATE_FIN_WAIT_2);
+    }
+
+    //Process the segment text
+    if (length > 0)
+        tcpProcessSegmentData(socket, segment, buffer, offset, length);
+
+    //Check the FIN bit
+    if (segment->flags & TCP_FLAG_FIN)
+    {
+        //The FIN can only be acknowledged if all the segment data
+        //has been successfully transferred to the receive buffer
+        if (socket->rcvNxt == (segment->seqNum + length))
+        {
+            //Advance RCV.NXT over the FIN
+            socket->rcvNxt++;
+            //Send an acknowledgment for the FIN
+            tcpSendSegment(socket, TCP_FLAG_ACK, socket->sndNxt, socket->rcvNxt, 0, FALSE);
+
+            //Check if our FIN has been acknowledged
+            if (segment->ackNum == socket->sndNxt)
+            {
+                //Release previously allocated resources
+                tcpDeleteControlBlock(socket);
+                //Start the 2MSL timer
+                tcpTimerStart(&socket->timeWaitTimer, TCP_2MSL_TIMER);
+                //Switch to the TIME-WAIT state
+                tcpChangeState(socket, TCP_STATE_TIME_WAIT);
+            }
+            else
+            {
+                //If our FIN has not been acknowledged, then enter CLOSING state
+                tcpChangeState(socket, TCP_STATE_CLOSING);
+            }
+        }
+    }
+}
+
+int main()
+{
+    // Initialisation
+    socketInit();
+
+    Socket *socket;
+    TcpHeader *segment;
+    size_t length, offset;
+    uint32_t ackNum, seqNum;
+    uint8_t flags;
+    uint16_t checksum;
+    struct socketModel *sModel;
+    NetBuffer *buffer;
+
+    segment = malloc(sizeof(TcpHeader));
+
+    // creation of a TCP socket
+    socket = socketOpen(SOCKET_TYPE_STREAM, SOCKET_IP_PROTO_TCP);
+
+    // TODO: See if it is the correct way to process.
+    // Maybe open the connection by following the real call of the function
+    // is a better way to do.
+    tcpChangeState(socket, TCP_STATE_FIN_WAIT_1);
+
+    klee_make_symbolic(&ackNum, sizeof(ackNum), "ackNum");
+    klee_make_symbolic(&seqNum, sizeof(seqNum), "seqNum");
+    klee_make_symbolic(&flags, sizeof(flags), "flags");
+    klee_assume(flags >= 0 && flags <= 31);
+    klee_make_symbolic(&checksum, sizeof(checksum), "checksum");
+
+    segment->srcPort = 80;
+    segment->destPort = socket->localPort;
+    segment->seqNum = seqNum;
+    segment->ackNum = ackNum;
+    segment->reserved1 = 0;
+    segment->dataOffset = 6; // Normalement sans importance
+    segment->flags = flags;
+    segment->reserved2 = 0;
+    segment->window = 26883; // Voir ce que c'est exactement
+    segment->checksum = checksum;
+    segment->urgentPointer = 0;
+
+    // We can assume that length, offset and buffer are null
+    // TODO: See after to model a not empty buffer
+    length = 0;
+    offset = 0;
+    buffer = NULL;
+    //klee_make_symbolic(&length, sizeof(length), "length");
+
+    // We make a hard copy of the struct to check if the fields have
+    // changed after the call to the function
+    sModel = toSockModel(socket);
+
+    klee_assert(socket->state == TCP_STATE_FIN_WAIT_1);
+
+    tcpStateFinWait1(socket, segment, buffer, offset, length);
+
+    klee_assert(equalSocketModel(socket, sModel) &&
+                (socket->state == TCP_STATE_FIN_WAIT_1 ||
+                 socket->state == TCP_STATE_FIN_WAIT_2 ||
+                 socket->state == TCP_STATE_TIME_WAIT ||
+                 socket->state == TCP_STATE_CLOSING ||
+                 (socket->state == TCP_STATE_CLOSED &&
+                  socket->resetFlag)));
+}

klee/fin_wait_2/Makefile

@@ -0,0 +1,49 @@
+CFILES = \
+	$(wildcard *.c) \
+	../model.c \
+	../../src/cyclone_tcp/core/net.c \
+	../../src/cyclone_tcp/core/tcp.c \
+	../../src/common/os_port_none.c \
+	../../src/cyclone_tcp/core/socket.c \
+	../../src/cyclone_tcp/core/nic.c \
+	../../src/cyclone_tcp/ipv4/arp.c \
+	../../src/cyclone_tcp/ipv4/ipv4_frag.c \
+	../../src/cyclone_tcp/ipv4/igmp.c \
+	../../src/cyclone_tcp/dhcp/dhcp_client.c \
+	../../src/cyclone_tcp/ipv6/ipv6_frag.c \
+	../../src/cyclone_tcp/ipv6/mld.c \
+	../../src/cyclone_tcp/ipv6/ndp.c \
+	../../src/cyclone_tcp/dns/dns_cache.c \
+	../../src/cyclone_tcp/ipv6/ipv6.c \
+	../../src/cyclone_tcp/core/ethernet.c \
+	../../src/cyclone_tcp/core/net_misc.c \
+	../../src/cyclone_tcp/core/tcp_misc.c \
+	../../src/cyclone_tcp/core/ip.c \
+	../../src/cyclone_tcp/core/net_mem.c \
+	../../src/common/cpu_endian.c \
+	../../src/cyclone_tcp/ipv4/ipv4.c \
+	../../src/cyclone_tcp/core/tcp_timer.c
+
+BCFILES = $(patsubst %.c, %.bc, $(CFILES))
+
+PATH_TO_KLEE = /home/cluzel/klee/klee/include/
+
+INCLUDES = \
+	-I../ \
+	-I../../src/cyclone_tcp/ \
+	-I../../src/common/ \
+	-I $(PATH_TO_KLEE)
+
+all: program.bc
+	klee -warnings-only-to-file $<
+
+%.bc: %.c
+	clang-6.0 -c -g -O0 -emit-llvm $(INCLUDES) $< -o $@
+
+program.bc: $(BCFILES)
+	llvm-link-6.0 $(BCFILES) -o $@
+
+.PHONY: clean all
+
+clean:
+	rm -rf $(BCFILES) klee-* program.bc

klee/fin_wait_2/fin_wait_2.c

@@ -0,0 +1,124 @@
+#include "core/socket.h"
+#include "klee/klee.h"
+#include "core/tcp_misc.h"
+#include <assert.h>
+#include <stdlib.h>
+#include "model.h"
+#include "core/tcp_timer.h"
+
+void tcpStateFinWait2(Socket *socket, TcpHeader *segment,
+                      const NetBuffer *buffer, size_t offset, size_t length)
+{
+    //Debug message
+    // TRACE_DEBUG("TCP FSM: FIN-WAIT-2 state\r\n");
+
+    //First check sequence number
+    if (tcpCheckSequenceNumber(socket, segment, length))
+        return;
+
+    //Check the RST bit
+    if (segment->flags & TCP_FLAG_RST)
+    {
+        //Switch to the CLOSED state
+        tcpChangeState(socket, TCP_STATE_CLOSED);
+        //Return immediately
+        return;
+    }
+
+    //Check the SYN bit
+    if (tcpCheckSyn(socket, segment, length))
+        return;
+    //Check the ACK field
+    if (tcpCheckAck(socket, segment, length))
+        return;
+    //Process the segment text
+    if (length > 0)
+        tcpProcessSegmentData(socket, segment, buffer, offset, length);
+
+    //Check the FIN bit
+    if (segment->flags & TCP_FLAG_FIN)
+    {
+        //The FIN can only be acknowledged if all the segment data
+        //has been successfully transferred to the receive buffer
+        if (socket->rcvNxt == (segment->seqNum + length))
+        {
+            //Advance RCV.NXT over the FIN
+            socket->rcvNxt++;
+            //Send an acknowledgment for the FIN
+            tcpSendSegment(socket, TCP_FLAG_ACK, socket->sndNxt, socket->rcvNxt, 0, FALSE);
+
+            //Release previously allocated resources
+            tcpDeleteControlBlock(socket);
+            //Start the 2MSL timer
+            tcpTimerStart(&socket->timeWaitTimer, TCP_2MSL_TIMER);
+            //Switch to the TIME_WAIT state
+            tcpChangeState(socket, TCP_STATE_TIME_WAIT);
+        }
+    }
+}
+
+int main()
+{
+    // Initialisation
+    socketInit();
+
+    Socket *socket;
+    TcpHeader *segment;
+    size_t length, offset;
+    uint32_t ackNum, seqNum;
+    uint8_t flags, dataOffset;
+    uint16_t checksum;
+    struct socketModel *sModel;
+    NetBuffer *buffer;
+
+    segment = malloc(sizeof(TcpHeader));
+
+    // creation of a TCP socket
+    socket = socketOpen(SOCKET_TYPE_STREAM, SOCKET_IP_PROTO_TCP);
+
+    // TODO: See if it is the correct way to process.
+    // Maybe open the connection by following the real call of the function
+    // is a better way to do.
+    tcpChangeState(socket, TCP_STATE_FIN_WAIT_2);
+
+    klee_make_symbolic(&ackNum, sizeof(ackNum), "ackNum");
+    klee_make_symbolic(&seqNum, sizeof(seqNum), "seqNum");
+    klee_make_symbolic(&flags, sizeof(flags), "flags");
+    klee_assume(flags >= 0 && flags <= 31);
+    klee_make_symbolic(&checksum, sizeof(checksum), "checksum");
+    klee_make_symbolic(&dataOffset, sizeof(dataOffset), "dataOffset");
+    klee_assume(0 <= dataOffset && dataOffset <= 15);
+
+    segment->srcPort = 80;
+    segment->destPort = socket->localPort;
+    segment->seqNum = seqNum;
+    segment->ackNum = ackNum;
+    segment->reserved1 = 0;
+    segment->dataOffset = dataOffset;
+    segment->flags = flags;
+    segment->reserved2 = 0;
+    segment->window = 26883; // Voir ce que c'est exactement
+    segment->checksum = checksum;
+    segment->urgentPointer = 0;
+
+    // We can assume that length, offset and buffer are null
+    // TODO: See after to model a not empty buffer
+    length = 0;
+    offset = 0;
+    buffer = NULL;
+    //klee_make_symbolic(&length, sizeof(length), "length");
+
+    // We make a hard copy of the struct to check if the fields have
+    // changed after the call to the function
+    sModel = toSockModel(socket);
+
+    klee_assert(socket->state == TCP_STATE_FIN_WAIT_2);
+
+    tcpStateFinWait2(socket, segment, buffer, offset, length);
+
+    klee_assert(equalSocketModel(socket, sModel) &&
+                (socket->state == TCP_STATE_FIN_WAIT_2 ||
+                 socket->state == TCP_STATE_TIME_WAIT ||
+                 (socket->state == TCP_STATE_CLOSED &&
+                  socket->resetFlag)));
+}

klee/listen/Makefile

@@ -0,0 +1,49 @@
+CFILES = \
+	$(wildcard *.c) \
+	../model.c \
+	../../src/cyclone_tcp/core/net.c \
+	../../src/cyclone_tcp/core/tcp.c \
+	../../src/common/os_port_none.c \
+	../../src/cyclone_tcp/core/socket.c \
+	../../src/cyclone_tcp/core/nic.c \
+	../../src/cyclone_tcp/ipv4/arp.c \
+	../../src/cyclone_tcp/ipv4/ipv4_frag.c \
+	../../src/cyclone_tcp/ipv4/igmp.c \
+	../../src/cyclone_tcp/dhcp/dhcp_client.c \
+	../../src/cyclone_tcp/ipv6/ipv6_frag.c \
+	../../src/cyclone_tcp/ipv6/mld.c \
+	../../src/cyclone_tcp/ipv6/ndp.c \
+	../../src/cyclone_tcp/dns/dns_cache.c \
+	../../src/cyclone_tcp/ipv6/ipv6.c \
+	../../src/cyclone_tcp/core/ethernet.c \
+	../../src/cyclone_tcp/core/net_misc.c \
+	../../src/cyclone_tcp/core/tcp_misc.c \
+	../../src/cyclone_tcp/core/ip.c \
+	../../src/cyclone_tcp/core/net_mem.c \
+	../../src/common/cpu_endian.c \
+	../../src/cyclone_tcp/ipv4/ipv4.c \
+	../../src/cyclone_tcp/core/tcp_timer.c
+
+BCFILES = $(patsubst %.c, %.bc, $(CFILES))
+
+PATH_TO_KLEE = /home/cluzel/klee/klee/include/
+
+INCLUDES = \
+	-I../ \
+	-I../../src/cyclone_tcp/ \
+	-I../../src/common/ \
+	-I $(PATH_TO_KLEE)
+
+all: program.bc
+	klee -warnings-only-to-file $<
+
+%.bc: %.c
+	clang-6.0 -c -g -O0 -emit-llvm $(INCLUDES) $< -o $@
+
+program.bc: $(BCFILES)
+	llvm-link-6.0 $(BCFILES) -o $@
+
+.PHONY: clean all
+
+clean:
+	rm -rf $(BCFILES) klee-* program.bc

klee/listen/listen.c

@@ -0,0 +1,280 @@
+#include "core/socket.h"
+#include "klee/klee.h"
+#include "core/tcp_misc.h"
+#include <assert.h>
+#include <stdlib.h>
+#include "model.h"
+
+// I'm not convinced here by what is done by klee. Maybe do something differently can be a good idea
+
+void tcpStateListen(Socket *socket, NetInterface *interface,
+                    IpPseudoHeader *pseudoHeader, TcpHeader *segment, size_t length)
+{
+    uint_t i;
+    TcpOption *option;
+    TcpSynQueueItem *queueItem;
+
+    //Debug message
+    // TRACE_DEBUG("TCP FSM: LISTEN state\r\n");
+
+    //An incoming RST should be ignored
+    if (segment->flags & TCP_FLAG_RST)
+        return;
+
+    //Any acknowledgment is bad if it arrives on a connection
+    //still in the LISTEN state
+    if (segment->flags & TCP_FLAG_ACK)
+    {
+        //A reset segment should be formed for any arriving ACK-bearing segment
+        // tcpSendResetSegment(interface, pseudoHeader, segment, length);
+        //Return immediately
+        return;
+    }
+
+    klee_print_expr("socket->synQueue: %p\n", socket->synQueue);
+
+    //Check the SYN bit
+    if (segment->flags & TCP_FLAG_SYN)
+    {
+        //Silently drop duplicate SYN segments
+        if (tcpIsDuplicateSyn(socket, pseudoHeader, segment))
+            return;
+
+        //Check whether the SYN queue is empty
+        if (socket->synQueue == NULL)
+        {
+            //Allocate memory to save incoming data
+            queueItem = memPoolAlloc(sizeof(TcpSynQueueItem));
+            //Add the newly created item to the queue
+            socket->synQueue = queueItem;
+        }
+        else
+        {
+            //Point to the very first item
+            queueItem = socket->synQueue;
+
+            //Reach the last item in the SYN queue
+            for (i = 1; queueItem->next != NULL; i++)
+                queueItem = queueItem->next;
+
+            //Make sure the SYN queue is not full
+            if (i >= socket->synQueueSize)
+                return;
+
+            //Allocate memory to save incoming data
+            queueItem->next = memPoolAlloc(sizeof(TcpSynQueueItem));
+            //Point to the newly created item
+            queueItem = queueItem->next;
+        }
+
+        //Failed to allocate memory?
+        if (queueItem == NULL)
+            return;
+
+#if (IPV4_SUPPORT == ENABLED)
+        //IPv4 is currently used?
+        if (pseudoHeader->length == sizeof(Ipv4PseudoHeader))
+        {
+            //Save the source IPv4 address
+            queueItem->srcAddr.length = sizeof(Ipv4Addr);
+            queueItem->srcAddr.ipv4Addr = pseudoHeader->ipv4Data.srcAddr;
+            //Save the destination IPv4 address
+            queueItem->destAddr.length = sizeof(Ipv4Addr);
+            queueItem->destAddr.ipv4Addr = pseudoHeader->ipv4Data.destAddr;
+        }
+        else
+#endif
+#if (IPV6_SUPPORT == ENABLED)
+            //IPv6 is currently used?
+            if (pseudoHeader->length == sizeof(Ipv6PseudoHeader))
+        {
+            //Save the source IPv6 address
+            queueItem->srcAddr.length = sizeof(Ipv6Addr);
+            queueItem->srcAddr.ipv6Addr = pseudoHeader->ipv6Data.srcAddr;
+            //Save the destination IPv6 address
+            queueItem->destAddr.length = sizeof(Ipv6Addr);
+            queueItem->destAddr.ipv6Addr = pseudoHeader->ipv6Data.destAddr;
+        }
+        else
+#endif
+        //Invalid pseudo header?
+        {
+            //This should never occur...
+            return;
+        }
+
+        //Initialize next field
+        queueItem->next = NULL;
+        //Underlying network interface
+        queueItem->interface = interface;
+        //Save the port number of the client
+        queueItem->srcPort = segment->srcPort;
+        //Save the initial sequence number
+        queueItem->isn = segment->seqNum;
+        //Default MSS value
+        queueItem->mss = MIN(TCP_DEFAULT_MSS, TCP_MAX_MSS);
+
+        //Get the maximum segment size
+        option = tcpGetOption(segment, TCP_OPTION_MAX_SEGMENT_SIZE);
+
+        //Specified option found?
+        if (option != NULL && option->length == 4)
+        {
+            //Retrieve MSS value
+            osMemcpy(&queueItem->mss, option->value, 2);
+            //Convert from network byte order to host byte order
+            queueItem->mss = ntohs(queueItem->mss);
+
+            //Debug message
+            // TRACE_DEBUG("Remote host MSS = %" PRIu16 "\r\n", queueItem->mss);
+
+            //Make sure that the MSS advertised by the peer is acceptable
+            queueItem->mss = MIN(queueItem->mss, TCP_MAX_MSS);
+            queueItem->mss = MAX(queueItem->mss, TCP_MIN_MSS);
+        }
+
+        //Notify user that a connection request is pending
+        tcpUpdateEvents(socket);
+
+        //The rest of the processing described in RFC 793 will be done
+        //asynchronously when socketAccept() function is called
+    }
+}
+
+int main()
+{
+    // Initialisation
+    socketInit();
+
+    Socket *socket;
+    IpPseudoHeader *pseudoHeader;
+    TcpHeader *segment;
+    size_t length;
+    uint32_t ackNum, seqNum;
+    uint8_t flags, dataOffset;
+    uint16_t checksum, srcPort;
+    struct socketModel *sModel;
+
+    segment = malloc(sizeof(TcpHeader) + sizeof(u_int8_t));
+    pseudoHeader = malloc(sizeof(IpPseudoHeader));
+
+    // creation of a TCP socket
+    socket = socketOpen(SOCKET_TYPE_STREAM, SOCKET_IP_PROTO_TCP);
+    socketListen(socket, 0);
+
+    // Creation of a "random" incomming package
+    // We assume the pseudo header is filled with ipv4 addresses
+
+    uint32_t srcAddr, destAddr;
+    uint16_t dataLength;
+    // IpAddr cannot be null
+    klee_make_symbolic(&srcAddr, sizeof(srcAddr), "srcAddr");
+    klee_make_symbolic(&destAddr, sizeof(destAddr), "destAddr");
+    klee_assume(srcAddr != 0);
+    klee_assume(destAddr != 0);
+    klee_make_symbolic(&dataLength, sizeof(dataLength), "dataLength");
+
+    pseudoHeader->length = sizeof(Ipv4PseudoHeader);
+    pseudoHeader->ipv4Data.srcAddr = srcAddr;
+    pseudoHeader->ipv4Data.destAddr = destAddr;
+    pseudoHeader->ipv4Data.reserved = 0;
+    pseudoHeader->ipv4Data.protocol = 6; // TCP protocol
+    pseudoHeader->ipv4Data.length = dataLength;
+    pseudoHeader->data[0] = 3;
+    pseudoHeader->data[1] = 220;
+    pseudoHeader->data[2] = 112;
+    pseudoHeader->data[3] = 94;
+
+    klee_make_symbolic(&ackNum, sizeof(ackNum), "ackNum");
+    klee_make_symbolic(&seqNum, sizeof(seqNum), "seqNum");
+    klee_make_symbolic(&flags, sizeof(flags), "flags");
+    klee_assume(0 <= flags && flags <= 31);
+    klee_make_symbolic(&checksum, sizeof(checksum), "checksum");
+    klee_make_symbolic(&dataOffset, sizeof(dataOffset), "dataOffset");
+    klee_assume(0 <= dataOffset && dataOffset <= 15);
+    klee_make_symbolic(&srcPort, sizeof(srcPort), "srcPort");
+    // The port cannot be null
+    klee_assume(srcPort != 0);
+
+    segment->srcPort = srcPort;
+    segment->destPort = socket->localPort;
+    segment->seqNum = seqNum;
+    segment->ackNum = ackNum;
+    segment->reserved1 = 0;
+    segment->dataOffset = dataOffset;
+    segment->flags = flags;
+    segment->reserved2 = 0;
+    segment->window = 26883; // Voir ce que c'est exactement
+    segment->checksum = checksum;
+    segment->urgentPointer = 0;
+    segment->options[0] = 0;
+
+    klee_make_symbolic(&length, sizeof(length), "length");
+
+    // We make a hard copy of the struct to check if the fields have
+    // changed after the call to the function
+    sModel = toSockModel(socket);
+
+    klee_assert(socket->state == TCP_STATE_LISTEN);
+
+    tcpStateListen(socket, socket->interface, pseudoHeader, segment, length);
+
+    int random;
+    klee_make_symbolic(&random, sizeof(int), "random");
+
+    // We see if the assertion is still true if more than one segment has been received
+    if (random)
+    {
+        klee_make_symbolic(&srcAddr, sizeof(srcAddr), "srcAddr");
+        klee_make_symbolic(&destAddr, sizeof(destAddr), "destAddr");
+        klee_assume(srcAddr != 0);
+        klee_assume(destAddr != 0);
+        klee_make_symbolic(&dataLength, sizeof(dataLength), "dataLength");
+
+        pseudoHeader->length = sizeof(Ipv4PseudoHeader);
+        pseudoHeader->ipv4Data.srcAddr = srcAddr;
+        pseudoHeader->ipv4Data.destAddr = destAddr;
+        pseudoHeader->ipv4Data.reserved = 0;
+        pseudoHeader->ipv4Data.protocol = 6; // TCP protocol
+        pseudoHeader->ipv4Data.length = dataLength;
+        pseudoHeader->data[0] = 3;
+        pseudoHeader->data[1] = 220;
+        pseudoHeader->data[2] = 112;
+        pseudoHeader->data[3] = 94;
+
+        klee_make_symbolic(&ackNum, sizeof(ackNum), "ackNum");
+        klee_make_symbolic(&seqNum, sizeof(seqNum), "seqNum");
+        klee_make_symbolic(&flags, sizeof(flags), "flags");
+        klee_assume(0 <= flags && flags <= 31);
+        klee_make_symbolic(&checksum, sizeof(checksum), "checksum");
+        klee_make_symbolic(&dataOffset, sizeof(dataOffset), "dataOffset");
+        klee_assume(0 <= dataOffset && dataOffset <= 15);
+        klee_make_symbolic(&srcPort, sizeof(srcPort), "srcPort");
+        // The port cannot be null
+        klee_assume(srcPort != 0);
+
+        segment->srcPort = srcPort;
+        segment->destPort = socket->localPort;
+        segment->seqNum = seqNum;
+        segment->ackNum = ackNum;
+        segment->reserved1 = 0;
+        segment->dataOffset = dataOffset;
+        segment->flags = flags;
+        segment->reserved2 = 0;
+        segment->window = 26883; // Voir ce que c'est exactement
+        segment->checksum = checksum;
+        segment->urgentPointer = 0;
+        segment->options[0] = 0;
+
+        klee_make_symbolic(&length, sizeof(length), "length");
+
+        tcpStateListen(socket, socket->interface, pseudoHeader, segment, length);
+    }
+
+    klee_assert(equalSocketModel(socket, sModel) &&
+                socket->state == TCP_STATE_LISTEN &&
+                (socket->synQueue != NULL ? (socket->synQueue->srcAddr.length != 0 &&
+                                             socket->synQueue->srcPort > 0 &&
+                                             socket->synQueue->destAddr.length != 0)
+                                          : 1));
+}

klee/model.c

@@ -0,0 +1,30 @@
+#include "model.h"
+#include <stdlib.h>
+
+struct socketModel* toSockModel(Socket* socket) {
+    struct socketModel* sModel;
+    sModel = malloc(sizeof(struct socketModel));
+
+    sModel->localIpAddr.length = socket->localIpAddr.length;
+    sModel->localIpAddr.ipv4Addr = socket->localIpAddr.ipv4Addr;
+    sModel->localPort = socket->localPort;
+    sModel->protocol = socket->protocol;
+    sModel->remoteIpAddr.length = socket->remoteIpAddr.length;
+    sModel->remoteIpAddr.ipv4Addr = socket->remoteIpAddr.ipv4Addr;
+    sModel->remotePort = socket->remotePort;
+    sModel->type = socket->type;
+
+    return sModel;
+}
+
+int equalSocketModel(Socket* socket, struct socketModel* sModel) {
+    return 
+        (sModel->localIpAddr.length == socket->localIpAddr.length &&
+        sModel->localIpAddr.ipv4Addr == socket->localIpAddr.ipv4Addr &&
+        sModel->localPort == socket->localPort &&
+        sModel->protocol == socket->protocol &&
+        sModel->remoteIpAddr.ipv4Addr == socket->remoteIpAddr.ipv4Addr &&
+        sModel->remoteIpAddr.length == socket->remoteIpAddr.length &&
+        sModel->remotePort == socket->remotePort &&
+        sModel->type == socket->type);
+}

klee/model.h

@@ -0,0 +1,14 @@
+#include "core/socket.h"
+
+struct socketModel {
+    uint_t type;
+    uint_t protocol;
+    IpAddr localIpAddr;
+    uint16_t localPort;
+    IpAddr remoteIpAddr;
+    uint16_t remotePort;
+};
+
+struct socketModel* toSockModel(Socket* socket);
+
+int equalSocketModel(Socket* socket, struct socketModel* sModel);

klee/net_config.h

@@ -0,0 +1,154 @@
+/**
+ * @file net_config.h
+ * @brief CycloneTCP configuration file
+ *
+ * @section License
+ *
+ * SPDX-License-Identifier: GPL-2.0-or-later
+ *
+ * Copyright (C) 2010-2020 Oryx Embedded SARL. All rights reserved.
+ *
+ * This file is part of CycloneTCP Open.
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
+ *
+ * @author Oryx Embedded SARL (www.oryx-embedded.com)
+ * @version 1.9.8
+ **/
+
+#ifndef _NET_CONFIG_H
+#define _NET_CONFIG_H
+
+//Trace level for TCP/IP stack debugging
+#define MEM_TRACE_LEVEL          0
+#define NIC_TRACE_LEVEL          0
+#define ETH_TRACE_LEVEL          0
+#define ARP_TRACE_LEVEL          0
+#define IP_TRACE_LEVEL           0
+#define IPV4_TRACE_LEVEL         0
+#define IPV6_TRACE_LEVEL         0
+#define ICMP_TRACE_LEVEL         0
+#define IGMP_TRACE_LEVEL         0
+#define ICMPV6_TRACE_LEVEL       0
+#define MLD_TRACE_LEVEL          0
+#define NDP_TRACE_LEVEL          0
+#define UDP_TRACE_LEVEL          0
+#define TCP_TRACE_LEVEL          0
+#define SOCKET_TRACE_LEVEL       0
+#define RAW_SOCKET_TRACE_LEVEL   0
+#define BSD_SOCKET_TRACE_LEVEL   0
+#define WEB_SOCKET_TRACE_LEVEL   0
+#define AUTO_IP_TRACE_LEVEL      0
+#define SLAAC_TRACE_LEVEL        0
+#define DHCP_TRACE_LEVEL         0
+#define DHCPV6_TRACE_LEVEL       0
+#define DNS_TRACE_LEVEL          0
+#define MDNS_TRACE_LEVEL         0
+#define NBNS_TRACE_LEVEL         0
+#define LLMNR_TRACE_LEVEL        0
+#define COAP_TRACE_LEVEL         0
+#define FTP_TRACE_LEVEL          0
+#define HTTP_TRACE_LEVEL         0
+#define MQTT_TRACE_LEVEL         0
+#define MQTT_SN_TRACE_LEVEL      0
+#define SMTP_TRACE_LEVEL         0
+#define SNMP_TRACE_LEVEL         0
+#define SNTP_TRACE_LEVEL         0
+#define TFTP_TRACE_LEVEL         0
+#define MODBUS_TRACE_LEVEL       0
+
+//Number of network adapters
+#define NET_INTERFACE_COUNT 1
+
+//Size of the MAC address filter
+#define MAC_ADDR_FILTER_SIZE 12
+
+//IPv4 support
+#define IPV4_SUPPORT ENABLED
+//Size of the IPv4 multicast filter
+#define IPV4_MULTICAST_FILTER_SIZE 4
+
+//IPv4 fragmentation support
+#define IPV4_FRAG_SUPPORT ENABLED
+//Maximum number of fragmented packets the host will accept
+//and hold in the reassembly queue simultaneously
+#define IPV4_MAX_FRAG_DATAGRAMS 4
+//Maximum datagram size the host will accept when reassembling fragments
+#define IPV4_MAX_FRAG_DATAGRAM_SIZE 8192
+
+//Size of ARP cache
+#define ARP_CACHE_SIZE 8
+//Maximum number of packets waiting for address resolution to complete
+#define ARP_MAX_PENDING_PACKETS 2
+
+//IGMP support
+#define IGMP_SUPPORT ENABLED
+
+//IPv6 support
+#define IPV6_SUPPORT ENABLED
+//Size of the IPv6 multicast filter
+#define IPV6_MULTICAST_FILTER_SIZE 8
+
+//IPv6 fragmentation support
+#define IPV6_FRAG_SUPPORT ENABLED
+//Maximum number of fragmented packets the host will accept
+//and hold in the reassembly queue simultaneously
+#define IPV6_MAX_FRAG_DATAGRAMS 4
+//Maximum datagram size the host will accept when reassembling fragments
+#define IPV6_MAX_FRAG_DATAGRAM_SIZE 8192
+
+//MLD support
+#define MLD_SUPPORT ENABLED
+
+//Neighbor cache size
+#define NDP_NEIGHBOR_CACHE_SIZE 8
+//Destination cache size
+#define NDP_DEST_CACHE_SIZE 8
+//Maximum number of packets waiting for address resolution to complete
+#define NDP_MAX_PENDING_PACKETS 2
+
+//TCP support
+#define TCP_SUPPORT ENABLED
+//Default buffer size for transmission
+#define TCP_DEFAULT_TX_BUFFER_SIZE (1430*2)
+//Default buffer size for reception
+#define TCP_DEFAULT_RX_BUFFER_SIZE (1430*2)
+//Default SYN queue size for listening sockets
+#define TCP_DEFAULT_SYN_QUEUE_SIZE 4
+//Maximum number of retransmissions
+#define TCP_MAX_RETRIES 5
+//Selective acknowledgment support
+#define TCP_SACK_SUPPORT DISABLED
+
+//UDP support
+#define UDP_SUPPORT ENABLED
+//Receive queue depth for connectionless sockets
+#define UDP_RX_QUEUE_SIZE 4
+
+//Raw socket support
+#define RAW_SOCKET_SUPPORT DISABLED
+//Receive queue depth for raw sockets
+#define RAW_SOCKET_RX_QUEUE_SIZE 4
+
+//Number of sockets that can be opened simultaneously
+#define SOCKET_MAX_COUNT 1
+
+//LLMNR responder support
+#define LLMNR_RESPONDER_SUPPORT ENABLED
+
+//FTP client support
+#define FTP_CLIENT_SUPPORT ENABLED
+
+#endif

klee/os_port_config.h

@@ -0,0 +1,36 @@
+/**
+ * @file os_port_config.h
+ * @brief RTOS port configuration file
+ *
+ * @section License
+ *
+ * SPDX-License-Identifier: GPL-2.0-or-later
+ *
+ * Copyright (C) 2010-2020 Oryx Embedded SARL. All rights reserved.
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software Foundation,
+ * Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
+ *
+ * @author Oryx Embedded SARL (www.oryx-embedded.com)
+ * @version 1.9.8
+ **/
+
+#ifndef _OS_PORT_CONFIG_H
+#define _OS_PORT_CONFIG_H
+
+//Select underlying RTOS
+#define USE_NO_RTOS
+#define GPL_LICENSE_TERMS_ACCEPTED
+
+#endif

klee/syn_received/Makefile

@@ -0,0 +1,49 @@
+CFILES = \
+	$(wildcard *.c) \
+	../model.c \
+	../../src/cyclone_tcp/core/net.c \
+	../../src/cyclone_tcp/core/tcp.c \
+	../../src/common/os_port_none.c \
+	../../src/cyclone_tcp/core/socket.c \
+	../../src/cyclone_tcp/core/nic.c \
+	../../src/cyclone_tcp/ipv4/arp.c \
+	../../src/cyclone_tcp/ipv4/ipv4_frag.c \
+	../../src/cyclone_tcp/ipv4/igmp.c \
+	../../src/cyclone_tcp/dhcp/dhcp_client.c \
+	../../src/cyclone_tcp/ipv6/ipv6_frag.c \
+	../../src/cyclone_tcp/ipv6/mld.c \
+	../../src/cyclone_tcp/ipv6/ndp.c \
+	../../src/cyclone_tcp/dns/dns_cache.c \
+	../../src/cyclone_tcp/ipv6/ipv6.c \
+	../../src/cyclone_tcp/core/ethernet.c \
+	../../src/cyclone_tcp/core/net_misc.c \
+	../../src/cyclone_tcp/core/tcp_misc.c \
+	../../src/cyclone_tcp/core/ip.c \
+	../../src/cyclone_tcp/core/net_mem.c \
+	../../src/common/cpu_endian.c \
+	../../src/cyclone_tcp/ipv4/ipv4.c \
+	../../src/cyclone_tcp/core/tcp_timer.c
+
+BCFILES = $(patsubst %.c, %.bc, $(CFILES))
+
+PATH_TO_KLEE = /home/cluzel/klee/klee/include/
+
+INCLUDES = \
+	-I../ \
+	-I../../src/cyclone_tcp/ \
+	-I../../src/common/ \
+	-I $(PATH_TO_KLEE)
+
+all: program.bc
+	klee -warnings-only-to-file $<
+
+%.bc: %.c
+	clang-6.0 -c -g -O0 -emit-llvm $(INCLUDES) $< -o $@
+
+program.bc: $(BCFILES)
+	llvm-link-6.0 $(BCFILES) -o $@
+
+.PHONY: clean all
+
+clean:
+	rm -rf $(BCFILES) klee-* program.bc

klee/syn_received/syn_received.c

@@ -0,0 +1,200 @@
+#include "core/socket.h"
+#include "klee/klee.h"
+#include "core/tcp_misc.h"
+#include <assert.h>
+#include <stdlib.h>
+#include "model.h"
+
+
+void tcpStateEstablished(Socket *socket, TcpHeader *segment,
+   const NetBuffer *buffer, size_t offset, size_t length)
+{
+   uint_t flags = 0;
+
+   //Debug message
+   // TRACE_DEBUG("TCP FSM: ESTABLISHED state\r\n");
+
+   //First check sequence number
+   if(tcpCheckSequenceNumber(socket, segment, length))
+      return;
+
+   //Check the RST bit
+   if(segment->flags & TCP_FLAG_RST)
+   {
+      //Switch to the CLOSED state
+      tcpChangeState(socket, TCP_STATE_CLOSED);
+
+      //Number of times TCP connections have made a direct transition to the
+      //CLOSED state from either the ESTABLISHED state or the CLOSE-WAIT state
+      // MIB2_INC_COUNTER32(tcpGroup.tcpEstabResets, 1);
+      // TCP_MIB_INC_COUNTER32(tcpEstabResets, 1);
+
+      //Return immediately
+      return;
+   }
+
+   //Check the SYN bit
+   if(tcpCheckSyn(socket, segment, length))
+      return;
+   //Check the ACK field
+   if(tcpCheckAck(socket, segment, length))
+      return;
+   //Process the segment text
+   if(length > 0)
+      tcpProcessSegmentData(socket, segment, buffer, offset, length);
+
+   //Check the FIN bit
+   if(segment->flags & TCP_FLAG_FIN)
+   {
+      //The FIN can only be acknowledged if all the segment data
+      //has been successfully transferred to the receive buffer
+      if(socket->rcvNxt == (segment->seqNum + length))
+      {
+         //Advance RCV.NXT over the FIN
+         socket->rcvNxt++;
+         //Send an acknowledgment for the FIN
+         tcpSendSegment(socket, TCP_FLAG_ACK, socket->sndNxt, socket->rcvNxt, 0, FALSE);
+         //Switch to the CLOSE-WAIT state
+         tcpChangeState(socket, TCP_STATE_CLOSE_WAIT);
+      }
+   }
+
+#if (TCP_CONGEST_CONTROL_SUPPORT == ENABLED)
+   //Duplicate AK received?
+   if(socket->dupAckCount > 0)
+      flags = SOCKET_FLAG_NO_DELAY;
+#endif
+
+   //The Nagle algorithm should be implemented to coalesce
+   //short segments (refer to RFC 1122 4.2.3.4)
+   tcpNagleAlgo(socket, flags);
+}
+
+void tcpStateSynReceived(Socket *socket, TcpHeader *segment,
+                         const NetBuffer *buffer, size_t offset, size_t length)
+{
+    //Debug message
+    // TRACE_DEBUG("TCP FSM: SYN-RECEIVED state\r\n");
+
+    //First check sequence number
+    if (tcpCheckSequenceNumber(socket, segment, length))
+        return;
+
+    //Check the RST bit
+    if (segment->flags & TCP_FLAG_RST)
+    {
+        //Return to CLOSED state
+        tcpChangeState(socket, TCP_STATE_CLOSED);
+
+        //Number of times TCP connections have made a direct transition to the
+        //CLOSED state from either the SYN-SENT state or the SYN-RECEIVED state
+        //MIB2_INC_COUNTER32(tcpGroup.tcpAttemptFails, 1);
+        //TCP_MIB_INC_COUNTER32(tcpAttemptFails, 1);
+
+        //Return immediately
+        return;
+    }
+
+    //Check the SYN bit
+    if (tcpCheckSyn(socket, segment, length))
+        return;
+
+    //If the ACK bit is off drop the segment and return
+    if (!(segment->flags & TCP_FLAG_ACK))
+        return;
+
+    //Make sure the acknowledgment number is valid
+    if (segment->ackNum != socket->sndNxt)
+    {
+        //If the segment acknowledgment is not acceptable, form a reset
+        //segment and send it
+        tcpSendSegment(socket, TCP_FLAG_RST, segment->ackNum, 0, 0, FALSE);
+
+        //Drop the segment and return
+        return;
+    }
+
+    //Update the send window before entering ESTABLISHED state (refer to
+    //RFC 1122, section 4.2.2.20)
+    socket->sndWnd = segment->window;
+    socket->sndWl1 = segment->seqNum;
+    socket->sndWl2 = segment->ackNum;
+
+    //Maximum send window it has seen so far on the connection
+    socket->maxSndWnd = segment->window;
+
+    //Enter ESTABLISHED state
+    tcpChangeState(socket, TCP_STATE_ESTABLISHED);
+    //And continue processing...
+    tcpStateEstablished(socket, segment, buffer, offset, length);
+}
+
+int main()
+{
+    // Initialisation
+    socketInit();
+
+    Socket *socket;
+    IpPseudoHeader *pseudoHeader;
+    TcpHeader *segment;
+    size_t length;
+    uint32_t ackNum, seqNum;
+    uint8_t flags, dataOffset;
+    uint16_t checksum, srcPort;
+    struct socketModel *sModel;
+
+    segment = malloc(sizeof(TcpHeader) + sizeof(u_int8_t));
+    pseudoHeader = malloc(sizeof(IpPseudoHeader));
+
+    // creation of a TCP socket
+    socket = socketOpen(SOCKET_TYPE_STREAM, SOCKET_IP_PROTO_TCP);
+
+    // TODO: See if it is the correct way to process.
+    // Maybe open the connection by following the real call of the function
+    // is a better way to do.
+    tcpChangeState(socket, TCP_STATE_SYN_RECEIVED);
+
+    // Creation of a "random" incomming package
+    // We assume the pseudo header is filled with ipv4 addresses
+
+    klee_make_symbolic(&ackNum, sizeof(ackNum), "ackNum");
+    klee_make_symbolic(&seqNum, sizeof(seqNum), "seqNum");
+    klee_make_symbolic(&flags, sizeof(flags), "flags");
+    klee_assume(0 <= flags && flags <= 31);
+    klee_make_symbolic(&checksum, sizeof(checksum), "checksum");
+    klee_make_symbolic(&dataOffset, sizeof(dataOffset), "dataOffset");
+    klee_assume(0 <= dataOffset && dataOffset <= 15);
+    klee_make_symbolic(&srcPort, sizeof(srcPort), "srcPort");
+    // The port cannot be null
+    klee_assume(srcPort != 0);
+
+    segment->srcPort = srcPort;
+    segment->destPort = socket->localPort;
+    segment->seqNum = seqNum;
+    segment->ackNum = ackNum;
+    segment->reserved1 = 0;
+    segment->dataOffset = dataOffset;
+    segment->flags = flags;
+    segment->reserved2 = 0;
+    segment->window = 26883; // Voir ce que c'est exactement
+    segment->checksum = checksum;
+    segment->urgentPointer = 0;
+    segment->options[0] = 0;
+
+    klee_make_symbolic(&length, sizeof(length), "length");
+
+    // We make a hard copy of the struct to check if the fields have
+    // changed after the call to the function
+    sModel = toSockModel(socket);
+
+    klee_assert(socket->state == TCP_STATE_SYN_RECEIVED);
+
+    tcpStateSynReceived(socket, segment, NULL, 0, 0);
+
+    klee_assert(equalSocketModel(socket, sModel) &&
+                (socket->state == TCP_STATE_SYN_RECEIVED ||
+                 socket->state == TCP_STATE_ESTABLISHED ||
+                 socket->state != TCP_STATE_CLOSE_WAIT ||
+                 (socket->state == TCP_STATE_CLOSED &&
+                  socket->resetFlag)));
+}