2_background.tex

\chapter{Background}
\label{chap:background}

In this chapter, we introduce the reader to the concepts that are necessary to understand the rest of this thesis.
We start by introducing how code verification works with a particular focus on the Gobra~\cite{wolf2021gobra} verifier.
Then, we present existing work on the verification of protocol implementations, which will form the foundation of our work.
Finally, we explain two important cryptographic concepts that will be used in the protocols that we aim to verify.

\section{The Gobra verifier}
\label{sec:the-gobra-verifier}

Gobra~\cite{wolf2021gobra} is a verifier for programs written in the Go programming language.
In practice, a user writes a specification of the program, and Gobra verifies that every execution of the program satisfies this specification.
Gobra is based on the Viper~\cite{muller2016viper} verification infrastructure. This means that the Gobra specification and Go implementation are translated to the Viper intermediate language, which is then verified using one of the Viper backends.

In this section, we first provide the reader with a brief introduction to the modular verification of Go programs using Gobra.
We then introduce fractional permissions, which are used to reason about heap memory accesses and in particular allow concurrent read operations.

\subsection{Verifying a Go program}
\label{sec:verifying-a-go-program}
% - Modularity of the verification, Hoare logic, pre/postconditions
% - Predicates

The first step in the verification of a Go program is to write a specification of the program, describing its intended behavior.
To do so, the user writes verification \emph{annotations} for each function of their Go implementation.
These annotations do not interfere with the execution of the program and are only used for verification purposes.

The main types of annotations are \emph{preconditions}, \emph{postconditions}, \emph{lemmas} and \emph{loop invariants}.
Preconditions and postconditions are used to specify the behavior of functions. Preconditions specify the requirements that must be met before a function is called, and postconditions specify the guarantees that the function provides when it returns.
The verification of the function is successful when Gobra can prove that the postcondition holds whenever the precondition holds.
Lemmas are ghost functions, meaning that they are only used for specification purposes and are not part of the implementation.
They are used to express and prove auxiliary properties of the program's specification and can be called in other verification annotations to help Gobra prove more complex properties.
Loop invariants are assertions that must hold at the beginning and the end of each iteration of a loop, and are used to specify the behavior of loops.
An example of a function with some verification annotations is shown in Figure~\ref{lst:multiply-example}.

\begin{figure}
    \begin{gobra}
requires a >= 0 && b >= 0
ensures  product == a * b
func multiply(a, b int) (product int) {
    product = a * b
    assert product == 0 ==> (a == 0 || b == 0)
}
    \end{gobra}
    \caption{This function returns the product of two positive integers. On line 1, “\texttt{requires}” specifies the precondition. Here, we specify for this particular example that \texttt{multiply} may only be called with positive arguments. On line 2, “\texttt{ensures}” specifies the postcondition. Here, the postcondition states that the product is equal to the product of the two arguments. On line 5, we use an “\texttt{assert}” statement to prove that one of the parameters must be zero if the product is zero. In this case, the assertion is not necessary for the verification of the function and is only given as an example.}
    \label{lst:multiply-example}
\end{figure}

Preconditions and postconditions enable a modular verification of the program, i.e.\ we verify functions in isolation and only consider the specification of the functions that they call, not their bodies.
Doing so, we verify only once the correctness of a function.
% Then, when this function is called by other functions, we simply assume that it satisfies its specification.
This greatly improves performance, as it decomposes the verification of a program into the verification of each component.

\subsection{Permissions}
\label{sec:permissions}
% - The fractional permission system must have been introduced in the Background chapter

Gobra supports verifying programs that manipulate heap memory.
Gobra reasons about potential side-effects or their absence using \emph{separation logic}, an extension of Hoare logic. 
In particular, a permission is associated with every heap location and a heap access induces a proof obligation that the current function has the necessary permission.
A permission is created when allocating a heap location.
Permissions allow us to deduce whether a callee might modify a heap location or not, because the callee may only modify a heap location if it has permission to do so.
To specify which heap locations are accessible to a function and with which permissions, we use an accessibility predicate, denoted \texttt{acc}.

% To do so, it requires a way to specify which heap locations should be accessible to a function.
% Otherwise, if we wanted to guarantee that a function did not modify the heap, we would have to write a postcondition iterating over all heap locations and stating that they are not modified, which would not be efficient.
% Therefore, Gobra uses \emph{separation logic} to reason about heap memory.

