3_design.tex

% TODO_ The following notions must have been introduced before:
% - What a DH key exchange is
% - CanFlow should be introduced in the background
% - Forward secrecy and post-compromise security (via state) must have been introduced before
% - Versions must have been introduced in the DY* chapter of the Background
% - The fractional permission system must have been introduced in the Background chapter
% - The Mem predicate must have been introduced in the Background chapter
% - Explain our notation for secrecy labels [(p,s,v), (p',s',v')]

\chapter{Design}
\label{chap:design}

In this chapter, we explain how we extended the work of Arquint et al.~\cite{ArquintSchwerhoffMehtaMueller23}, presented in section~\ref{sec:modular-verification-of-existing-implementations}, to express time-sensitive values and to enforce their deletion at the right time.
Practically, we extended their Reusable Verification Library in order to provide someone verifying a protocol implementation with the possibility of proving security properties like forward secrecy and post-compromise security.
In the following sections, we will refer to this person as \emph{the developer}, who uses this library to verify a protocol implementation.

We start by giving an overview of our goal and a high-level idea of our methodology to achieve it.
Then, we introduce counting permissions, as the core tool on which our deletion mechanism is based.
We continue by explaining how we extended the library to implement our deletion mechanism.
Finally, we give a brief look into an alternative approach that would have been simpler, but that is not currently supported by Gobra~\cite{wolf2021gobra}.

\section{Overview}
\label{sec:overview}

This section gives an overview to better understand our goal and the high-level idea of our methodology to achieve it.
With the aim of verifying properties like forward secrecy and post-compromise security for a protocol implementation, we need to model the fact that some ephemeral values should only exist for a limited amount of time.
Additionally, we need to enforce that these values are deleted before the end of their time frame.

We start by explaining the goal of our methodology by introducing a relevant protocol, the Diffie-Hellman Ratchet~\cite{perrin2016double}, and the security properties we want to prove about it.
Then, we explain how we introduce a notion of temporality in the methodology, by adding  \emph{versions}, which define fine-grained time frames during which certain values are present in memory.
Finally, because versions specify that a value should only be able to exist in some time frame, we reason about how to enforce that it is deleted before this time frame ends.

\subsection{Goal}
\label{sec:goal}

We aim to verify protocol implementations that frequently renew their communication keys to provide strong security properties.
A notable example is the Signal Double Ratchet protocol.
We consider a slightly simpler protocol, on which Signal is based, involving a single ratchet; the Diffie-Hellman Ratchet.

\subsubsection{Diffie-Hellman Ratchet}
\label{sec:diffie-hellman-ratchet}

The Diffie-Hellman (DH) Ratchet~\cite{perrin2016double} is a continuous key agreement protocol, which repeatedly performs Diffie-Hellman key exchanges to encrypt each message with a new key.
It is presented in Figure~\ref{fig:dh-ratchet}.

\begin{figure}
    \centering
    \includegraphics[width=1.0\textwidth]{figures/DH-ratchet.png}
    \caption{The Diffie-Hellman (DH) Ratchet~\cite{perrin2016double} is a continuous key agreement protocol between two participants, Alice and Bob, which repeatedly performs Diffie-Hellman key exchanges to encrypt each message with a new key.
    Here, \texttt{AeadEnc(K, MSG, ad)} refers to the AEAD encryption of the message \texttt{MSG} with the key \texttt{K} and the associated data \texttt{ad}. \texttt{KDF(a, b)} refers to a key derivation function that derives a new key from two inputs \texttt{a} and \texttt{b}.
    This figure is inspired by a similar figure from the DY* paper~\cite{bhargavan2021text}.}
    \label{fig:dh-ratchet}
\end{figure}

The protocol starts with an established communication key $K_0$, mutually shared by both participants.
The initiator uses the responder's public key and a newly generated secret key to compute a shared Diffie-Hellman secret.
This new shared secret and $K_0$ are input to a key derivation function (KDF) to derive a new communication key $K_1$, which is used to encrypt a payload, i.e.\ \texttt{MSG\textsubscript{1}}.
This step of generating a new key from the previous one is called a \emph{ratcheting step}.
Behind this name, there is the idea of a ratchet, which one could turn in one direction to generate new keys, but that cannot be turned back, meaning that previous keys cannot be derived from the current one.
Then, $K_1$ is used to encrypt the message sent to the responder, accompanied by the initiator's new DH public key $g^{x_1}$.
The responder can compute the same Diffie-Hellman shared secret and take the same ratcheting step to obtain $K_1$, then use $K_1$ to decrypt the message.
This iterative process is repeated for each message, i.e., every payload is encrypted with a different key obtained by ratcheting the previous one.

After this ratcheting process has been performed and has given us a communication key $K_n$, the previous key $K_{n-1}$ is no longer needed and is deleted.
Deleting the previous key is an essential step for a protocol implementation to achieve forward secrecy, which we explain in the following.

\subsubsection{Security properties}
\label{sec:security-properties}

The DH Ratchet protocol is designed to provide strong security properties, such as forward secrecy and post-compromise security.
We define these properties below and explain how the DH Ratchet protocol satisfies them.

\paragraph{Forward secrecy.}
\label{sec:forward-secrecy}

The DH Ratchet protocol is designed to be secure against an attacker recording all previous encrypted messages and obtaining a shared secret or a communication key at some point.
If the attacker compromises a participant, for example, Alice, they may be able to decrypt some messages using the keys and secrets stored in Alice's memory. If Alice keeps storing all previous secrets and session keys, then the attacker would be able to decrypt all previous messages that they previously observed on the network. This is why it is crucial for Alice to delete previous secrets and communication keys as soon as she has derived the new ones.
Indeed, if previous keys are correctly deleted from Alice's memory, then the attacker may only be able to decrypt the last message and not all previous ones.

Therefore, the DH Ratchet protocol satisfies forward secrecy. This property is enabled by two main factors: cryptographically preventing past communication keys from being derived from long-term secrets and current communication keys, and securely deleting previous keys.

\paragraph{Post-compromise security.}
\label{sec:post-compromise-security}

Additionally, the DH Ratchet protocol is designed to be \emph{self-healing}, meaning that it should allow communication to resume securely at some point after a compromise. This is the property of post-compromise security.
Recall that post-compromise security is not achievable after the \emph{unrestricted} compromise of a participant, but we instead consider that some secret data remains available exclusively to the participants after the compromise (post-compromise \emph{via state}~\cite{7536374}).
In the DH Ratchet protocol, we consider that the attacker compromised Alice's $K_n$ communication key \emph{after} she derived the new $K_{n+1}$ key, and after she and her peer Bob have deleted their DH private key they used to compute $K_{n+1}$.
At this point, the attacker cannot obtain $K_{n+1}$ because they cannot have access to the associated DH shared secret.

Therefore, all future communication keys are safe from the attacker, so the DH Ratchet protocol satisfies post-compromise security via state.
Post-compromise security requires that past states do not contain secret data on which future communication depends. This is why it requires fine-grained reasoning about the data occurring in a participant's state at a particular point in time, and secure deletion of old data.

Our methodology to prove these two strong security properties, forward secrecy and post-compromise security, requires a notion of temporality because we have to specify the lapses of time during which certain keys are possibly present in memory. Outside these lapses, keys must not be present in memory because they have either not been generated yet or have already been securely deleted.

\subsection{Versions}
\label{sec:versions}

To introduce a notion of temporality, we divide the time axis into successive time frames. We number these time frames with integers, starting at $0$, and call them \emph{versions}.
Similarly to what is done in DY*~\cite{bhargavan2021text}, each participant's session is given a version field, which keeps track of the current version of the protocol.
At this point, we can uniquely identify a time frame in a protocol session by the triplet $(p, s, v)$, where $p$ is the participant executing the protocol session $s$, and $v$ is the version defining the time frame. We call this triplet a version identifier.

We then use these identifiers to specify the time frames during which certain terms are present in memory.
Recall that each term, e.g.\  a key or a nonce, is assigned a secrecy label stating who can access it. While these labels could previously only be defined from participant or session identifiers, we now allow them to be defined from version identifiers $(p, s, v)$ as well.

We distinguish two cases: \emph{versioned} and \emph{unversioned} terms.
A term is said to be versioned if it is made to be accessible only in one or several specific versions of the current protocol session.
Conversely, a term is said to be unversioned if it is made to be accessible by the current participant or session, i.e.\ in all versions of the current protocol session.
For example, considering the current session $s$ of participant $p$, a term with secrecy label $[(p, s, 0), (p')]$, where $p'$ is any other participant, is versioned because it is only readable in version $0$ of the current session $s$. But a term with secrecy label $[(p)]$ or $[(p, s)]$ is unversioned because it is readable in all versions of the current session $s$.
Additionally, we define a $i$-versioned term as a versioned term that is accessible in version $i$.

The existing methodology already enforces that unversioned terms can only be accessed by participants or sessions allowed by their secrecy label.
A key property of our methodology extension is to ensure that versioned terms can only be accessed when the session is in a version allowed by their secrecy label. Intuitively, this means that an ephemeral key, defined as a versioned value, should only be accessible during a limited time frame defined by the versions allowed by its secrecy label.
The crucial difference of this work compared to the existing methodology is that it allows non-monotonic secrecy labels, i.e.\ a term being readable now might not be readable in all future timepoints.

On a high level, enforcing the time-limited existence of versioned terms requires two kinds of checks.
First, we enforce when creating a versioned term that it should be readable in the current version of the protocol.
Second, we enforce that when increasing the version of a session, all versioned terms that are no longer accessible in the new version have been deleted.
While the first check can be easily implemented similarly to the existing check for unversioned terms, the second check requires more work. Indeed, using Gobra, there is no trivial way to check a condition on all versioned terms that are stored in memory at a particular time point.

This second check is to ensure that ephemeral keys are deleted when they are no longer needed. Let us discuss this in more detail.

\subsection{Enforcing deletion of old data}
\label{sec:enforcing-deletion-of-old-data}

Before increasing the version of a session, we have to securely delete all versioned terms that are no longer accessible in the new version. By doing so, we more generally ensure that terms are only accessible in the versions allowed by their secrecy label.

We discuss next the solution used in DY*. However, this solution is not applicable in our setting, which does not restrict the way implementations store application state. Hence, we afterward present a more generic solution.

\subsubsection{Existing approach in DY*}
\label{sec:existing-approach-in-dy}

In DY*~\cite{bhargavan2021text}, a participant uses a storage API to store all of its knowledge on the trace.
In particular, recall from section~\ref{sec:dy-star} that a participant stores the knowledge of ongoing sessions into an array, composed of each serialized session state, and each session is given a version number.
Upon updating some session state, the participant can also update and increment the version number of the session.
An invariant over the state makes sure that only data from the session's version can be stored, ensuring that old keys cannot remain in memory.
Practically, this means that previous keys are effectively deleted from the state when the session's version is incremented.

This solution is however not applicable to us because, as explained previously, we do not restrict the way implementations store application state, and we use a ghost trace, removed at runtime, which cannot store program data.
Because we do not store the program state on the trace, it makes it impossible to express the same invariant over the state as in DY* in our case.
Furthermore, DY* enforces the invariant over state only at certain time points, namely when the state is stored on the trace, without taking into account the state in-between.
Finally, it is not sure if DY* enforces that outdated keys are \emph{securely} deleted, meaning explicitly zeroed out from memory.
In the next part, we present our generic approach to enforce the deletion of old data.

\subsubsection{Our approach}
\label{sec:our-approach}

As we cannot simply iterate over the full session state to remove outdated keys like in DY*, we present a new approach to ensure that versioned values get safely deleted before their version expires.
Note that our approach only \emph{extends} the existing approach of Arquint's et al.~\cite{ArquintSchwerhoffMehtaMueller23}, which means that our modified library can still be used to verify unversioned protocols in the same way as before.

The intuition of the methodology is to let the developer (that is verifying a protocol implementation) choose when to delete a versioned value.
For this purpose, we provide a \emph{secure} deletion function that deletes a value by zeroing out the memory and ensuring that this write operation is not optimized away by the compiler.
% for which we assume that it erased the value, e.g.\  by zeroing out the memory and ensuring that this write operation is not optimized away by the compiler.
The crucial aspect now is to verify that, before the session version is incremented, the secure deletion function has been called for all versioned values that will no longer be accessible in the new version.

Intuitively, we could solve this problem with a counter. Starting with version $i$, we use the counter $c_i:=0$.
Each time we create a versioned value readable in version $0$, we increment the counter $c_i = c_i + 1$.
And each time we delete a versioned value readable in version $0$, we decrement the counter $c_i = c_i - 1$.
When we increment the version of the session, we check that $c_i = 0$, meaning that all versioned values readable in version $i$ have been deleted.

However, this approach cannot be trivially implemented in our case because we cannot just use a counter \emph{variable} that the developer could access at will: they would just have to manually set it to $0$ before incrementing the version of the session, and the counter check would be meaningless.
We would have to ensure that the developer cannot directly manipulate the counter, which may be difficult to achieve.
Additionally, we want to support concurrency which would require us at least to use an atomic counter or to protect the counter by a lock.
Instead, to solve these challenges without the limitations of a counter variable, we will create a mechanism based on \emph{counting permissions}~\cite{roshardt2021extending}. Those will be explained in the next section, before using them to design our deletion mechanism.

Note that with this approach, one could think that the developer could just never increment the version of the session, and thus would never have to delete any versioned value. While this is true, if the developer wants to verify meaningful properties like forward secrecy, they will have to increment the version at some point to express the property in terms of the version.

\section{Counting permissions}
\label{sec:counting-permissions}

Because keeping track of created and deleted values using a counter variable could be easily bypassed by the developer, we base our work on counting permissions~\cite{roshardt2021extending}.
% In this section, we build our method on the same intuition as the approach explained above, but using counting permissions should prevent the developer from circumventing the deletion mechanism.
While counting permissions follow a similar idea as a counter, they overcome the limitations mentioned earlier and are suitable for our use case, i.e.\ they support arbitrary representations of the application state and can be adapted to support concurrency.

We start by introducing the notion of counting permissions.
Because this permission model is not available in the current version of Gobra, we then explain how we can obtain similar functionality using the existing permission system.

\subsection{Introduction}
\label{sec:counting-permissions-introduction}

Counting permissions are a permission model where permission shares are valued in $\mathbb{Z}\cup\{u\}$, where $u$ represents the identity element of the share addition operation. A share of value $0$ means full permission, a share of value $u$ means no permission, and any other value means partial permission. A non-negative share $n\geq0$ is called a token \emph{factory} and can be split, for any integer $k>0$, into another factory $n+k$ and an equivalent amount of negative token \emph{bundles} of value $-k<0$. A token factory and some amount of token bundles can be summed, and the result is always non-negative (because the subtracted bundle value had to be added to the factory before). 

In particular terms, counting permissions can be used as a counter: a full permission (0) can be split into a factory $1$ and a bundle $-1$ representing incrementing the counter by one.
% In practical terms, this means that starting with full permission ($0$) of some predicate one could use it as a counter. It could be incremented by splitting it into a factory~$1$ and a bundle~$-1$.
A second increment would create a factory~$2$ and a second bundle~$-1$. Invertly, decrementing the counter could be done by summing the factory~$2$ with a bundle~$-1$, resulting in a factory~$1$.

We therefore annotate the library functions such that they keep track of the number of versioned values, i.e.\ increment the counter when creating a new versioned value and decrement the counter when safely deleting such a value.
Unversioned values do not need to be tracked as they do not have to be safely deleted because they can be present in memory for the entire (remaining) execution of the protocol.

To implement a deletion mechanism using the counting permissions model, we use an abstract predicate that we call \texttt{guard(i int)}, which takes a version number as an argument, and on which we initially have full permission $0$. The library functions that create a versioned term readable in version $i$ require access to the token factory $n\geq0$ of \texttt{guard(i)}, and return an incremented share $n+1$, \emph{without} returning the token bundle $-1$. Invertly, the secure deletion function returns a token bundle $-1$ upon deletion of a versioned term readable in version $i$. Therefore, if the developer deletes all $i$-versioned terms, they will obtain as many token bundles $-1$ as the value of the token factory $n$. Summing them together will result in a full permission $n = 0$. This means that we know that no $i$-versioned values exist in memory when we have full permission on \texttt{guard(i)}.

The major difference with a simple counter variable is that the developer \emph{cannot} create a $-1$ token bundle the way they could just decrement the counter variable. They \emph{have to} delete all $i$-versioned terms and cannot circumvent the deletion mechanism.

To support concurrency using counting permissions, we could protect the token factory with a (ghost) lock.
Then, splitting the factory to obtain a bundle, or summing the factory with a bundle, would require acquiring the lock.
This lock would however complicate the entire reasoning as the lock and each thread would have to be aware of the amount of created versioned values.
Thus, in the next section, we present an alternative to counting permissions that, in addition to supporting concurrency without a lock, is supported by Gobra.

\subsection{Implementation in Gobra}
\label{sec:implementation-in-gobra}

Gobra~\cite{wolf2021gobra} currently does not support counting permissions but only fractional permissions, which were explained in section~\ref{sec:permissions}.
Recall that in this model, permission shares are valued in $[0,1]\cap\mathbb{Q}$, a share of value $0/1$ means no permission, a share of value $1/1$ means full permission, and any other value means partial permission.

Because fully encoding counting permissions using fractional permissions is not trivial, we instead restrict ourselves to a solution based on fractional permissions that tracks the number of versioned values with the help of our annotated library functions.
% we just need to obtain some level of functionality sufficient to implement our deletion mechanism.

\subsubsection{Idea}
\label{sec:counting-permissions-idea}

We introduce below two abstract predicates that we use to implement our deletion mechanism.

\begin{gobra}
pred guard(v uint32)
pred receipt(key []byte, v uint32)
\end{gobra}

The \texttt{guard} predicate can be seen as the token factory and is initially given with full permission ($1/1$) to the developer.
The \texttt{receipt} predicate can be seen as a token bundle.
The idea is for all library functions that create a versioned value \texttt{key} readable in version \texttt{v} to require partial permission to \texttt{guard(v)}, and to return the same amount of permission of \texttt{receipt(key, v)}.
Then, upon deletion of \texttt{key}, the secure deletion function requires some amount of permission of \texttt{receipt(key, v)} and returns the same amount of permission of \texttt{guard(v)}.
We illustrate these explanations with the Gobra specification of two basic \texttt{Create} and \texttt{Delete} functions given below.
Note that in Gobra, a function argument annotated with \texttt{ghost} is an argument for verification purposes only, i.e.\ it is not part of the program state and is removed at runtime.

\begin{gobra}
requires acc(guard(version), versionPerm)
ensures  acc(receipt(key, version), versionPerm)
func Create(ghost version, ghost versionPerm) (key []byte) {/*...*/}

requires acc(receipt(key, version), versionPerm)
ensures  acc(guard(version), versionPerm)
func Delete(key []byte, ghost version, ghost versionPerm) {/*...*/}
\end{gobra}

In practice, the developer may have to create several \texttt{v}-versioned values and will consume some amount of permission of \texttt{guard(v)} for each of them.
For each created value, they will receive the same amount of permission of \texttt{receipt(key, v)} as the amount of permission of \texttt{guard(v)} they consumed to create it.
When they want to increment the version of the session, they will have to delete all \texttt{v}-versioned values and will consume all \texttt{receipt(key, v)} fractional permissions.
They will receive the same amount of permission of \texttt{guard(v)} as the consumed \texttt{receipt(key, v)} permission for each deleted value.
Therefore, we know that no versioned value readable in version \texttt{v} remains in memory when we have full permission on \texttt{guard(v)}.
The following lemma expresses this property:

\begin{lemma}\label{lem:full-guard-no-versioned-value}
    We denote $\texttt{perm}$ the function taking a predicate and returning its available permission fraction.
    If there exists a $v \in \mathbb{N}$ such that $\texttt{perm}(\texttt{guard}(v)) = 1$, then $v$ is the current session's version, and no $v$-versioned value exists in memory.
    % Reciprocally, if $v$ is the current session's version and no $v$-versioned value exists in memory, then $\texttt{perm}(\texttt{guard}(v)) = 1$.
\end{lemma}

Consequently, we require full permission on \texttt{guard(v)} to call the function that increments the version of the session.

Additionally, this approach naturally supports concurrency, because separation logic allows us to split the permission of the \texttt{guard} predicate into several fractions and hand each fraction to a different thread.
Doing so, each thread can independently perform creation and deletion operations on versioned values because they only require a fraction of the permission of the \texttt{guard} predicate.

Similarly to counting permissions, the developer cannot bypass the deletion mechanism because they cannot obtain \texttt{guard} or \texttt{receipt} fractional permissions without going through the library functions.
This is assuming that the developer does not use Gobra's \texttt{inhale} statement to bypass the permission system.

Note that the receipt predicate takes the created byte array \texttt{key} as an argument.
This is used at deletion time to verify that we delete the actual value associated with the receipt, before returning the \texttt{guard(v)} permission fraction. Otherwise, the developer could simply delete arbitrary (unversioned) values to transform some \texttt{receipt(key, v)} permission fraction into a \texttt{guard(v)} permission fraction, and thus violate lemma~\ref{lem:full-guard-no-versioned-value}. %circumvent the guarantee of deletion of versioned values.
% We can express the fact that our deletion mechanism cannot be circumvented with the following definition:

% \begin{definition}\label{def:sum-perm-leq-1}

%     Let $v$ represent the current version of the session and $n$ the number of $v$-versioned values in the current state. $\forall i \in \llbracket 0, n \rrbracket$, we denote $key_i$ the $i$-th $v$-versioned value.
%     Then, we can express the following property:
%     \begin{align*}
%         \left(\texttt{perm(guard($v$))} + \sum_{i=1}^n \texttt{perm(receipt($key_i$, $v$))}\right) \leq 1
%     \end{align*}

% \end{definition}

\subsubsection{Choosing the right permission amounts}
\label{sec:choosing-the-right-permission-amounts}

With these library specifications, the developer has some flexibility in choosing fractional permission amounts when invoking library functions.
Indeed, upon creating or deleting a versioned value, the developer chooses the permission amount of the \texttt{guard} or \texttt{receipt} that will be consumed.
Picking too large permission amounts that would result in a contradiction of lemma~\ref{lem:full-guard-no-versioned-value} correctly results in verification errors.
The chosen permission amounts thus only affect completeness.
% With this Gobra implementation, the developer is given more responsibility than in the counting permissions model.

When creating versioned values, the developer has to choose small enough permission amounts of the \texttt{guard} predicate to consume so that all desired values can be created.
For example, if they want to create $3$ versioned values, but consume $1/2$ of \texttt{guard} for the two first values, they will not be able to create the third value because they will not have enough permission of \texttt{guard} left.
This does not affect the soundness of the methodology but simply prevents the developer from implementing their goal.
It is therefore in their interest to carefully choose permission amounts.
Note that unboundedly many versioned values can be created even when it is not statically known how many values will be created in the implementation.
For example, this is doable by consuming $1/2$ of the \texttt{guard} predicate permission for the first created value and dividing the consumed permission by $2$ for each subsequent created value, i.e.\ consuming $1/4$ for the second value, $1/8$ for the third value, etc.

When deleting a versioned value, the developer has to specify the same permission amount of the \texttt{receipt} predicate to consume as the amount that was created by the library when creating the versioned value.
Indeed, automatically picking the available permission amount of \texttt{receipt} in the current context could be insufficient in cases where some permission amount of \texttt{receipt} has leaked or is hidden\footnote{We say that some permission amount to a heap location or a predicate $x$ \emph{leaks} when the total available permission amount of $x$ in the current context is not fully returned to the caller in a postcondition of the current function, so a permission amount of $x$ is lost forever. We say that some permission amount of $x$ is \emph{hidden} when it is \emph{folded} in a predicate $y$, meaning that a permission amount of $x$ is replaced with a permission amount of $y$.}, and is either way not currently supported by Gobra.
% Additionally, in Gobra, we currently cannot know how much permission of \texttt{receipt} is available in the current context.
This is why we require the developer to manually specify the right permission amount of \texttt{receipt} to consume.
% However, they could specify a smaller amount than the amount they have, and the deletion function call would work.
If the developer calls the delete function and specifies a smaller amount than the permission amount of the \texttt{receipt} predicate that was created by the library, while there will be no immediate verification error, the developer will not be able to recover the full permission to the \texttt{guard} predicate.
This will prevent them from incrementing the version of the session.
Again, the methodology's soundness remains unaffected, but the developer has to be careful when specifying the permission amount of \texttt{receipt} to consume to avoid completeness issues.
% the only consequence is the developer's inability to realize their objective.
% It is therefore in their interest to specify the full \texttt{receipt} permission amount upon deletion.
The following lemma expresses this property:

\begin{lemma}\label{lem:sum-perm-eq-1}

    % We consider the same notations as in Definition~\ref{def:sum-perm-leq-1}.
    Let $v$ represent the current version of the session and $n$ the number of $v$-versioned values in the current state. $\forall i \in \llbracket 1, n \rrbracket$, we denote $key_i$ the $i$-th $v$-versioned value.
    Additionally, we assume the developer always deletes a versioned value specifying the same permission amount as the one they used to create it, and more generally that no permission amount of the predicates \texttt{guard} and \texttt{receipt} has leaked or is hidden.
    Then, we can express the following property:
    \begin{align*}
        \left(\texttt{perm(guard($v$))} + \sum_{i=1}^n \texttt{perm(receipt($key_i$, $v$))}\right) = 1
    \end{align*}

\end{lemma}

To conclude, we have obtained a satisfactory approach to track the number of versioned values, which meets all of our requirements.
Our approach is, contrary to counting permissions, supported by Gobra.
As we wanted, our approach also supports arbitrary representations of the application state, concurrency and unboundedly many versioned values.
% To conclude, we have identified a satisfactory approach for achieving functionality reminiscent of counting permissions in Gobra.
Despite giving more flexibility to the developer, this method is sound and constitutes the core of our deletion mechanism.

\section{Extension of the library}
\label{sec:extension-of-the-library}

We introduced a general mechanism to enforce the deletion of versioned values before the end of their time frame, defined in terms of versions allowed by their secrecy label.
This mechanism is central to the methodology.
In this section, we explain how we integrate it in Arquint's et al.\ Reusable Verification Library~\cite{ArquintSchwerhoffMehtaMueller23}, to provide the developer with functions handling versioned values.

We start by explaining how we store and access the current version of a session.
Then, we explain how we adapted the functions that create a value, e.g.\  a nonce, to support versioned values according to our methodology.
Similarly, we present our secure deletion function made to delete those versioned values.
We continue by introducing two special cases that required particular effort to support versioned values and fit our methodology: key ratcheting and encryption/decryption. 
Afterward, we describe our function for increasing the version of a session when all “old” values have been deleted.

Finally, we give a glimpse of an alternative approach to implement a similar deletion mechanism, based on obligations, which can be used instead if the targeted verifier supports obligations.
% in the case of a verifier that supports obligations, which is not the case of Gobra. 

\subsection{Storing the current session version}
\label{sec:storing-the-current-session-version}

We will later see several library functions that have to compare a version appearing in a secrecy label to the \emph{current} version of the session.
Retrieving the current version from the global trace directly is not possible because, as it is a concurrent data structure, there might be interleaving operations by other participants or sessions between the moment we retrieve the version and the moment we use it.
However, we assume that each session has its own version, which can only be altered by this session.
Hence, we turn the version into a local field within the library that can only be altered by corresponding library calls.

% Before we can implement the deletion mechanism in detail, we need a place to store the current version of a protocol session.
Currently, the library already handles the storage of the current protocol participant and session.
These are stored in a field called \texttt{owner} that is either a participant identifier $(p)$ or a session identifier $(p,s)$, where $p$ is a participant and $s$ is a session.
This field is used in the concurrent data structure, as a key to a dictionary mapping identifiers to their corresponding snapshot, where we recall that snapshots are local copies of the global trace.
% Even though a first thought could be to store the version $v$ as part of the \texttt{owner}, in a version identifier $(p,s,v)$, a protocol participant should keep using the same snapshot mapping during a protocol session.
Since \texttt{owner} is used as a key to the snapshots mapping, we cannot include the version in the \texttt{owner} field because this would result in a different map lookup whenever the session's version is incremented.

Therefore, we store the current version of a session in a separate field, as an integer.
The session is stored as part of the library state, which makes it easily accessible to all library functions.
For a function taking a \texttt{LabeledLibrary} struct \texttt{l}, holding the state of the library, the current version of the session will be referred to as \texttt{l.Version()} in the future code figures.
The owner is similarly obtainable using \texttt{l.Owner()}.
Additionally, it is often useful when working with secrecy labels to know the complete version identifier $(p,s,v)$. This is the combination of the owner and version fields, which is returned by \texttt{l.OwnerWithVersion()}.

\subsection{Creation of versioned values}
\label{sec:creation-of-versioned-values}

It is easy to categorize functions that create values: they all return full permission to a new memory predicate \texttt{Mem} of the created value.
The library provides three functions to create values: \texttt{CreateNonce} to create some random value, \texttt{GeneratePkeKey} to create a public/private key pair, and \texttt{GenerateDHKey} to create a secret key for Diffie-Hellman key exchange.
Those three functions are implemented very similarly and have required the same changes to support versioned values. Therefore, we will only discuss the \texttt{CreateNonce} function in this section. Its simplified specification is provided in Figure~\ref{lst:create-nonce}.

\begin{figure}
    \begin{gobra}
requires versionPerm >= 0
requires versionPerm == 0 ==>
    CanFlow(l.Snapshot(), nonceLabel, Readers(set[p.Id]{l.Owner()}))
requires versionPerm > 0 ==>
    acc(guard(l.Version()), versionPerm) &&
    l.Owner().IsSession() &&
    CanFlow(l.Snapshot(), nonceLabel,
        Readers(set[p.Id]{l.OwnerWithVersion()}))
ensures  err == nil && versionPerm > 0 ==>
    acc(receipt(nonce, l.Version()), versionPerm)
ensures  err == nil ==> Mem(nonce)
func (l *LabeledLibrary) CreateNonce(ghost nonceLabel SecrecyLabel,
    ghost versionPerm perm) (nonce []byte, err error) {
    // ...
}
    \end{gobra}
    \caption{Specification of \texttt{CreateNonce} showcasing the changes to support versioned values. Preconditions, postconditions and arguments that are not relevant to the changes have been omitted.
    \texttt{CanFlow} represents the flow relation between secrecy labels, as defined in section~\ref{sec:dy-star}, and takes a snapshot of the global trace and two secrecy labels as arguments.}
    \label{lst:create-nonce}
\end{figure}

This function takes a \texttt{versionPerm} argument, which is required to be non-negative.
The developer can use this argument to specify whether they want to create a versioned or unversioned nonce. Choosing $0$ means that the nonce will be unversioned, and choosing a strictly positive value means versioned.
In both cases, when the function completes with no error, it returns full permission of the memory predicate \texttt{Mem(nonce)}, expressing that the nonce is now stored in memory.

\subsubsection{Unversioned nonce}
\label{sec:unversioned-nonce}

In this case, the developer chooses $0$ for the \texttt{versionPerm} argument.
As required by lines 2-3, the provided secrecy label has to flow to the library owner because otherwise, the developer could create a nonce that they are not allowed to read, contradicting the modeling of corruption.
Depending on if sessions are used, the library owner is either a participant $(p)$ or a session $(p,s)$ identifier.
The other preconditions do not have to be satisfied because they are only relevant to the versioned case.

Because no version identifier $(p,s,v)$ flows to $(p,s)$ or $(p)$, we know when verifying this precondition that the nonce label must be composed of some non-versioned identifier, e.g.\  is unversioned.
Therefore, when the developer chooses $0$ for the \texttt{versionPerm} argument and proves that the nonce label is unversioned, then the library behaves as the original implementation and creates an unversioned nonce, without consuming any permission of \texttt{guard}.

\subsubsection{Versioned nonce}
\label{sec:versioned-nonce}

In this second case, the developer chooses a strictly positive \texttt{versionPerm} value.
This value is used to specify the amount of permission of \texttt{guard} to consume (line 5), as discussed in section~\ref{sec:choosing-the-right-permission-amounts}.
Additionally, the library owner must be a session identifier (line 6) and not a participant, because a version identifier $(p,s,v)$ requires a session $s$ to be defined.
Finally, the nonce label must flow to the library owner \emph{at the current version} (lines 7-8).
This is to at least ensure that the created nonce is readable by the current session and version.

However, the flow relation is not enough to ensure that the nonce label is actually versioned. To do so, one would have to prove that the nonce label \emph{cannot} flow to the library owner (without version), as shown in this precondition:

\begin{gobra}
requires versionPerm > 0 ==>
    !CanFlow(l.Snapshot(), nonceLabel, Readers(set[p.Id]{l.Owner()}))
\end{gobra}

Establishing this precondition is however not possible because it would entail proving that no reader specified in the nonce label has been corrupted. Indeed, if one of the readers had been corrupted, then the nonce label would flow to \emph{Public}, so it would flow to any secrecy label, including the library owner.
Therefore, we decided to not enforce this condition, as it is not necessary to ensure soundness of the methodology.
If the developer “accidentally” creates a nonce with an unversioned label, but uses a strictly positive \texttt{versionPerm} (meant to be used for versioned values), verification will not fail.
However, they will be bound by the constraints of the deletion mechanism. For now, this means that they will be forced to safely delete their unversioned nonce before the next increment of the session's version (but we will see in section~\ref{sec:conversion-function} that another way is possible).
Either way, this will just result in additional proof obligations without any benefits for proving security properties because the nonce's secrecy label is still the same, i.e.\ unversioned.
% too tight constraints but does not call into question the soundness of the deletion mechanism.

Finally, the postcondition (lines 9-10) states that the developer will receive the same (strictly positive) amount of permission of \texttt{receipt} as the amount of permission of \texttt{guard} consumed. This is indeed what was defined in section~\ref{sec:counting-permissions-idea}.

\subsection{Secure deletion of versioned values}
\label{sec:secure-deletion-of-versioned-values}

The library provides the function \texttt{DeleteSafely} to securely delete a versioned value. Its implementation and simplified specification are provided in Figure~\ref{lst:delete-safely}.

\begin{figure}
    \begin{gobra}
requires versionPerm > 0
requires acc(receipt(value, l.Version()), versionPerm)
requires Mem(value)
ensures  acc(guard(l.Version()), versionPerm)
func (l* LabeledLibrary) DeleteSafely(value []byte,
    ghost versionPerm perm) {
    // Overwrite the value with zeros
    for i := range value {
        value[i] = 0
    }
    // Prevent the compiler from optimizing the entire function
    runtime.KeepAlive(value)
    return
}
    \end{gobra}
    \caption{Implementation and specification of \texttt{DeleteSafely}, used to delete a versioned value. Preconditions, postconditions and arguments that are not relevant to the deletion mechanism have been omitted.}
    \label{lst:delete-safely}
\end{figure}

This function behaves like the opposite of the \texttt{CreateNonce} function in the \emph{versioned} case.
It takes a strictly positive \texttt{versionPerm} argument, which is used to specify the amount of permission of \texttt{receipt} to consume (line 2).
The same amount of permission of \texttt{guard} is then returned (line 4).
Recall that the \texttt{DeleteSafely} function does not check that the given \texttt{receipt} permission amount for this value is the full amount of permission available.
But as discussed in section~\ref{sec:choosing-the-right-permission-amounts}, it is in the developer's interest to specify the full amount if they want verification to succeed, i.e.\ eventually being able to increment the session's version.
Additionally, \texttt{DeleteSafely} consumes the memory predicate of the deleted value (line 3), expressing that the value is no longer stored in memory.

To securely erase a value from memory, we use the implementation shown in lines 7-12 of Figure~\ref{lst:delete-safely}.
This ensures that the memory is zeroed out and that this operation is not optimized away by the compiler.
Line 12 currently seems sufficient to prevent the Go compiler from eliminating the function's body.
Various alternatives have been surveyed by Yang et al.~\cite{yang2017dead} for the C language.

\subsection{Creating values with multiple versions for ratcheting}
\label{sec:creating-values-with-multiple-versions-for-ratcheting}

When presenting the Diffie-Hellman Ratchet~\cite{perrin2016double} in section~\ref{sec:diffie-hellman-ratchet}, we explained the purpose of the ratcheting step, which is to derive a new communication key from the previous one. Once a new communication key has been derived, the previous one is no longer needed and should be deleted.
Intuitively, the new key should exist in a more recent time frame than the previous one, and both keys should coexist for a short period of time, from the ratcheting step to the deletion of the previous key.

In terms of versions, this means that if the previous key $K_n$ is versioned with the current version $v$, it is not sufficient to create the new key $K_{n+1}$ only with version $v+1$ because it could not coexist with $K_n$.
% we want to create a new versioned key $K_{n+1}$ with version $v+1$. This way, the developer could increment the session's version after the ratcheting step, which would enforce the deletion of $K_n$.
Additionally, we have seen in section~\ref{sec:versioned-nonce} that creating a versioned key requires it to be readable at least in the current context. This means that when creating $K_{n+1}$, we would have to prove that it is readable in the current version $v$. To make $K_{n+1}$ readable both in version $v$ and $v+1$, we could for example use the secrecy label $[(p,s,v), (p,s,v+1)]$, where $p$ and $s$ are the participant and session of the library owner.
This label now allows $K_n$ and $K_{n+1}$ to coexist in version $v$.
Then, after the ratcheting step, the developer would want to increment the session's version to $v+1$. The methodology enforces that $K_n$ is deleted before the version increment.

However, while this label makes $K_{n+1}$ theoretically readable in version $v+1$, it does not yet align with our deletion methodology. Because $K_{n+1}$ is created while the current version is $v$, a permission fraction of \texttt{guard(v)} (and not \texttt{guard(v+1)}) will be consumed\footnote{For the sake of clarity, note that in this and subsequent paragraphs, $v$ and \texttt{v} denote the same version value.}. This fraction can currently be restored only by deleting $K_{n+1}$ \emph{before} incrementing the session's version to $v+1$, which would defeat the purpose of the ratcheting step.

\subsubsection{Conversion function}
\label{sec:conversion-function}

To solve this problem, we introduce a generic way to migrate values from one version to the next one if this is permitted by their secrecy labels.
Intuitively, a versioned value \texttt{key} created in version $v$ has consumed some permission of \texttt{guard(v)} and returned some permission of \texttt{receipt(key, v)}.
If \texttt{key}'s secrecy label also flows to the next version $v+1$, we want to allow \texttt{key} to continue to exist in version $v+1$.
To do so, we offer the developer to \emph{convert} \texttt{key}'s receipt to a new \texttt{receipt(key, v+1)}. At the same time, we return the consumed \texttt{guard(v)} permission but consume an equivalent amount of \texttt{guardNext(v+1)} permission, to make the permission amounts behave \emph{as if} the developer had created \texttt{key} directly in version $v+1$.
Note that we use a different predicate \texttt{guardNext(v+1)}, playing the same role as \texttt{guard(v+1)}, for reasons that will be explained in the next section.
Ultimately, this means that before incrementing the session's version to $v+2$, the deletion methodology will either force the developer to safely delete \texttt{key} or convert it once more if permitted by its secrecy label.

From this intuition, we can define the \texttt{ConvertToNextVersion} function shown in Figure~\ref{lst:convert-to-next-version}.
Similarly to \texttt{CreateNonce}, the library owner must be a session identifier (line 1) and not a participant. A positive fraction of the existing \texttt{receipt} permission and the next version's \texttt{guard} permission is consumed (lines 2-4). Finally, the secrecy label of the value must flow to the next version (lines 5-6).
In return, \texttt{ConvertToNextVersion} returns the same amount of permission of the current version's \texttt{guard} (line 7) that was consumed when creating the value. It also returns a \texttt{receipt} for the next version (line 8).

\begin{figure}
    \begin{gobra}
requires l.Owner().IsSession()
requires versionPerm > 0
requires acc(receipt(value, l.Version()), versionPerm)
requires acc(guardNext(l.Version() + 1), versionPerm)
requires CanFlow(l.Snapshot(), GetLabel(valueT),
    Readers(set[p.Id]{l.OwnerWithNextVersion()}))
ensures  acc(guard(l.Version()), versionPerm)
ensures  acc(receipt(value, l.Version() + 1), versionPerm)
func (l* LabeledLibrary) ConvertToNextVersion(value []byte,
    valueT Term, versionPerm perm)
    \end{gobra}
    \caption{Specification of the abstract \texttt{ConvertToNextVersion} function, converting consumed and emitted \texttt{guard} and \texttt{receipt} permission fractions to the next version when the secrecy label of the value allows it. Preconditions and postconditions that are not relevant to the conversion mechanism have been omitted.}
    \label{lst:convert-to-next-version}
\end{figure}

The \texttt{ConvertToNextVersion} function solves our ratcheting problem. While in a protocol session with version $v$, we can obtain a new key $K_{n+1}$ with secrecy label $[(p,s,v), (p,s,v+1)]$, where $p$ and $s$ are the participant and session of the library owner, from a key $K_n$ versioned with version $v$. At this point, the two keys coexist in version $v$.
The developer can then convert $K_{n+1}$ to the next version, meaning that it replaces the obligation to delete $K_{n+1}$ in version $v$ with an obligation to delete $K_{n+1}$ in version $v+1$.
After this conversion, the developer can delete the old key $K_n$ and has now obtained full permission to the \texttt{guard(v)} predicate. They can now increment the session's version to $v+1$.

\subsubsection{Handling mutliple guards}
\label{sec:handling-mutliple-guards}

While the conversion function solves the initial ratcheting problem, it introduces a new challenge: we now have to deal with two \texttt{guard} predicates at the same time. One, \texttt{guard(v)}, for the current version and one, \texttt{guardNext(v+1)} for the next version.
Otherwise, the conversion function would not be able to consume a fractional amount of the next version's \texttt{guardNext} predicate.
Because a session's version is initialized at $0$, it implies giving the developer full permission to both \texttt{guard(0)} and \texttt{guardNext(1)} predicates at the beginning of a protocol session.

Some parts of the implementation of our deletion mechanism rely on the existence of a single \texttt{guard(v)} predicate, where $v$ is necessarily the current version of the session.
In particular, some helper functions that play a role in the deletion mechanism do not have access to the session state, so do not know the current version.
In these cases, \texttt{guard(v)} can be used to bind the current version \texttt{v} to the function's argument.
% It is then handy to give them access to a \texttt{guard(v)} permission fraction, so they know that $v$ is the current version.
% For example, the body of \texttt{CreateNonce} calls a trusted implementation, called \texttt{CreateNonceImpl}, which generates a random nonce and stores it in a byte array.
% As this implementation is in the library, we want to prevent the developer from calling it with arguments that would compromise the soundness of the methodology.
% In particular, \texttt{CreateNonceImpl} does not have access to the session state, so it does not know the current version. 

% We use a simple trick to keep the assumption that there is only one \texttt{guard} predicate at a time. We define an additional predicate:
To prevent developers from accidentally calling these helper functions with the next version instead of the current one, we introduce a distinct predicate:
\begin{gobra}
pred guardNext(v uint32)
\end{gobra}

The \texttt{guardNext} predicate is another abstract predicate, like \texttt{guard}, and is used in our methodology for the same purpose as \texttt{guard}, but for the next version. 
% In practice, it means that we initially give the developer full permission on \texttt{guard(0)} and \texttt{guardNext(1)} predicates when creating a session.
% This also requires us to slightly change the \texttt{ConvertToNextVersion} implementation given in Figure~\ref{lst:convert-to-next-version}.
% We replace line 4 with the following:
% \begin{gobra}
% requires acc(guardNext(l.Version() + 1), versionPerm)
% \end{gobra}
Using this simple adaptation, we can rely on the fact that at any time, the existing \texttt{guard} predicate has the current version as argument.
This is expressed in the following lemma:

\begin{lemma}\label{lem:unique-version}
    \begin{align*}
        \forall v_1, v_2 \in \mathbb{N}, \texttt{perm}(\texttt{guard}(v_1)) > 0 \land \texttt{perm}(\texttt{guard}(v_2)) > 0 \Rightarrow v_1 = v_2
    \end{align*}
\end{lemma}

\subsection{Encryption and decryption of versioned values}

In section~\ref{sec:creation-of-versioned-values}, we categorized functions that create values as the ones returning full permission to a new memory predicate of the created value.
Functions that fit into this category, which we have not mentioned yet, are \emph{encryption} and \emph{decryption} functions.
Indeed, encryption functions take (and return) read permission to a plaintext, encrypt it to create a ciphertext, and return full permission on a new memory predicate for the ciphertext.
Invertly, decryption functions take (and return) read permission to a ciphertext, decrypt it to create a plaintext, and return full permission on a new memory predicate for the plaintext.
Both functions create a new value that is stored in memory (a ciphertext and a plaintext respectively), we should therefore make sure they are compatible with our deletion methodology.

\subsubsection{Encryption}

Encryption is the simpler case. By definition of secrecy labels, an encryption function creates a \emph{public} ciphertext, which is unversioned.
% As this ciphertext is meant to be sent on the network, which the attacker can read, it would not make sense to create a ciphertext with a restrictive secrecy label, let alone a versioned one.
Therefore, we do not need to change the encryption function to support versioned values.

\subsubsection{Decryption}

% The decryption case requires more work. 
Since a decryption function creates a plaintext, whose value is the same as the original plaintext used for encryption, the returned plaintext might contain versioned values.
% Its secrecy label should therefore be the same as the original plaintext's secrecy label.

As a simple example, suppose that a participant creates a versioned value $key$, and then encrypts and decrypts it.
They will obtain a copy $key_{copy}=key$ of the initial versioned value, with its own memory predicate.
While the current deletion methodology forces the developer to delete (or convert) the versioned value $key$ before the next version increment, we need to adapt the methodology to decryption functions to also enforce the deletion of $key_{copy}$.

Intuitively, we want to treat the decryption function like a creation function and consume some permission of \texttt{guard} only when the created plaintext is versioned.
However, we can not refer to the plaintext or its secrecy label in the preconditions of the decryption function to distinguish between the case where the plaintext is versioned, in which we require a fraction of the \texttt{guard} predicate, and the case where the plaintext is unversioned.
% As the decrypted plaintext is the result of the decryption function, we do not know anything about its secrecy label before calling it. This prevents us from using the plaintext secrecy label in a precondition to the decryption function to condition whether we consume a \texttt{guard} permission or not.

A possible solution to this problem would be to always require partial permission of \texttt{guard} when calling the decryption function.
Then, this permission could be returned later when the developer manages to prove that the decrypted plaintext is unversioned.
However, this is not ideal because it would always require the developer to use the \texttt{guard} predicate to decrypt, even when verifying a protocol that does not use versioned values at all and should thus not be affected by the deletion mechanism.

Instead, we take advantage of an existing encryption property implemented in all encryption functions of the library: everyone who can read the key used for decryption can possibly obtain the plaintext and must thus be able to read it.
In terms of secrecy labels, this means that the secrecy label of the plaintext must flow to the secrecy label of the used secret key\footnote{In asymmetric encryption, while we encrypt with the public key, we consider the label of the private (decryption) key for this property.}.
In particular, this means that a versioned plaintext must be encrypted with a versioned key.
Upon decryption, while we do not know the secrecy label of the plaintext to be created, we know the secrecy label of the key used for decryption.
We thus over-approximate and treat the plaintext as versioned if it was encrypted using a versioned key.
% The intuition is to consider that versioned encryption keys are mostly used to encrypt versioned plaintexts, so we could require partial permission of \texttt{guard} only when the decryption key is versioned.
This is a sound overapproximation that should not burden the developer in practice.

Proving that the decryption key is versioned involves proving that its secrecy label \emph{does not} flow to the library owner. We have already seen when creating a versioned nonce section~\ref{sec:versioned-nonce} that such a negation is not provable in general.
Instead, we adopt the same workaround and require the developer to specify whether the decryption key is versioned or not, using a \texttt{versionPerm} argument.
The simplified specification of the AEAD decryption function \texttt{AeadDec} is provided in Figure~\ref{lst:aead-dec}.
Like in the \texttt{CreateNonce} function, the \texttt{versionPerm} argument must be non-negative (line 1) and is used to specify whether the decryption key is versioned or not.

\begin{figure}
    \begin{gobra}
requires versionPerm >= 0
requires versionPerm == 0 ==>
    CanFlow(l.Snapshot(), GetLabel(keyT),
        Readers(set[p.Id]{l.Owner()}))
requires versionPerm > 0 ==>
    acc(guard(l.Version()), versionPerm) &&
    l.Owner().IsSession()
ensures  err == nil ==> Mem(res)
ensures  err == nil && versionPerm > 0 ==>
    acc(receipt(res, l.Version()), versionPerm)
func (l *LabeledLibrary) AeadDec(ghost keyT tm.Term,
    ghost versionPerm perm) (res []byte, err error) {
    // ...
}
    \end{gobra}
    \caption{Specification of \texttt{AeadDec}, showcasing the changes to support versioned values in AEAD decryption. Preconditions, postconditions and arguments that are not relevant to the changes have been omitted.}
    \label{lst:aead-dec}
\end{figure}

If the developer chooses $0$ for the \texttt{versionPerm} argument, the decryption key is meant to be unversioned, which the developer has to prove on lines 2-4.
In this case, this is the only modification to the original implementation of the \texttt{AeadDec} function.
Because the decryption key is unversioned, the resulting plaintext is necessarily also unversioned, which justifies that the deletion methodology does not apply in this case.

If the developer chooses a strictly positive \texttt{versionPerm} value, the decryption key is meant to be versioned. 
As explained before, we do not create a proof obligation that the decryption key is versioned.
As mentioned in section~\ref{sec:choosing-the-right-permission-amounts}, this over-approximation does not affect soundness but only forces an implementation to safely delete a plaintext in case it would not be necessary.
% In a similar manner as in section~\ref{sec:choosing-the-right-permission-amounts}, we can prove that this does not impact soundness and it is in the developer's interest to use a versioned decryption key in this case.
We then consume a partial permission of \texttt{guard} (line 6) and return the same amount of permission of \texttt{receipt} (lines 9-10).
Additionally, the library owner must be a session identifier (line 7) for versions to make sense.
Then, if decryption succeeds, the resulting plaintext is returned and a memory predicate is issued (line 8), expressing that it is now stored in memory.

Finally, let's reason about the case where the encryption key is versioned, but not the encrypted content.
% This case is expected to be rare in practice, as there are no benefits in encrypting an unversioned plaintext (that could exist for a whole session) with a versioned key (that is bound to exist for a short period of time).
When it happens, the developer is forced to hand a strictly positive permission fraction of \texttt{guard}. 
They will receive the same amount of permission of \texttt{receipt} for the plaintext in return as if it was versioned.
Since the plaintext is unversioned and exists in the current version, it means that its secrecy label allows the current session or participant to access it.
This means that it could be converted to the next version infinitely with the \texttt{ConvertToNextVersion} function, which would allow the value to keep existing in memory despite version increments.
Although it works, converting this value for each version would be a verification burden in practice.
This is why we offer an additional library function, provided in Figure~\ref{lst:guard-from-unversioned-receipt}, which checks if a value associated with a receipt is unversioned (lines 3-4), and if so returns the consumed \texttt{guard} permission (line 5).
This conceptually removes the corresponding values from our deletion tracking mechanism.

\begin{figure}
    \begin{gobra}
requires versionPerm > 0
requires acc(receipt(value, l.Version()), versionPerm)
requires CanFlow(l.Snapshot(), GetLabel(valueT),
    Readers(set[p.Id]{l.Owner()}))
ensures  acc(lib.guard(l.Version()), versionPerm)
func (l* LabeledLibrary) GuardFromUnversionedReceipt(value []byte,
    valueT Term, versionPerm perm)
}
    \end{gobra}
    \caption{Specification of the abstract \texttt{GuardFromUnversionedReceipt} function, removing an unversioned value from the deletion mechanism. Preconditions and postconditions that are not relevant to the deletion mechanism have been omitted.}
    \label{lst:guard-from-unversioned-receipt}
\end{figure}

\subsection{Increasing the version of a session}

After having seen all cases in which a versioned value can be created, for one or several versions, and deleted, we explain how to increment the version of a session.
This is done using the \texttt{BumpVersion} function, whose simplified implementation is provided in Figure~\ref{lst:bump-version}.

\begin{figure}
    \begin{gobra}
requires acc(guard(l.Version()), 1/1)
requires nextPerm >= 0
requires acc(guardNext(l.Version() + 1), nextPerm)
ensures  l.Version() == old(l.Version()) + 1
ensures  acc(guard(l.Version()), nextPerm)
ensures  acc(guardNext(l.Version() + 1), 1/1)
func (l* LabeledLibrary) BumpVersion(nextPerm perm) {
    exhale acc(guard(l.Version()), 1/1)
    exhale acc(guardNext(l.Version() + 1), nextPerm)
    l.manager.version = l.Version() + 1 // Increment the version
    inhale acc(guard(l.Version()), nextPerm)
    inhale acc(guardNext(l.Version() + 1), 1/1)
}
    \end{gobra}
    \caption{Implementation and specification of \texttt{BumpVersion}, incrementing the session's version.
    In the function's body, \texttt{exhale} is used to consume permission and \texttt{inhale} to emit permission.
    Note that after the session's version is incremented line 10, a call to \texttt{l.Version()} returns the incremented version, not the old one.
    Preconditions, postconditions and statements that are not relevant to the deletion mechanism have been omitted.
    In particular, incrementing the session's version requires permission to modify the library, which does not appear in this simplified specification.}
    \label{lst:bump-version}
\end{figure}

As explained in the core idea of the methodology (section~\ref{sec:counting-permissions-idea}), the developer must have deleted all $v$-versioned values before incrementing the session's version $v$ to $v+1$. This means that the developer must have obtained the full permission of the \texttt{guard(v)} predicate, which corresponds to the precondition on line 1.
% This was exactly the purpose of the deletion mechanism, as written in Definition~\ref{lem:full-guard-no-versioned-value}.
Indeed, by lemma~\ref{lem:full-guard-no-versioned-value}, full permission to \texttt{guard(v)} implies that all $v$-versioned values have been deleted.

Additionally, we have seen in section~\ref{sec:creating-values-with-multiple-versions-for-ratcheting} that, if allowed by their secrecy label, $v$-versioned values can be converted to version $v+1$, which consumes a partial permission of the \texttt{guardNext(v+1)} predicate.
This means that before incrementing the session's version, the developer has some amount of permission of \texttt{guardNext(v+1)} that may vary between $0$ and $1$.
Thus, the \texttt{BumpVersion} function takes a \texttt{nextPerm} argument, and turns \texttt{nextPerm}-many permissions of \texttt{guardNext(v+1)} into \texttt{nextPerm}-many permissions of \texttt{guard(v+1)} (see the preconditions lines 2-3 and the postcondition line 5).
This happens because the \texttt{BumpVersion} function increments the session's version (done on line 10, ensured on line 4).
Now that the session's version is $v+1$, the methodology explained in section~\ref{sec:handling-mutliple-guards} requires us to use the predicate \texttt{guard(v+1)} instead of \texttt{guardNext(v+1)}.
Finally, the \texttt{BumpVersion} function returns full permission to the \texttt{guardNext(v+2)} predicate (postcondition line 6).
% This follows the intuition that each session's version comes with full permission to a \texttt{guard} predicate 

After incrementing the session's version to $v+1$, we are in a similar situation as in version $v$ but with all predicates shifted by one version.
We have partial permission to \texttt{guard(v+1)}, and we still may have some receipts from values converted before the version increment.
As those receipts are for version $v+1$, we could delete them to obtain full permission to \texttt{guard(v+1)}.
In parallel, permissions to \texttt{guard(v+1)} and \texttt{guardNext(v+2)} allow us to create and convert new values, exactly like before.

Note that similarly to section~\ref{sec:choosing-the-right-permission-amounts}, it is in the developer's interest to specify in \texttt{nextPerm} the full amount of permission of \texttt{guardNext(v+1)} that they have. If they provide a lower amount, the function call to \texttt{BumpVersion} will still succeed, but they will not be able to retrieve the full \texttt{guard(v+1)} permission afterward, which will prevent them from incrementing the session's version to $v+2$.

\subsection*{Summary}
In this section, we have seen how we adapted the Reusable Verification Library to support versioned values, and how the implemented mechanism enforces the deletion of those values at the end of their time frame.
While the end result is functional and sound, we have come across various challenges that we had to solve by complexifying the methodology a bit.
In the next section, we will give a glimpse into an alternative approach to implementing the deletion mechanism more simply, in case obligations are supported by the targeted program verifier.

\section{Alternative design using obligations}
\label{sec:alternative-design-using-obligations}

An obligation~\cite{bostrom2014modular}, defined for a thread, specifies an action to be eventually performed by this thread. An obligation is initially \emph{emitted}, and once the action is performed, the obligation is \emph{discharged}.

In this section, we first present how we could use obligations to implement the deletion mechanism in a simpler way.
Then, as Gobra does not support obligations, we present a way to add them to the language to be able to implement the deletion mechanism.
This section will not be as exhaustive as the description of our deletion mechanism and only aims at giving an intuition of how obligations could be used to implement it.

\subsubsection{Idea}
\label{sec:obligations-idea}

With a verifier supporting obligations, we could, upon creation of a time-sensitive value, emit an obligation to delete it before the next version increment. 
In practice, the obligation would be a construct linking the versioned value to its version number.
The obligation can then be discharged upon calling the secure deletion function on the value.
Then, when incrementing the protocol's session version, we check that all existing obligations are valid: meaning that the version defined in the obligation is greater than or equal to the new version number.
This means that “old” obligations, with the previous version number, must have been discharged before the version increment.

The obligation mechanism would therefore be composed of two main parts: an obligation construct, and a way to check that all existing obligations satisfy certain properties.

\subsubsection{Adding obligations to Gobra}
\label{sec:adding-obligations-to-gobra}

In this section, we present a way to add obligations to Gobra to solve the particular problem of implementing our deletion mechanism.
To add obligations to Gobra, we first need to define the obligation construct.
In our case, it should be parameterized by the value to delete and its version number.
We therefore introduce the keyword \texttt{obligation} to define an obligation in Gobra, and we use a syntax similar to the definition of an abstract predicate:
\begin{gobra}
obligation Obl(key []byte, version uint32)
\end{gobra}
This construct could then be emitted upon creation of a versioned value, by returning it in the creation function's postcondition.
Invertly, the secure deletion function would require the obligation as a precondition, and would not return it to discharge it.

The second part of the mechanism is to have an assertion capable of checking certain properties for all existing obligations. This assertion could then be evaluated upon incrementing the session's version.
To do so, our main challenge is to ensure that this assertion has access to all existing obligations in its scope.
Indeed, if the obligations are framed around a function call, they will not be visible to the callee.
% not passed in function calls from a caller to a callee, they will \emph{leak} and will not be visible to the callee. It would be as if the obligation had been discharged.
And if obligations are not returned to the caller after a function call, they will leak and will not be visible to the caller.

To avoid this, we introduce \emph{frame checks}, to ensure that all obligations are passed to a function call, and leak checks, to ensure that all obligations are returned to the caller at the end of a function call.
We can implement these frame and leak checks by using inhale-exhale expressions available on the Viper level.
These expressions can be used in preconditions and postconditions and will only be evaluated either in the caller or in the callee context, which gives us sufficient expressivity.
% Within an inhale-exhale expression, we can use the \texttt{forperm} construct to quantify over all obligations in the current context.
% The idea is to add preconditions and postconditions to all functions to make sure that all obligations in scope are passed in function calls. This ensures that in any function, all existing obligations are in scope.
When verifying Gobra files, the Gobra code is first translated to Viper code, which is then verified.
To add frame and leak checks to all Gobra functions, we could modify the translation process to automatically add such checks to all Viper functions.
In our case, a frame check and a leak check can be defined in Viper with the same assertion, using the \texttt{forperm} construct to quantify over all obligations in the current context:
\begin{gobra}
define check [true, forperm k: Ref, v: Int [Obl(k, v)] :: false]
\end{gobra}
Without going into details, this \texttt{check} assertion, when used as a precondition, behaves as a frame check and makes sure that the function caller passes all obligations in its scope to the callee. When used as a postcondition, it behaves as a leak check and makes sure that the function callee returns all obligations in its scope to the caller.
Now that all obligations are always available in the current context, we could check the version of all existing obligations upon incrementing the session's version, with a similar \texttt{forperm} expression.

Therefore, using frame and leak checks, we provide a simple way to implement obligations in Gobra to ultimately implement a deletion mechanism.
Note that this mechanism, given for the sake of simplicity, is not optimal yet. Indeed, it requires passing all obligations in scope, even when calling a function that does not need to read them, which can be a verification burden for the developer.
The approach could be improved by allowing framing obligations around a function call in the case that the callee and all transitively called callees do not increment the version.