\section{Introduction}\label{sec:introduction}

This User Manual describes the \pate{} verifier as of July 2024, and is maintained in the \pate{} source repository\footnote{\url{https://github.com/GaloisInc/pate}}.

The \pate{} verifier is a static relational verifier for binaries that builds assurance that micropatches have not introduced any adverse effects.
The verifier is a static relational verifier that attempts to prove that two binaries have the same observable behaviors.
When it cannot, the verifier provides detailed explanations that precisely characterize the difference in behavior between the two binaries.
After applying a micropatch to a binary, domain experts can apply the verifier to ensure that the effects are intended.

Note that while the verifier attempts to prove that the original and patched binaries have the same observable behaviors under all possible inputs, it is expected that they do not (or the patch would have had no effect).
When the two binaries can exhibit different behaviors, the verifier provides the user with an explanation of how and where the behavior is different.

If DWARF debugging information is available in either the original or patched binary, the verifier will use that information to improve diagnostics.
Currently, function names, function argument names, local variable names, and global variable names can be used to make diagnostics more readable, for example, by replacing synthetic names with their source-level counterparts.
If working with binaries that do not come with DWARF debug information natively, see the \lstinline{dwarf-writer}\footnote{\url{https://github.com/immunant/dwarf-writer}} tool for a possible approach to adding DWARF debug information.

\pate{} is designed to analyze binaries produced by applying a micropatch at the binary level where overall the pair of binaries are ``mostly'' similar.
It is more difficult for \pate{} to compare binaries with substantially different control flow due to the challenges in finding corresponding slices to align for analysis.
Major control flow divergences may require user input to guide \pate{} in its analysis process.
We have observed that in some cases, compiling two programs with similar source (such as making a small source-level modification and rebuilding) can result in binaries that are more different than the small source code change might imply, as a result of various modern compiler heuristics and optimizations.

Currently, the verifier supports 32-bit ARM binaries, and 64-bit and 32-bit PowerPC binaries.