By default, a function has no permission to access heap locations.
To give a function permission to access some location, we specify the corresponding permission in the preconditions.
A permission of $1$ to a heap location gives full permission, allowing the function to read and write to the location, and a permission of $0$ gives no permission.
Gobra uses fractional permissions, which defines a permission as a rational number between $0$ and $1$.
Any strictly positive permission smaller than one only gives read permission to the heap location.
There can only be a total permission amount of $1$ for each heap location, which enforces that there can be either only a single writer at a time or multiple readers.
To illustrate how we can use permissions in Gobra, we show in Figure~\ref{lst:multiply-example-heap} the same example as in Figure~\ref{lst:multiply-example}, but this time \texttt{a} and \texttt{b} are pointers to heap locations.

\begin{figure}
    \begin{gobra}
requires acc(a, 1/2) && acc(b, 1/2)
requires *a >= 0 && *b >= 0
ensures  acc(a, 1/2) && acc(b, 1/2)
ensures  product == *a * *b
func multiply(a, b *int) (product int) {
    product = *a * *b
    assert product == 0 ==> (*a == 0 || *b == 0)
}
    \end{gobra}
    \caption{This function returns the product of two positive integers. This is the same example as in Figure~\ref{lst:multiply-example}, but this time reading \texttt{a} and \texttt{b} from heap locations. \texttt{acc(a, 1/2)} specifies permission of $1/2$ to the heap location \texttt{a}. Notice that we require read permissions (line 1), which we can return at the end of the function (line 3). Removing line 1 would result in a verification error.}
    \label{lst:multiply-example-heap}
\end{figure}

Another construct supported by Gobra that will be useful in this thesis is the \emph{predicate}.
A predicate is a parametrized assertion to which we give a name.
It is defined with the keyword \texttt{pred}. 
In particular, a predicate can be used to abstract over individual permissions.
For example, we could create a predicate to express permission to access an array of bytes instead of specifying the permission to each byte individually.
A predicate that does not contain an assertion is called an \emph{abstract} predicate. We will see later how they can be useful.

\section{Verification of protocol implementations}
\label{sec:verification-of-protocol-implementations}

Verifying a protocol implementation requires more work than verifying the correctness of a simple Go program.
Indeed, a protocol describes a distributed system where each participant is implemented in a separate program.
We can verify each participant individually, but we would like to express and prove protocol-level global properties that require the collaboration of all participant implementations.
% Additionally, our goal of verifying security properties requires us to introduce sufficient verification specifications to be able to express these properties.

In this section, we introduce the notion of symbolic protocol analysis to present how protocols are usually modeled when verifying their security properties.
Next, we discuss the security properties that we aim to verify.
We then present two existing approaches aiming at verifying protocol \emph{implementations}. These approaches are the main basis for our work.

\subsection{Symbolic protocol analysis}
\label{sec:symbolic-protocol-analysis}
% - The trace invariant (but not the message invariant)

In symbolic protocol analysis, we analyze a protocol at a higher level of abstraction to verify its behavior in all possible executions.
We use the symbolic model of cryptography, where we assume that the cryptographic primitives are secure, i.e.\ the plaintext can only be obtained from a ciphertext if decryption is performed with the correct decryption key.
Additionally, we assume that all operations are performed on symbolic \emph{terms} instead of bytes.%, which is why we abstract concrete bit-strings to terms.

