diff --git a/.gitignore b/.gitignore index b315da7..4598557 100644 --- a/.gitignore +++ b/.gitignore @@ -11,3 +11,5 @@ gnatprove/ libs/ prove-loc.xml codepeer/ +*.bc +klee-* diff --git a/klee/Makefile b/klee/Makefile new file mode 100644 index 0000000..57f62b1 --- /dev/null +++ b/klee/Makefile @@ -0,0 +1,9 @@ +TOPTARGETS := all clean + +SUBDIRS := $(wildcard */.) + +$(TOPTARGETS): $(SUBDIRS) +$(SUBDIRS): + $(MAKE) -C $@ $(MAKECMDGOALS) + +.PHONY: $(TOPTARGETS) $(SUBDIRS) \ No newline at end of file diff --git a/klee/close_wait/Makefile b/klee/close_wait/Makefile new file mode 100644 index 0000000..6c5e196 --- /dev/null +++ b/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 diff --git a/klee/close_wait/close_wait.c b/klee/close_wait/close_wait.c new file mode 100644 index 0000000..0526293 --- /dev/null +++ b/klee/close_wait/close_wait.c @@ -0,0 +1,107 @@ +#include "core/socket.h" +#include "klee/klee.h" +#include "core/tcp_misc.h" +#include +#include +#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))); +} diff --git a/klee/closed_state/Makefile b/klee/closed_state/Makefile new file mode 100644 index 0000000..a0d43ce --- /dev/null +++ b/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 diff --git a/klee/closed_state/closed_state.c b/klee/closed_state/closed_state.c new file mode 100644 index 0000000..a391bd0 --- /dev/null +++ b/klee/closed_state/closed_state.c @@ -0,0 +1,207 @@ +#include "core/socket.h" +#include "klee/klee.h" +#include +// #include "core/tcp_fsm.h" +#include + +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; +} \ No newline at end of file diff --git a/klee/closing/Makefile b/klee/closing/Makefile new file mode 100644 index 0000000..03c065a --- /dev/null +++ b/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 diff --git a/klee/closing/closing.c b/klee/closing/closing.c new file mode 100644 index 0000000..78ffaaa --- /dev/null +++ b/klee/closing/closing.c @@ -0,0 +1,105 @@ +#include "core/socket.h" +#include "klee/klee.h" +#include "core/tcp_misc.h" +#include +#include +#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))); +} diff --git a/klee/fin_wait_1/Makefile b/klee/fin_wait_1/Makefile new file mode 100644 index 0000000..03c065a --- /dev/null +++ b/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 diff --git a/klee/fin_wait_1/fin_wait_1.c b/klee/fin_wait_1/fin_wait_1.c new file mode 100644 index 0000000..b75130d --- /dev/null +++ b/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 +#include +#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))); +} diff --git a/klee/fin_wait_2/Makefile b/klee/fin_wait_2/Makefile new file mode 100644 index 0000000..03c065a --- /dev/null +++ b/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 diff --git a/klee/fin_wait_2/fin_wait_2.c b/klee/fin_wait_2/fin_wait_2.c new file mode 100644 index 0000000..41b6685 --- /dev/null +++ b/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 +#include +#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))); +} diff --git a/klee/listen/Makefile b/klee/listen/Makefile new file mode 100644 index 0000000..03c065a --- /dev/null +++ b/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 diff --git a/klee/listen/listen.c b/klee/listen/listen.c new file mode 100644 index 0000000..7cf2fbe --- /dev/null +++ b/klee/listen/listen.c @@ -0,0 +1,280 @@ +#include "core/socket.h" +#include "klee/klee.h" +#include "core/tcp_misc.h" +#include +#include +#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)); +} diff --git a/klee/model.c b/klee/model.c new file mode 100644 index 0000000..3a90622 --- /dev/null +++ b/klee/model.c @@ -0,0 +1,30 @@ +#include "model.h" +#include + +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); +} \ No newline at end of file diff --git a/klee/model.h b/klee/model.h new file mode 100644 index 0000000..f15277d --- /dev/null +++ b/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); \ No newline at end of file diff --git a/klee/net_config.h b/klee/net_config.h new file mode 100644 index 0000000..b28c1b8 --- /dev/null +++ b/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 diff --git a/klee/os_port_config.h b/klee/os_port_config.h new file mode 100644 index 0000000..5d93544 --- /dev/null +++ b/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 diff --git a/klee/syn_received/Makefile b/klee/syn_received/Makefile new file mode 100644 index 0000000..03c065a --- /dev/null +++ b/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 diff --git a/klee/syn_received/syn_received.c b/klee/syn_received/syn_received.c new file mode 100644 index 0000000..fa02a4a --- /dev/null +++ b/klee/syn_received/syn_received.c @@ -0,0 +1,200 @@ +#include "core/socket.h" +#include "klee/klee.h" +#include "core/tcp_misc.h" +#include +#include +#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))); +} diff --git a/klee/syn_sent/Makefile b/klee/syn_sent/Makefile new file mode 100644 index 0000000..03c065a --- /dev/null +++ b/klee/syn_sent/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 diff --git a/klee/syn_sent/syn_sent.c b/klee/syn_sent/syn_sent.c new file mode 100644 index 0000000..19d3005 --- /dev/null +++ b/klee/syn_sent/syn_sent.c @@ -0,0 +1,181 @@ +#include "core/socket.h" +#include "klee/klee.h" +#include "core/tcp_misc.h" +#include +#include +#include "model.h" + + +void tcpStateSynSent(Socket *socket, TcpHeader *segment, size_t length) +{ + TcpOption *option; + + //Debug message + // TRACE_DEBUG("TCP FSM: SYN-SENT state\r\n"); + + //Check the ACK bit + if(segment->flags & TCP_FLAG_ACK) + { + //Make sure the acknowledgment number is valid + if(segment->ackNum != socket->sndNxt) + { + //Send a reset segment unless the RST bit is set + if(!(segment->flags & TCP_FLAG_RST)) + tcpSendSegment(socket, TCP_FLAG_RST, segment->ackNum, 0, 0, FALSE); + + //Drop the segment and return + return; + } + } + + //Check the RST bit + if(segment->flags & TCP_FLAG_RST) + { + //Make sure the ACK is acceptable + if(segment->flags & TCP_FLAG_ACK) + { + //Enter 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); + } + + //Drop the segment and return + return; + } + + //Check the SYN bit + if(segment->flags & TCP_FLAG_SYN) + { + //Save initial receive sequence number + socket->irs = segment->seqNum; + //Initialize RCV.NXT pointer + socket->rcvNxt = segment->seqNum + 1; + + //If there is an ACK, SND.UNA should be advanced to equal SEG.ACK + if(segment->flags & TCP_FLAG_ACK) + socket->sndUna = segment->ackNum; + + //Compute retransmission timeout + tcpComputeRto(socket); + + //Any segments on the retransmission queue which are thereby + //acknowledged should be removed + tcpUpdateRetransmitQueue(socket); + + //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(&socket->smss, option->value, 2); + //Convert from network byte order to host byte order + socket->smss = ntohs(socket->smss); + + //Debug message + // TRACE_DEBUG("Remote host MSS = %" PRIu16 "\r\n", socket->smss); + + //Make sure that the MSS advertised by the peer is acceptable + socket->smss = MIN(socket->smss, TCP_MAX_MSS); + socket->smss = MAX(socket->smss, TCP_MIN_MSS); + } + +#if (TCP_CONGEST_CONTROL_SUPPORT == ENABLED) + //Initial congestion window + socket->cwnd = MIN(TCP_INITIAL_WINDOW * socket->smss, socket->txBufferSize); +#endif + + //Check whether our SYN has been acknowledged (SND.UNA > ISS) + if(TCP_CMP_SEQ(socket->sndUna, socket->iss) > 0) + { + //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; + + //Form an ACK segment and send it + tcpSendSegment(socket, TCP_FLAG_ACK, socket->sndNxt, socket->rcvNxt, 0, FALSE); + //Switch to the ESTABLISHED state + tcpChangeState(socket, TCP_STATE_ESTABLISHED); + } + else + { + //Form an SYN ACK segment and send it + tcpSendSegment(socket, TCP_FLAG_SYN | TCP_FLAG_ACK, socket->iss, socket->rcvNxt, 0, TRUE); + //Enter SYN-RECEIVED state + tcpChangeState(socket, TCP_STATE_SYN_RECEIVED); + } + } +} + +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) + sizeof(u_int8_t)); + + // 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_SENT); + + 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); + + 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; + 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_SENT); + + tcpStateSynSent(socket, segment, length); + + klee_assert(equalSocketModel(socket, sModel) && + (socket->state == TCP_STATE_SYN_SENT || + socket->state == TCP_STATE_SYN_RECEIVED || + socket->state == TCP_STATE_ESTABLISHED || + (socket->state == TCP_STATE_CLOSED && + socket->resetFlag))); + +}