-
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!