Furthermore, we consider a Dolev-Yao~\cite{dolev1983security} attacker present in the network. This attacker can perform arbitrary operations on this term level, has full control over the network (including reading and sending any message), and can corrupt any participant (which means that the attacker learns all the terms contained in a participant's state).

A common way for reasoning about protocols in this setting is to consider all possible \emph{traces} of a protocol.
A trace records the sequence of protocol events in a particular run of the protocol.
Security properties can be expressed as a logical expression about a trace, and then verified by checking whether it holds for all possible traces of the protocol.
Automated provers like Tamarin~\cite{meier2013tamarin} and ProVerif~\cite{blanchet2016modeling} can verify trace-based security properties by analyzing all possible traces.

In this work, we aim to verify security properties for protocol \emph{implementations}.
While verifying protocol \emph{models} is useful to prove the security of the protocol design, it does not guarantee that an implementation of this protocol is free of security vulnerabilities induced by common programming errors or the incorrect implementation of the protocol design.
When considering the verification of protocol implementations, traces can also be used.
By expressing an invariant over the trace and proving that this invariant is maintained by all executions, we obtain properties that hold for all possible traces. 
We call this invariant the \emph{trace invariant}.
Then, we verify security properties by showing that these security properties are implied by the trace invariant.
% The overall idea is to extend the implementation with a ghost trace to record protocol operations. In order to reason about the whole protocol (and not a single execution), we define a \emph{trace invariant}. It is a property that every prefix of any trace of the protocol must satisfy.
% Verifying the protocol implementation ultimately consists of proving that each action of a participant or the attacker maintains the trace invariant, and then proving that the invariant implies the intended security properties.
We detail the security properties that we aim to verify in the next paragraph.

\subsection{Security properties}
\label{sec:security-properties-def}
% - Forward secrecy and post-compromise security (via state) must have been introduced before

We have mentioned that using a trace and maintaining a trace invariant allows us to prove some security properties.
In particular, we want to prove forward secrecy and post-compromise security for certain protocols. In this subsection, we explain what these properties are and why they are important.

Forward secrecy is a security property expressing how past communications are protected from a future compromise.
A protocol is forward-secure if compromising the current state of a participant does not reveal past communications, meaning that the attacker cannot decrypt previous messages.
However, forward secrecy does not protect future communication. The attacker could use the compromised knowledge to impersonate a legitimate participant and read all future communications.
This is why we are interested in the next property, post-compromise security.

Post-compromise security is a security property expressing how future communications are protected from a past compromise.
First, notice that post-compromise security is not achievable after the \emph{unrestricted} compromise of a participant.
After such a compromise, other participants have no guarantee whether they are communicating with the compromised participant or the attacker because the attacker has access to the same secrets as the compromised participant and can thus impersonate this participant.
We instead consider the formalized notion of post-compromise \emph{via state}~\cite{7536374}:
a participant can communicate securely with a peer even when a past state of the participant is revealed to the attacker, as long as the participant's current state is not revealed to the attacker and some secret data remains available exclusively to the participants.
If the participant's current state is revealed to the attacker, post-compromise security via state trivially holds but we get no guarantee of the security of future communications.
% during a session even when long-term keys have been leaked as long as there is some secret data available exclusively to the participants.
% Some secret data remains available to the participant by considering the scenario that a past state is revealed to the attacker but not the current one. If the current one is revealed, then there is no hope (and thus post-compromise security holds trivially in that particular case).
To be able to prove this property, we must be able to prove that a certain state in the past, to which an attacker has gained access, does not contain the secret data on which future communication depends.

In the following, we will introduce two existing approaches in this verification setting aiming at verifying strong security properties for protocol \emph{implementations}. These approaches are the main basis for our work.

\subsection{DY*}
\label{sec:dy-star}
% - Versions must have been introduced in the DY* chapter of the Background
% - Explain our notation for secrecy labels [(p,s,v), (p',s',v')]
% - CanFlow should be introduced in the background
% - Snapshots

DY*~\cite{bhargavan2021text} is a framework for proving security properties about protocol implementations written in the F* programming language.
Using a particular code structure and a particular way of storing program state, DY* is able to account for some implementation-level specificities.

While DY* uses a trace to record protocol events, it is not \emph{ghost}, i.e.\ the trace is not only used for verification purposes.
In particular, each participant's state is stored in a serialized way on the trace.
% DY* uses a \emph{global trace} to model the global execution state of the protocol.
When a protocol participant is taking a protocol step, it first reads its serialized state from the trace, deserializes it, performs the step, and then saves its new serialized state to the trace.
This means that only protocols with this particular way of storing program state can be verified with DY*.
% Note that because the global trace is storing program state, it is part of the protocol implementation and not only a verification artifact: we say that it is a \emph{non-ghost} data structure.
This also affects the runtime behavior of the protocol, as the trace must exist and be used to store and retrieve the program state.

This trace is append-only and existing entries cannot be modified or deleted. In addition to state changes, the trace records all operations that are important for proving security properties (nonce generation, sent messages, and corruption).
% The attacker can perform these operations at any time as well.
Ultimately, this global trace contains each participant's current and all past states, and provides a global view over the entire distributed system. % such that global properties can be expressed and proven.
DY* achieves modular reasoning by specifying a trace invariant and verifying that each function modifies the global trace only in ways that maintain the trace invariant. Global security properties can then be proved from this trace invariant.

On the global trace, each state is annotated with a \emph{session state identifier} to indicate to which participant and protocol session it belongs. This models the fact that a participant may be involved in multiple independent protocol sessions simultaneously. The session state identifier includes a \emph{version} that distinguishes between different phases within a protocol session (further explanations about versions will be given in section \ref*{sec:versions}).
%, as explained in detail in section \ref*{sec:existing-approach-dy}. 
Each participant's state comprises several values that together constitute the program state of the participant.
By value, we mean here and in the rest of this thesis a piece of data that is stored on the heap.
Each of these values is assigned a \emph{secrecy label}, indicating which participant is allowed to read a value and at what times.
These secrecy labels enable modular reasoning about secrecy because a secrecy label provides an over-approximation of which participant states might contain a particular value.
% In DY*, if an attacker corrupts a participant or one of its sessions (possibly with a specific version), they will obtain all values having the corrupted session state identifier as a secrecy label.
A value can be made accessible to a participant $p$, to only some specific session $s$ of a participant, or even to some specific version $v$ of a session.
A secrecy label is most often defined as a list of everyone who can access the value\footnote{A secrecy label can also be defined by the union or the intersection of participant, session and version identifiers, which we omit for brevity.}. For example, a value with a secrecy label $[(\text{Alice}), (\text{Bob}, 3), (\text{Charlie}, 2, 7)]$ can be accessed by Alice at any time, by Bob in session 3, and by Charlie when his second session is in version 7. We will keep this notation of secrecy labels throughout this thesis.
Additionally, the secrecy label of a value can also be \emph{Public}, which means that the value is accessible to everyone, including the attacker.

The version label attributed to each session is used to introduce a notion of temporality. Initially, all session versions are 0 and are incremented at some times to represent new protocol phases.
A value with a secrecy label $[(p,s,v)]$ can only occur in the specific phase of the protocol when the session $s$ of participant $p$ has version $v$.
DY* enforces this restriction with a suitable invariant over states, which they enforce whenever state is stored on the trace. Thus, only data from the current version can be stored, ensuring that neither outdated keys nor future keys are present in memory.
Hence, these versions are used to define the period of existence of values.
Building on this, they are able to prove forward secrecy and post-compromise security for protocols like Signal.

A hierarchy between secrecy labels is necessary to express some properties. For this, DY* introduces a \texttt{CanFlow(l1,l2)} relation specifying that a less restrictive secrecy label \texttt{l1} can flow to a more restrictive secrecy label \texttt{l2}.
For example, the label $[(\text{Alice}), (\text{Bob})]$ can flow to the more specific $[(\text{Alice})]$. And the label $[(\text{Alice})]$ can flow to a single session $[(\text{Alice}, 3)]$.
In particular, DY*'s state invariant expressing that a value should be readable in the current context can be specified using the \texttt{CanFlow} relation: the value's label should flow to the current participant, session and version.

Protocol implementations written in F* and verified with DY* are executable but require a special runtime environment that provides access to the trace such that a participant's state can be stored and retrieved.
Additionally, the DY* framework is composed of a library, containing protocol-independent parts that only need to be verified once, and can then be reused across different protocols. This significantly reduces the overall verification time.

\subsection{Modular verification of existing implementations}
\label{sec:modular-verification-of-existing-implementations}
% - The Mem predicate must have been introduced in the Background chapter
% - It does not support versions, which limits the protocols and properties that this approach can verify

% The DY* framework is limited to verifying protocol implementations written in the functional F* language and makes several assumptions on how implementations are structured and how program state is stored.
The DY* framework can only verify protocol implementations written in the functional F* language that adhere to certain assumptions about their structure and program state storage.
% However, there are many existing protocol implementations written in various languages that cannot be verified with this approach.
However, these assumptions do not hold in general for existing implementations.
Arquint et al.~\cite{ArquintSchwerhoffMehtaMueller23} present a methodology for verifying existing heap-manipulating protocol implementations. This methodology is agnostic to the programming language and relies only on standard features present in most separation logic-based verifiers. In the following, we will focus on Go implementations and the Gobra~\cite{wolf2021gobra} verifier.

This methodology is inspired by DY*~\cite{bhargavan2021text} and also uses a global trace to provide a global view of the entire system.
% Arbitrary code structure
To address the issue of arbitrary code structure in existing implementations, the trace is treated as a concurrent data structure.
This treatment ensures that all possible interleaving of events are considered, without relying on any code structure assumptions.
% It allows arbitrary interleavings of operations, in a more fine-grained manner than arbitrary interleavings of protocol steps in DY*, which is crucial for soundness in this setting.
% Program state management
As existing implementations manage the program state in their unique ways, we cannot assume that they store the state on the trace or rewrite implementations to do so. Instead, \emph{local invariants} are used to relate the program state stored at a participant to events on the trace.
% Snapshot
Because the global trace is a shared structure, each participant maintains its own local \emph{snapshot}, which is a local copy of the global trace. Since the global trace can only grow, a snapshot is a prefix of the global trace. 
The global trace only records a sequence of events corresponding to high-level operations (similar to DY*, except for the state storage entry) that must maintain a trace invariant, which is used to prove global security properties.
% Ghost
Unlike DY*, the global trace is a \emph{ghost} data structure for verification-only purposes, which will be erased before compilation. As such, the global trace has no impact on the runtime behavior or performance.

Furthermore, separation logic's resources are used to prove injective agreement, which is to the best of our knowledge not possible with DY*.
To do so, they use that separation logic's resources are not duplicable, so if an assertion includes two resources, they are distinct.
This can be used to express the uniqueness of an event and prove that an implementation detects when an attacker replays messages, which is necessary to satisfy injective agreement.
Because DY*'s invariant is expressed in first-order logic, it is unclear how they could reason about the uniqueness of particular events.

Similarly to DY*, this methodology comes with a library, called the Reusable Verification Library, which allows the reuse of protocol-independent parts (verified only once) across different protocol implementations.
Because they are using Gobra, verification is based on separation logic, which allows us to reason about heap manipulations.
Currently, any creation of an array of bytes (i.e.\ creation of nonce, keys, etc.) is controlled by a memory predicate \texttt{Mem}.
The \texttt{Mem} predicate is used to abstract over the memory of a byte array and thus specifies permissions to every byte in the array.
The predicate body is shown below, for illustration purposes only\footnote{The \texttt{Mem} predicate is in fact abstract in the library, meaning that clients of the reusable verification library cannot get direct access to the individual bytes of the array and instead have to perform all operations via corresponding library calls.}:
\begin{gobra}
pred Mem(s []byte) {
    forall i int :: 0 <= i && i < len(s) ==> acc(&s[i])
}
\end{gobra}
Permission to this predicate is then required by all library functions performing operations on the associated byte array.

Each created value is also assigned a secrecy label, like in DY*, to specify allowed readers.
However, this methodology does not support versions in secrecy labels.
Without this fine-grained temporality, it is not possible to prove forward secrecy and post-compromise security for protocols like Signal.

\section{Cryptography}
In this section, we explain two important cryptographic concepts: AEAD encryption~\cite{10.1145/586110.586125} and Diffie-Hellman key exchange~\cite{diffie2022new}.
These notions will play a major role in the rest of this thesis. 
However, the discerning reader can skip this section if he or she is already familiar with these basics.

\subsection{AEAD encryption}
% - What associated data is 
In the protocols that we aim to verify and that we will present later, authenticated encryption with associated data (AEAD)~\cite{10.1145/586110.586125} plays an important role in the communication between participants.
AEAD is a symmetric encryption scheme.
It provides confidentiality, meaning the encrypted message cannot be read by an attacker who does not know the key.
It also provides authenticity, meaning that an active attacker cannot modify the encrypted message or associated data without being detected and that the receiver can verify that the message was sent by the expected sender.

AEAD encryption takes as input a key, a plaintext, and optionally some associated data, and returns a ciphertext.
While the message is sent encrypted and authenticated, the purpose of the associated data is to send in clear some data that is not confidential but that is authenticated.
For example, we will in the following use the associated data to send public keys in an authenticated way.
Then on the receiver side, AEAD decryption takes as input the same key, the ciphertext, the received associated data, and returns the plaintext if decryption succeeds.

\subsection{Diffie-Hellman key exchange}
% - What a DH key exchange is

A Diffie-Hellman key exchange~\cite{diffie2022new} is a public-key protocol that allows two participants to agree on a shared secret key over an insecure channel.
Each participant $p$ has a secret key $s_p$ and a public key $g^{s_p}$, where $g$ is a primitive root modulo a prime number\footnote{
    In the following, we will not mention the modulo prime number for brevity.
}.
In a Diffie-Hellman key exchange, participants Alice and Bob first exchange their public keys $g^{s_{Alice}}$ and $g^{s_{Bob}}$ over the insecure channel.
Then, Alice computes a shared secret key $(g^{s_{Bob}})^{s_{Alice}} = g^{s_{Alice} \cdot s_{Bob}}$ by combining her secret key and Bob's public key, and Bob computes the same shared secret key $(g^{s_{Alice}})^{s_{Bob}} = g^{s_{Alice} \cdot s_{Bob}}$ by combining his secret key and Alice's public key.

This key exchange will be extensively used in the protocols that we aim to verify and that we will present later.