% !TeX root = Fenrir.tex

\part{Implementation}[salt_time.png][I promise!]


\chapter{Implementation choices}

\lettrine{T}{his} doesn't want to be a full-featured RFC, but it will help in understanding why and how a lot of things that are not present on the previous formal
model are tied to it and why the addition of new data still conforms to the formal model.

The formal model only checks for security leaks, but it does nothing to test against amplification attacks. We will further discuss this treat and the precautions
that Fenrir adopts to avoid this problem.\\ As we can not model all the real-world data structures in proverif (the complexity would explode and there are no
ways to model some data), we will have to explain how and why we can distinguish packets, sessions and user data.

\section{Connections}

The first thing that we find in a packet is the connection id. The obvious use of this is to identify the different connections, but there are more uses
that this field can have.

The most important one is the handshake. We can not grant a connection id every time we receive an handshake packet, or we would expose ourselves
to DoS. All handshakes must be handled by a single connection id, which will be the id 0.

The rest of the packet will be a stream with random id that will contain the handshake data. The stream identifier and counter will act as a tcp sequence number,
providing us with the necessary tracking information so that both client and server can distinguish different connections and fragmented packets.

As per the TCP sequence number, we will use the counter to make sure that the client is not spoofing somebody else's ip address. This assurance is
not complete, as the attacker might be snffing the victim traffic or might be the next op in the server traffic, but it still avoids lots of easier spoofing attacks.

In the future (see \ref{future}) this field might sustain more restrictions to include caching proxies and multicast delivery.

\subsection{Connection id allocation}

Each client should have the full $2^{32}$ connection space available, and we should not try to spend time synchronizing on which connection id
is available between the server and client, as that would require too many round trips and/or data transfer to be feasible.

The obvious choice is that both the client and server will choose one connection id, and will communicate the choice to the other party. The sender will then
use the connection id the receiver requested.\\
Each party now has the full connection space at his disposal, and there are no clashes or synchronization mechanisms.



\section{Streams}

The stream section can be repeated multiple times in the packet to achieve parallel delivery of multiple streams. The concept is very similar to switching
from a virtual circuit network to a packet switched one.

Each stream is identified by a \textbf{16 bit} id, which should leave plenty of space to handle all different network flows that a single program needs.\\
Fenrir itself uses one of this streams to carry connection information, ACKs and so on, but it can use multiple streams to implement features like
forward error correction.

Each stream identifier must be random. By doing so we will increase the entropy of the encrypted data and make chosen plaintext or known-plaintext attacks
impossible or at least more difficult. Then in the future we might be able to apply compression techniques to the whole packet with less worry of
attacks like CRIME or BREACH.

\subsection{Flags}

The 1-byte stream flags field could have been used for multiple things. Experiments included padding and tracking of features like forward error corrections
and/or type of stream.

Eventually it was clear that 2 bits had to be allocated to signal the beginning and end of the user message, as that lets us break away from the raw-bytestream
model used in TCP that forced the users to meddle with message boundaries, lengths of escape sequences. Introducing this leads to a big
simplification of the management of user messages for any type of stream.

There were experiments with additional message counters, padding and tracking of stream features, but all these could be derived from other fields or
did not change quickly enough to need dedicated space in every packet. This meant that the original 1-byte bitfield for flag was reduced down to only
2 bits.\\
The next 5 bits were used to increase the maximum transferable unit in the fenrir streams, to bring the counter up to 1GB. The rationale for this is in the
next section.

\subsection{Stream counter}
\label{stream counter}

The stream counter works like the tcp sequence number, and also limits the maximum window size. TCP had a segment size of 32 bits, but a window size of 16
bits: this was proved to be inefficient in high-bandwidth, high-delay connections, for example when using satellite links. To solve this problem extensions to the
tcp header have been introduced to increase the receiving window.

The well known \textbf{bandwidth-delay product}\index{Bandwidth-Delay product} ($B*D = bytes$) tells us how much unacknowledged data can be in transit at
any given time. TCP had a maximum window size of $2^{16}$ bits, which meant that on a satellite link with a 200ms RTT we could only transfer up to 320KB/s,
or 116KB/s on a link with 550ms delay. Due to this problem a ``window scale'' option was created, were a shift (up to 14 times) could be applied to the receive
 window, bringing the maximum window size up to almost $2^{30}$. This brings the total maximum bandwidth of TCP to 1.8GB/s.

In Fenrir the receiving window is handling is done inside the control stream, so there is no need for an ad-hoc field in each stream. Fenrir also has multiple
streams, but handling the congestion window and the receiving window is slightly more complicated as multiple interfaces and streams are involved in a
single connection.

Initially the counter was set to only 3 bytes (tracking $2^{24}$ bytes). The counter can obviously overflow without having to destroy the stream, but $2^{24}$
bytes can be considered a limit for the receiving/congestion window, thus it was decided to use the last 5 bits on the stream flags to bring the maximum stream
counter to $2^{30}$ bytes. By the previous bandwidth delay product, this means we can transfer data with up to 5GB/s on the 200ms-delayed link.

Geostationary satellites have a physical limit of at least 550ms of latency, which means that we will be limited to 1.8GB/s
(slightly more than TCP in the same case).\\
The latest satellites have a total bandwidth of about 140Gbit/s, or about 17.8GB/s, which are only 10 Fenrir streams at full speed.

