35C3 preroll music
Herald-Angel: The next talk is by Hannes
Mehnert, you can see him here already.
It's called Transmission Control Protocol,
also known as TCP and Hannes Mehnert works
at a non-profit organization in Berlin.
It's called Center for the cultivation of
technology. And he also works on an open
... no, Mirage OS. If you don't know it,
maybe you can find out what it is. And he
researches in several engineering areas
such as: programming languages, network
protocols, security protocols and many
many more. So give him a warm applause for
his talk.
Applause
Hannes Mehnert: Thank you. Yes, today I
want to talk a bit about the Transmission
Control Protocol and the Internet Protocol
suite. So, what is it all about? It's a
foundation talk here, so if you already
know TCP/IP by heart then maybe only the
last five minutes will be of interest for
you, otherwise. So, if you want to connect
your laptop or if you want to browse to a
Web site somewhere, you want to read that
Web site, it is that, the client on your
laptop or the browser that sends an HTTP
request to the web server host. So it sends
an HTTP request which is specified by the
HTTP protocol. It's maybe GET /. It's a
common method of getting the main page of
a website, but how is this information
actually transmitted to the server? That
is the question and the motivation for
this talk. So that is something I want to
go deep into the answer for the question.
So let's look a bit at the network
topology. So, on the left hand side we
have the laptop which sends to some server
a GET request. You can see that by the
dashed arrow and the laptop itself is
connected, likely via a wireless network
to the Internet. But what is actually the
Internet? Well, the Internet is a
collection of computers and your laptop or
anyone's mobile phone is likely connected
to a router, a router is just a normal
computer which has some knowledge about
the network and that router is likely
connected via fiber or a satellite or any
other link, can also be an ethernet cable
to another router or to several routers.
And in this picture you can only see two
routers, the router A and router B, but
there may be any number of routers or
nearly any number of routers in between
you and the server. So here the router B
is connected via Ethernet, which is just a
physical cable to the server and Ethernet
is a protocol which is talked over the
cable. So I won't to go into the physical
network connectivity like fibers and
satellite and cables and copper cables, in
this talk at all but I will start with the
layer which is on top of the physical
medium. So the first one is the data link
layer. And, well, what is the data link
layer? What's task is it? It has a scope
of a network and it only spans over the
local network to which a host is
connected. So in this picture, only the
laptop and the router A share the same
data link layer as well as the router B
and the router A, they share the same data
link layer. It's also the case that router
B and the server share the same data link
layer. What is the task of the data link
layer? Well it's pretty easy, it just
moves Internet layer packets between two
different hosts that sit on the same link.
So, the data link layers really it's only
purpose is to provide an abstraction over
the physical thing and how many bytes you
can transport on the physical media over
the link. So the next layer is already the
Internet layer. The internet layer which
task is to transport packets across
multiple networks. So as you have seen in
the diagram there are router A and router
B, they are both connected to several data
link layers and they use the Internet
layer in order to transport packets
across. The Internet layer solves already
the issue of addressing by providing for
every host an IP address. IP address is
actually the Internet Protocol address and
the Internet layer provides another task
or solves another task which is routing so
it forwards packets to the next router
which is hope fully closer to the final
destination. That is the task. The
Internet layer also has support for
fragmentation. So if your higher layer
sends something which is way too big for
the data link layer, then the Internet
layer can fragment that and the other side
has to reassemble it. What is on top of
the Internet layer is the transport layer.
So the transport layer establishes host to
host connectivity. It does multiplexing
usually using source and destination ports
and there are two widely used transport
layer protocols, which I will go into more
detail in this talk, which is the user
datagram protocol and the transmission
control protocol, that's UDP and TCP and
they have different properties. So UDP is
unreliable and it is not ordered and it is
only an abstraction over datagrams and it
has on the advantage side, a very low
overhead. Whereas TCP is a reliable and
ordered byte stream, so you have a
reliable byte stream which you can work
on. The downside of TCP is that it's
connection establishment and teardown is
slightly more complex. In UDP, you just
don't have to establish a connection and
teardown and connect. But in TCP you have
to synchronize the two hosts. Then on top
of the transport layer we have the
application layer and the application
layer just exchanges application data over
the transport layer. So some examples for
application layers are HTTP or TLS or DNS.
So in the first example we saw there was
HTTP and HTTP was used to send the GET
request. So that is all application layer,
which I won't focus on in this talk at
all. For the lower layers the application
layers, just payload so it's just some
arbitrary data. So if we look again at
that picture and we draw the different
layers which are supported or which are
used by the different devices, we end up
with a diagram similar to that. So here on
the left we have the laptop again which
has all four layers and then we have the
routers in the middle which are only using
the data link and the Internet layer and
then on the right hand side we have the
server which also has all four layers. So
the transport layer is really host to
host, so the TCP we saw earlier, the TCP
is establishing a connection from the
laptop to the server and on top of TCP. So
on top of the transport layer there is the
process to process communication so the
application layer which is the web browser
talking to the web server. So only on the
highest layer here, we have the GET
request. And the routers in the middle
they don't have to inspect or they don't
have to use information of the transport
or application layer from the laptop or
the server. So the routers just for using
the Internet layer they forward packets to
the next router or to the final
destination. So the laptop first sends the
whole TCP segment or a TCP packet to the
router and the router A decides, oh yeah
we'll forward it to router B because
router B is more closer to the final
destination than myself and the router B
says, oh yeah well I actually know and I'm
connected via ethernet to the final
destination so I will just forward it to
the server. That's how the data flow of
such a connection would look like. How
does a packet actually look like? So we
have seen that at the application layer we
have the application data, which is here
in blue and that one is just the GET
request. Then the transport layer actually
prefixes the application data with a
header which is a common header that
encodes some data, we will look into the
TCP header in more detail soon, then the
Internet layer also adds a header, a
prefix: the IP header, which is just put
in front of the TCP header. And then the
data link layer, well that is the lowest
layer we actually care about and that one
will likely prepend a header and append a
footer in order to synchronize or to make
sure that the physical wire only has only
sees a single packet at a time. So as you
can see from the layering from those two
pictures on the one side you have the
bottom two up layer and every layer if you
go down from the application to the
transport, to the Internet, to data link,
they basically add some header information
and the Internet layer for example that
takes the TCP header, so the transport
layer and the application layer as
payload, so it doesn't care that it is
TCP, it could as well be UDP in this case.
So what is actually in the. So I will not
go into the data link layer details at
all, but here is the header of an IP
version 4 frame or packet and that one is
at least 20 bytes, it contains various
fields. The first one is a four bit
version, which usually is version 4 in our
current world. Then it has a 4 bits header
length, which is a header length invert,
so in multiples of 32 bits. Then it has
some not really used stuff I won't deal
with in this talk. It has the total length
field with just 16 bits and it describes
how long the entire IP frame is. Then it
has an identification, which is also a 16
bit unique number and the 16 bits for
fragmentation flags and offset. And that
is crucial. So, if the IP header decides:
oh yeah well the package, the application
data you sent me is way too big for this
data link, I need to fragment it, then it
will just reuse the very same
identification number and then use here
the 16 bits in the fragmentation flags and
offset in order to portion that
application data into multiple IP
fragments. Then it has a field which is 8
bit, so 1 entire byte, it's the time to
live and it's actually not a timestamp but
it's only a count. So how many routers
should this package live. How long should
this package live and every router
decreases that time to live by 1. Then it
has a 1 byte protocol field which
specifies what is the type of the payload
carried by this IP version 4 packet, then
it has a 16 bit header checksum which is
the CRC checksum to avoid that some bits
got flipped on the transport. Then we can
see the source IP address and the
destination IP address which is, yeah I
mean, the source IP address is the IP
address of my laptop and the destination
IP address, is the IP address of the
server. And then after those 20 bytes you
have either IP options, if the header
length was more than 20 bytes or you have
directly the payload. Now for the protocol
field here there are various types and
various types are predefined. 1 is ICMP
which is the internet control message
protocol, I will talk a bit about that
which is the product field, there the
number set to 1, then for TCP it's set to
6 and for UDP it's 17. We have other
protocols which can be carried over an IP
frame or an IP packet but I won't go into
the details here. As you can see there are
at least 255 numbers here in the product
field. So because it's 8 bit long, you can
store up to 256 different numbers in
there. So ICMP is a protocol I haven't
talked about at all but it is the internet
control message protocol. So it sits on
top of IP and its purpose is on the one
side, to deliver error messages such as
destination host unreachable or time to
live exceeded and on the other side it can
also carry operational information like
diagnostics. There's one program which you
may know which is called ping. The purpose
of ping is to send an ICMP echo request to
a remote host and the remote host is then
supposed to send the very same packet with
only 1 single bit flipped and send that back
to you and that is an ICMP echo reply. And
if you can successfully ping another host
you can verify that the other host has at
least ip connectivity up and online. OK,
Let's look into the next layer which is
the transport layer. And at first we will
look into a UDP header. A UDP header has
only eight bytes. it contains. It consists
of a source port, the destination port.
Then the length of the entire UDP frame
and the checksum the checksum is again a
16 bit field computed over the entire
payload and the header plus some IP pseudo
header. So this actually carries the
information of the source and destination
ip address inside of itself. UDP as I
mentioned is unreliable, unordered and its
advantage is that the low overhead data
grams as you can see it adds 8 bytes to the
to the payload whereas IP already added 20
bytes to the payload. Here's a simple Unix
program which is a UDP client. This
program does not compile because I left
out some bits but in order to see what how
do you actually use this whole IP stack.
So the IP stack the TCP IP stack is
usually embedded in the kernel and as a
programmer as an API programmer you have the
API provided by the Unix sockets API. And
that one usually contains of the very same
five or seven functions which is the first
one is a socket socket opens or creates a
file descriptor and you specifie the
address family and the socket type. So
this is the adress family Internet and the
socket is a datagram socket. It's called
DGRAM in Unix. Once that is created then
you for a UDP client and you just say Oh I
will use the function "send to" which
takes a socket file descriptor. So just
the file descriptor and then some data and
will just send it to the other side since
it's unreliable it's just fire and forget.
Then afterwards we close the socket file
descriptor because we are nice here and we
try to be nice the other side. So if you
don't have a UDP client but if you want to
implement a UDP server or a UDP listener
what do you do is you again create a
socket then you have the function which is
called bind. Bind binds it to a combined
into a specific IP address on your server
or on your network stack then you say
receive from recieve from takes the socket
file descriptor and a buffer and some
maximum size and an offset. And yeah you
just receive from will only return once
you actually receive the UDP frame on that
IP address and port and then you then we
print out that we received some packets
and we close the socket file descriptor.
So that's UDP. UDP is used for a variety
of protocols and that's crucial to have it
TCP on the other hand is a bit bigger. So
instead of eight bytes header TCP adds
another 20 bytes of header what does the
TCP header contain? Well similar to UDP it
contains a source port and Destination Port
both again 16 bits then it contains two
sequence numbers one is the sequence
number itself it's a 32 bit number and one
is the acknowledgement number which is the
last sequence number we have seen from the
other side then TCP contains a data offset
date offset is similar to the header
length field so TCP a TCP segment may also
contain some options so the header may
contain options before a payload. That's
why we need a data set field in order to
be able to find out where this extra
payload start then TCP has certain flags
and some of these flags a some of these
flags are just a single bit of values and
some of them I mentioned down here of
which I will go into more detail later
which is acknowledgement or ACK
synchronize or SYN and finished or FIN
there is also reset and some urgent stuff
I will not go into detail of that then we
have a six sixteen bit field which is the
window size which is the size of the
receive buffer then we have again sixteen
bit field checksum and then we have some
space for the urgent stuff I will not go
into detail. A TCP client if you program
it in a Unix way. You have a very similar
API as we have seen in the UDP. So we
first call. We first create a file
descriptor using the socket system call
which we give again the adress family INET
and the SOCK_STREAM which is the since we
are stream oriented. It's it's the name of
the TCP. It's the name for TCP socket.
Then as a TCP client we connect using the
socket file descriptor to a remote host.
And then once we are connected so connect
will only return once a TCP session has been
established. Then we say here receive. So
we receive on the socket file descriptor.
The specific buffer buffer then we print
it and then we close the socket file
descriptor again. The TCP listener is very
similar. So well first we create a socket.
Then we bind it and bind specifies the IP
address and also the port number. Then we
use a function called listen on the socket
file descriptor and then we enter a loop.
And so now we wait for client connections
which appear at some point. And for every
client connection we well we call accept
and accept returns whenever there was a
client which successfully established a
TCP connection. What accept returns is a
new file descriptor so another file
descriptor not the same as a socket file
descriptor. So the socket file descriptor
we call again except on it at a later
point. Usually you then handle any work on
the client connection on this new_fd. You
handle that in a separate process or set a
separate thread or a separate task in
order to enable the server to accept
another connection while you are handling
the the one client connection. Then we
just do some printf output and we send
hello world to the client to the client
connection so to this new file descriptor
then we close it and we start from the
while(1) and we accept a new client
socket. So that is TCP listener as we have
seen it as you will see it in an in any
network program. Now TCP as I mentioned it
has to do some work in order to establish
a section a session and to tear down the
main work which needs to be done is to
synchronize the initial sequence numbers
because we have seen in the header that we
have this sequence number and somehow we
need to transform that information to the
other side. So here's the TCP state machine
which is which has initially been part of
the RFC, which is the specification
for TCP and also duplicated in books like
Stevens design and implementation of the
of TCP IP and TCP IP illustrated and so
on. So you can see it is it has here one
specific state which is listen and listen
is as we've seen in the server
implementation if you call listen then you
are in the listen stand in the listen
state and you always start well you always
end up in the in the closed state after
you've called Close. Basically I will go
into more detail of connection
establishment and teardown right now. So
on the connection establishment we have
seen on the client side we start with the
socket in the closed state. Then we say
the Unix call connect on that socket and
that connect. Does send an initial TCP
segment to the server side which has the
synchronized flag set to true or set to
one and the sequence number is some
artificial number some random 32 bits
integer number. So just call it "a" here.
The State of the file descriptor goes from
closed to SYN_SENT and SYN_SENT yeah well
we just have sent out the the synchronize
segment so aTCP segment which doesn't carry
any data but only the TCP header on the
server side. We had prepared previously.
We started in a closed state then we
called Listen. Then we end up in a listen
state. Now in the listen state we call
accept and accept blocks until the SYN is
received and once the SYN is received, a
new socket is a new file descriptor
spawned and that one ends up in the
SYN_RECIEVED state. The server sends out
the TCP segment again without any data but
the SYN and acknowledgement flags are set
and the sequence number is sent to some b
and the acknowledgement number is set to
a+1. So the acknowledgement number
acknowledges that the SYN was received
with the sequence number a +1. Upon
the client receiving that SYN and ACK, it is
in the established state and it will send out
an acknowledgement segment so that the
other side the server knows. Oh yeah. My
segment has been received and that one is
sent with the sequence number of a+1
because a was already used here and the
SYN flag consumes one one byte or 1 in the
sequence number range and the
acknowledgement number is also set to
b + 1. So that is the sequence number
from here plus 1. Once that is received
the server ends up in the established
state. Sequence numbers. Yeah well it's a
good idea of both. Pick a random initial
sequence number for each connection
otherwise we can get into some nasty
attacks. The acknowledgement number is the
next sequence number from the other hosts
and the sequence numbers always increased
for each byte of data. And for the SYN and
FIN flags which only a single bits each
sequence number must be not acknowledged
and each sent packet is retransmited unless
it is acknowledged after a certain timeout
and after certain retransmit time after trying
it several times at some point the TCP
stack gives up the trardown since I am a
bit short on time I will skip that. TCP
provides us with the flow control. What
does that mean. Well every network stack
has received so the Kernel has a receive
buffer for each TCP connection and that
buffer is size limited to avoid Kernel
memory exhaustion which means that
whenever the application so the web server
or the web browser is reading data some
buffer spaces are reclaimed and when TCP
segments are arriving. Some of that buffer
is consumed. It's a sliding window and we
have seen in the TCP header is is a
windows size so there is a 16 bit field
called window size which specifies how
many more bytes my TCP Stack has for
receiving data from the other side to
avoid deadlocks there is also a timer in a
timer called the persist timer which is
started when the window is when the window
size is zero and that then at a time out
try retransmits TCP segment in order to
get information about the new window size
from the other side. Congestion control
I will also skip a bit but the main idea is
to control the rate of data entering the
network because if you're using multiple
routers at some point you may saturate
some of the network links and that is
avoided in TCP by doing by applying
congestion control which measures for
example the time between segments sent and
acknowledgement received also has to do
with a slow start and how your window size
your window buffer grows.
Acknowledgments. Well there are some
strategys the basic one is every segment
is acknowledged individually there's
delayed ACK where you collect multiple
segments to acknowledge them at a certain
time then you have also selective
acknowledgements where you can acknowledge
discontinuous segments which helps for
lowering the amount of retransmissions. TCP
also carries some maximum segment size to
avoid fragmentation. Actually on the IP
layer because to this partially open
there's some struggle because you have
simultaneous open so what if both parties
want to open a connection at the very same
time. Then you have a flag which is called
the reset in order to terminate a
connection. There are some extensions like
Window scaling and fast open to improve
the throughput and also to lower the
delay. There are some attacks like denial
of service. So if your server
implementation accepts something and
allocates a lot of memory for a client
which doesn't do a lot but just sending a
SYN frame that is bad and leads to denial
of service connection hijacking if you can
predict the sequence numbers then you can
hijack and emit data into an established
connection. There have been some blind in-
window attacks. What does that mean that
even without knowing the sequence number
you can do something on an established TCP
connection such as, yeah sending a reset
or sending a FIN frame and tearing that
connection down. The specification for TCP
is written in English prose in a
collection of RFC and there are some
widely deployed implementations. During
some research work in Cambridge over the
last years me and various colleagues
implemented a formal model developed in
the interactive theorem prover HOL4, which
has a precise specification with
implementation looseness and we really use
that as an input so the sockets API and
interface for getting the TCP control
block, which is the host internal state of
the TCP and then the wire interface which
is data received and sent on that. And we
use that formal model to validate itself,
so we used actual implementations to do
that, we use it to draw some diagrams
where you can see the rules which fires on
the left hand side, when something
happened like there was a CONNECT called
and then the logical rule connect_1 was
used in the label transition system. Then
we see here as well some TCP segments
which are going out and then what are the
contributions of the network semantics, we
checked the model, we validated the model
by recording traces and executing them. We
published a paper called Engineering with
Logic: Rigorous Test-Oracle Specification
and Validation for TCP/IP and the unix
Sockets API. The specification itself is
typeset in 384 pages, that's all the
transitions you basically need. So roughly
10000 lines of HOL4 code and a lot of
comments, where we embedded a lot of
LaTex code. And the Unix TCP/IP stack has
usually around 15000 lines of code, the
TCP state machine we saw earlier, is here
in this paragraph, in this diagram and we
try to draw a more correct TCP state
machine which led us to this picture,
which is a bit more complicated. We have
this state NONEXIST up here and we have
much more transitions due to timers and so
on. So the state machine used in common
literature is actually not complete or not
precise and we have a revision for that.
The conclusion is you have all TCP/IP
widely deployed. I hope I managed to give
you some insight how TCP/IP actually
works. It's a layered architecture which
is agnostic of underlying layers and in
the network semantics working, we had an
executable specification. That's all I
have to say and I welcome you to ask any
questions, either now or offline.
Applause
Applause
Herald-Angel: Thank you. So, if you have
any questions just go to the microphones.
We have two here and two on the right
side. And do we have some question from
the Internet? No questions? No questions?
Yeah, 1 question, come on, don't be shy.
Microphone 1: Right. Hi thanks, that was a
very interesting talk. So your model, does
it allow synthesizing a implementation
from the specification, or is it used
mostly for validating?
HM: It's at the moment used for validation
because we have the specification
looseness. So we have an implementation
looseness. So at some point in implementation
you have to choose whether you take one
transition or the other one. So if you go
into a failure state or if you go into a
success or if you transmit some piece of
data and go into a success state. So we
don't have synthesized any implementation
but there is ongoing work to use it as the
implementation, as a base for an
implementation.
Mic: Okay. And do you think that such an
implementation can be made, can it be made
efficient as well, once synthesized?
HM: Yes.
Mic 1: Okay, thanks.
Applause
Herald-Angel: Yeah, your question please.
Microphone 2: Yeah, thank you. How
independent is TCP from IP? I mean, can
you integrate TCP over different protocols
like Bluetooth or something like that?
HM: Sighs
Since TCP requires for error messages, a
bit of ICMP, I haven't seen any TCP
implementation on top of any other medium
than IP.
Mic 2: Okay.
HM: So, I don't know, but I can think of
it. Could work.
Herald-Angel: Okay, your question please.
Microphone 3: Thank you. Hello. So you
used HOL4 for the specification part. Did
you actually need the higher order logic
part of HOL, or would it be possible to
just use predicate logics?
HM: Sighs
I, I will have to reread. I think we need
actually some higher order logic for it,
for the whole state and the transitions.
Mic 3: It would be interesting to meet
and...
HM: Yes, well, the paper has been
published at the journal of ACM and
luckily scihub.is is available and you can
download it for free from there.
Laughs
Mic 3: Okay, thanks.
Herald-Angel: Any more questions? No?
Then, thank you Hannes. A warm applause
for Hannes please.
Applause
postroll music
subtitles created by c3subtitles.de
in the year 2018. Join, and help us!