5_conclusion.tex

\chapter{Conclusion}
\label{chap:conclusion}

% Recap what we have designed and implemented, and the core idea
In conclusion, this thesis has successfully extended the methodology developed by Arquint et al.~\cite{ArquintSchwerhoffMehtaMueller23} for the modular verification of security protocol implementations, adding support for the specification of time-sensitive data and enforcing their secure deletion at the end of their lifetime.
To the best of our knowledge, our contributions enable for the first time the verification of strong security properties relying on the secure deletion of sensitive data for real-world protocol implementations.
By building upon standard separation logic predicates, the extended methodology remains agnostic to programming languages.

The generic extension we introduced is flexible enough to verify various protocol implementations that use ephemeral data, such as Signal~\cite{marlinspike2016x3dh} and its key rotation scheme. Our methodology can be used to prove strong security properties like forward secrecy and post-compromise security.

Furthermore, we have extended the Reusable Verification Library~\cite{ArquintSchwerhoffMehtaMueller23} for Go to contain our methodology.
Using a solution inspired by counting permissions~\cite{roshardt2021extending}, we provide the library with the ability to track sensitive values in a protocol implementation and ensure that they are deleted in a timely manner.
By implementing this solution in several functions of the library, we facilitate the work of the developer by ensuring in a sound way that the values they create can only exist during the periods of time specified for these values.

% Explain how the case study shows that our methodology works
We evaluate our methodology with a case study on a Signal-like protocol implementation.
This case study shows that our extended methodology is expressive enough to reason about complex mechanisms such as key ratcheting.
While the full security proof could not be completed for time reasons, we provide a clear path toward its completion in this thesis.
% in which we showcase how we can use our methodology and its implementation in the Go library.
% This case study explains how we can apply our methodology and reason about some non-trivial technical concepts found in protocol implementations such as key ratcheting.
% We conclude this case study by providing a clear path toward verifying forward secrecy and post-compromise security for this protocol implementation.

In the next and final section, we propose some ideas for future work that could improve or extend this thesis.

\section{Future work}
\label{sec:future-work}
% Future work:
%   - Finish the case study?
%   - Change AEAD methodology to support verification of the DH Ratchet
%   - Implement obligations in Gobra

\paragraph{Finishing the case study.}
The case study presented in chapter~\ref{chap:case-study} could be completed by following the path we have outlined in section~\ref{sec:remaining-work}, resulting in the verification of forward secrecy and post-compromise security for this protocol implementation.

\paragraph{Adding obligation support to Gobra.}
As discussed in detail in section~\ref{sec:alternative-design-using-obligations}, adding obligations~\cite{bostrom2014modular} to Gobra~\cite{wolf2021gobra} would allow us to implement a simpler and more elegant solution for tracking sensitive values.
This may result in a more intuitive methodology and simpler specification for library functions that developers can use more easily.

\paragraph{Improving how the methodology handles AEAD.}
When choosing the protocol to verify for our case study, in section~\ref{sec:chosen-protocol}, we had to slightly adapt the original Diffie-Hellman ratchet protocol to make it more easily verifiable.
The reason for this comes from how the current methodology handles AEAD decryption, which hinders our ability to decrypt the message using a key that is derived from the associated data we just received.
In future work, we could analyze how ratcheting protocols use associated data before computing the necessary decryption key.
In particular, we should reconsider the preconditions and postconditions of the AEAD decryption function such that we can invoke this function in these situations and soundly obtain the associated message invariant unless the ciphertext has been created by the attacker.