But this is \textit{not} the real limit of a Fenrir connection, because we are still looking at the theoretical maximum for a single stream. Fenrir leaves the user
with up to $2^{16}-1$ different streams, for a \textit{total of more than 116TB/s}. This will also mean that the congestion window for the whole connection
now needs to be of at least $30+16=46$ bits, so that we can scale up to the maximum theoretical speed. The receiving window will be set per-stream and
will thus remain at 30 bits.

\section{Handshake}

Security and performance are often opposites. While developing the handshake, it became clear that a tradeoff was necessary in terms of performance
and security. Most users will only care about performance, but developers and administrators might care more about security, especially for applications
that require reliability. For this reason Fenrir has multiple handshakes, designed either for speed of security.

The three handshakes for Fenrir are the Full-security, the stateful handshake and the directory-synchronized handshake.

Before looking at the details, let's look at some generic choices:

\subsection{0-RTT protocols}

While we might have incorporated 0-RTT connections, like QUIC, minimaLT and the newer TLS1.3, a brief analysis revealed that any implementation of this
features is a big problem for security and developer usability. The problem was big enough to actively avoid any kind of 0-RTT handshake.

To easier understand why a 0-RTT protocol is a bad idea no matter the implementation, let's start analyzing what 0-RTT means: 0-RTT means that we will need
to keep a state, as (at least) keys and ciphers must be agreed upon. The state can become bigger when we consider session resumption, so how long
will we keep a state? Keeping this state breaks any guarantee of perfect forward secrecy, and if kept too much leaves us open to memory DoSes.

MinimaLT provides a 0-RTT connection, but technically does not implement perfect forward secrecy. All clients use the same server key, until such key is replaced
in the directory service(DNS).

How do we distinguish a legitimate connection from a replay attack? The server can only use the state until the first successful 0-RTT connection, and if the
client loses connection before asking new shared keys and data, it can't be used again, or replay attacks become possible.

Fenrir detaches itself from the IP layer, so that is can use multiple connections and ips without problems. But if we can connect without even one RTT, what
guarantees us that the client didn't spoof the ip address while requesting a big file? This alone can create amplification attacks of an unseen magnitude.
The only reason TLS can get away with this is that the IP confirmation is provided by the 2-RTT TCP handshake, but DTLS servers might suffer from it when
the dtls specification get updated.\\


In short, safe 0-RTT connections can not be used for the first connection, can only come from the previous ip address(es),
can only be used once (then must be renegotiated), and break the perfect forward secrecy model.\\
This features are nearer to a session resumption than to a new connection setup.


For these reasons new 0-RTT connections will not be allowed in Fenrir, and 1-RTT is the minimum by design.

\subsection{Session resumption}

TLS and other protocols have to provide cookies, shared secrets or signed data to implement session resumption. It is not easy to decide what has to
be used to represent the client-server connection, and thus attacks like 3shake\cite{3Shake} were born.

In the case of the 3Shake attack, the problem was that most of the information that identified a client was taken from freely modifiable fields in the lower
layer protocols. As such, an attacker could impersonate any client and steal a user session.

In Fenrir we are completely detached from the lower layers, so there is no need for cookies or signed data to be transmitted. If the server simply keeps
a long time to live for each connection, the connection id is enough to resume the connection from any IP. Much simpler and straightforward.

\subsection{Protocol version and protection}

Protocols can advance, new versions can be developed, and old version will be deprecated. This is normal, and even SSL and TLS have a field
dedicated to version tracking.\\
What has never been tracked however was the \textit{complete list} of the supported versions. And this lead to downgrade attacks in the SSL/TLS protocols.

During the handshake both the client and server list the supported ciphers. The whole list is then used when signing the data, so that both client and
server know that the received list is the correct one, and has not been tampered with. But for some reason, this concept was not applied to protocol versions.

So during the SSL-TLS transition, an attacker could drop the TLS handshake and force a timeout, thus making the client try older (and bugged) SSL version.\\
The solution today is to simply disable the whole SSL protocol, but this is still a poor way of handling a transition, and does not protect anyone during
the actual transition.

To avoid these problems Fenrir will list and sign all supported protocols and handshakes, making sure that the whole protocol can be upgraded in the
future, without dangerous transitional periods.

\chapter{Bits on the Wire}

\lettrine{T}{he} full packet is listed here:


\rowcolors{1}{green}{green}
\begin{tabularx}{0.7\textwidth}{| l || X | X | X | X |}
\hline \hline
\hiderowcolors bytes &0&1&2&3\\ \hline \hline
  0-3 & \multicolumn{4}{c|}{Connection id} \\ \hline
  & \multicolumn{4}{c|}{Encryption Header} \\ \hline
\showrowcolors  4-7 & \multicolumn{2}{c|}{Stream id} & \multicolumn{2}{c|}{Data length} \\ \hline
  8-11 & flags & \multicolumn{3}{c|}{Stream counter} \\ \hline
\hiderowcolors    & \multicolumn{4}{c|}{Authentication header} \\ \hline \hline
\end{tabularx}
\begin{center}
The packet so far. Green color highlights the encrypted data
\end{center}

