Update user manual

README.rst

@@ -14,9 +14,9 @@ First, build the Docker image with the command::
 
   docker build . -t pate
 
-Next, run the verifier on an example from the test suite::
+Next, run the verifier on an example::
 
-  docker run --rm -it -p 5000:5000 -v `pwd`/tests:/tests pate --original /tests/aarch32/const-args.original.exe --patched /tests/aarch32/const-args.patched.exe
+  docker run --rm -it --platform linux/amd64 -v "$(pwd)"/tests/integration/packet/exe:/target pate --original /target/packet.exe --patched /target/packet.patched.exe -s parse_packet
 
 
 Command Line Options
@@ -28,8 +28,7 @@ The verifier accepts the following command line arguments::
   -o,--original EXE        Original binary
   -p,--patched EXE         Patched binary
   -b,--blockinfo FILENAME  Block information relating binaries
-  -s,--startsymbol ARG     Start analysis from the function with this symbol,
-                           otherwise start at the program entrypoint
+  -s,--startsymbol ARG     Start analysis from the function with this symbol
   -d,--nodiscovery         Don't dynamically discover function pairs based on
                            calls.
   --solver ARG             The SMT solver to use to solve verification
@@ -77,6 +76,22 @@ The verifier accepts the following command line arguments::
   -r,--rescopemode ARG     Variable rescoping failure handling mode
                            (default: ThrowOnEqRescopeFailure)
   --skip-unnamed-functions Skip analysis of functions without symbols
+  --skip-divergent-control-flow
+                           <DEPRECATED>
+  --target-equiv-regs ARG  Compute an equivalence condition sufficient to
+                           establish equality on the given registers after the
+                           toplevel entrypoint returns. <DEPRECATED>
+  --ignore-segments ARG    Skip segments (0-indexed) when loading ELF
+  --json-toplevel          Run toplevel in JSON-output mode (interactive mode
+                           only)
+  --read-only-segments ARG Mark segments as read-only (0-indexed) when loading
+                           ELF
+  --script FILENAME        Save macaw CFGs to the provided directory
+  --no-assume-stack-scope  Don't add additional assumptions about stack frame
+                           scoping
+  --ignore-warnings ARG    Don't raise any of the given warning types
+  --always-classify-return Always resolve classifier failures by assuming
+                           function returns, if possible.
 
 Extended Examples
 -----------------
@@ -115,14 +130,7 @@ Controlling the Verifier Entry Point
 
 By default, the verifier starts verifying from the formal program entry point. This is often not very useful (and can be problematic for complex binaries with a large ``_start`` that causes problem for our code discovery).  Additionally, for changes with a known (or at least expected) scope of impact, analyzing just the affected functions is significantly faster. To instead specify an analysis entry point, passing the ``-s <function_symbol>`` option will start the analysis
 from the function corresponding to the given symbol. Note that this requires function symbols to be provided for the binaries (either as embedded debug
-symbols or separately in one of the hint formats)::
-
-  docker run --rm -it -v `pwd`/tests:/tests/hints pate \
-             --original /tests/01.elf \
-             --patched /tests/01.elf \
-             --original-anvill-hints /tests/01.anvill.json \
-             --patched-anvill-hints /tests/01.anvill.json \
-             -s main
+symbols or separately in one of the hint formats).
 
 Treating Functions As No-Ops
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@@ -176,23 +184,23 @@ Development
 Requirements
 ------------
 
-- ghc (8.10.4 suggested)
+- ghc (9.6 suggested)
 - cabal
 - yices
 
 Build Steps
 -----------
 
-The pate tool is written in Haskell and requires the GHC compiler (version 8.6-8.10) and the cabal build tool to compile.  Building from source can be accomplished by::
+The pate tool is written in Haskell and requires the GHC compiler (we test with 9.6) and the cabal build tool to compile.  Building from source can be accomplished by::
 
   git clone [email protected]:GaloisInc/pate.git
   cd pate
   git submodule update --init
   cp cabal.project.dist cabal.project
   cabal configure pkg:pate
-  pate.sh --help
+  ./pate.sh --help
 
-The verifier requires an SMT solver to be available in ``PATH``. The default is ``yices``, but ``z3`` and ``cvc4`` are also supported.
+The verifier requires an SMT solver to be available in ``PATH``. The default is ``yices`` - ``z3`` and ``cvc4`` may also work but are not regularly tested with PATE.
 
 Acknowledgements
 ============

docs/user-manual/ack.tex

@@ -1,11 +1,20 @@
-\section{Acknowledgement}
-
-This material is based upon work supported by the Defense Advanced
-Research Projects Agency (DARPA) and Naval Information Warfare Center
-Pacific (NIWC Pacific) under Contract Number N66001-20-C-4027. Any
-opinions, findings and conclusions or recommendations expressed in this
-material are those of the author(s) and do not necessarily reflect the
-views of the DARPA \& NIWC Pacific. 
+\section{Acknowledgements}
+
+This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) and Naval Information Warfare Center Pacific (NIWC Pacific) under Contract Number N66001-20-C-4027.
+Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the DARPA \& NIWC Pacific.
+
+\subsection*{SBIR DATA RIGHTS}
+
+\begin{description}
+\item[Contract No] 140D0423C0063
+\item[Contractor Name] Galois, Inc.
+\item[Contractor Address] 421 SW Sixth Ave., Suite 300, Portland, OR 97204
+\item[Expiration of SBIR Data Protection Period] 06/07/2042
+\end{description}
+
+The Government's rights to use, modify, reproduce, release, perform, display, or disclose technical data or computer software marked with this legend are restricted during the period shown as provided in paragraph (b)(5) of the Rights in Noncommercial Technical Data and Computer Software-Small Business Innovation Research (SBIR) Program clause contained in the above identified contract.
+After the expiration date shown above, the Government has perpetual government purpose rights as provided in paragraph (b)(5) of that clause.
+Any reproduction of technical data, computer software, or portions thereof marked with this legend must also reproduce the markings.
 
 %%% Local Variables:
 %%% mode: latex

docs/user-manual/binary-ninja-ui.tex

@@ -0,0 +1,131 @@
+\section{The \pate{} Binary Ninja Plugin}
+\label{sec:binary-ninja-ui}
+
+The \pate{} Binary Ninja plugin enables user to invoke and interact with \pate{} directly within the Binary Ninja reverse engineering platform.
+
+The \pate{} plugin requires a commercially-licensed Binary Ninja installation.
+We have tested \pate{} with Binary Ninja stable version 4.0.5336.
+
+\subsection{Installation}
+
+First, install the \pate{} Docker container as described in Section~\ref{sec:build-pate-verif}.
+
+Second, copy (or create a symlink from) the \texttt{pate\_binja/} directory from the \pate{} source repo to your local Binary Ninja \texttt{plugins/} directory. Typically these are found in:
+\begin{description}
+\item[macOS] \texttt{\$HOME/Library/Application Support/Binary Ninja/plugins/}
+\item[Linux] \texttt{\$HOME/.binaryninja/plugins/}
+\end{description}
+
+The Binary Ninja plugin requires a relatively recent version of Python (3.10 or newer) and requires the \texttt{grpcio} package.
+If these are not present on the system, we recommend creating a Python \texttt{venv} or similar on your host, with something like:
+
+\begin{verbatim}
+  python -m venv /path/to/new/virtual/environment
+  source /path/to/new/virtual/environment/bin/activate
+  pip install grpcio
+\end{verbatim}
+
+and then modifying Binary Ninja Python settings appropriately in the Binary Ninja Preferences list to point to this new environment.
+Specifically, check the settings for:
+
+\begin{itemize}
+    \item Python Path Override
+    \item Python Interpreter
+    \item Python Virtual Environment Site-Packages
+\end{itemize}
+
+Once these steps have been completed, restart Binary Ninja.
+If the plugin is correctly installed and initialized, then the ``Plugins'' menu will now have a ``Pate...'' menu option.
+
+\subsection{Usage}
+
+In Section~\ref{sec:terminal-ui} we examined the \texttt{packet.exe} example using the \pate{} terminal UI.
+In this section, we describe analyzing the same example using the \pate{} Binary Ninja plugin.
+
+\begin{figure}[h]
+  \centering
+  \includegraphics[width=\textwidth]{pate-binja-overview.png}
+  \caption{The PATE Binary Ninja Plugin. The top region is the PATE analysis overview graph. The bottom panel is used by the operator to interact with the PATE verifier.}
+  \label{fig:overview}
+\end{figure}
+
+Once installed, invoke the \pate{} plugin from the Binary Ninja ``Plugins $\rightarrow$ Pate...'' menu option.
+
+The \pate{} plugin opens a window to select a \emph{run configuration} file in JSON format.
+This file must end in the suffix \texttt{.run-config.json}.
+The run configuration must contain a key-value map with the following keys:
+\begin{description}
+    \item[\texttt{original}] (absolute or relative) file path to the original binary
+    \item[\texttt{patched}] (absolute or relative) file path to the patched binary
+    \item[\texttt{args}] a list additional arguments to pass to \pate{}
+\end{description}
+
+For example, the file \texttt{tests/integration/packet/packet.run-config.json} contains:
+
+\begin{verbatim}
+  {
+    "original": "exe/packet.original.exe",
+    "patched": "exe/packet.patched.exe",
+    "args": [
+      "-s parse_packet"
+    ]
+  }
+\end{verbatim}
+
+After selecting the run configuration file, the \pate{} plugin will open three Binary Ninja tabs: one for each of the original and patched binaries, and a third \emph{\pate{} analysis} tab.
+
+As shown in Figure~\ref{fig:overview}, the \pate{} analysis tab is composed of two primary regions.
+The bottom portion is an interactive text view that corresponds to the terminal user interface.
+The user interacts with this region through the text input field at the bottom of the window.
+In the \texttt{packet.exe} example, the user enters the same commands described in Section~\ref{sec:terminal-ui} through the \texttt{Finish and view final result} step, at which point results will be rendered in the interactive Binary Ninja view.
+
+The top portion of the \pate{} analysis tab is a graph view showing the current state of the \pate{} analysis.
+When \pate{} analysis is complete (via interaction in the bottom portion), the \pate{} graph shows rectangles for each slice of the program analyzed by \pate{}.
+Default-colored rectangles represent a pair of programs slices that were able to matched up between the original and patched binary.
+Green rectangles represent slices present only in the original program, if any.
+Blue rectangles represent slices present only in the patched program, if any.
+Right click on a rectangle for options to jump directly to the relevant program location in the appropriate tab for the corresponding binary.
+
+A red rectangle represents the ``active'' region, where \pate{} has found an equivalence condition.
+Right click and select ``Show Equivalence Condition'' to open the Equivalence Condition window.
+Please see Figure~\ref{fig:equiv-cond} for an example screenshot of the equivalence condition window in the PATE Binary Ninja plugin.
+An equivalence condition window includes:
+
+\begin{itemize}
+    \item the expression describing the conditions under which programs behave equivalently
+    \item a generated (concretized) trace through the program(s) showing an example where the equivalence condition is met
+    \item a generated (concretized) trace through the program(s) showing an example where the equivalence condition is \emph{not} met
+\end{itemize}
+
+\begin{figure}[h]
+  \centering
+  \includegraphics[width=\textwidth]{pate-binja-equiv-cond.png}
+  \caption{The PATE Binary Ninja plugin equivalence condition window.}
+  \label{fig:equiv-cond}
+\end{figure}
+
+Right clicking on a rectangle in the \pate{} analysis graph and selecting ``Show Instruction Trees'' will open a new window showing basic blocks from the original program on the left and corresponding basic blocks from the patched program on the right.
+At the bottom will be a linearized representation of the instruction trees in the original and patched program, with colorized diff view.
+Instructions conditionally reachable through conditional control flow edges (if any) are prefixed by \texttt{+} or \texttt{-} to differentiate instructions in distinct branches.
+See Figure~\ref{fig:mcad} for an example of the instruction tree view, with MCAD integration (described below).
+
+\subsection{Replays}
+
+Executing a run configuration file with the \pate{} plugin will produce a \emph{replay} in a file named \texttt{lastrun.replay}, which can be preserved by renaming to another filename on disk.
+These files cache the user input and verifier output, enabling the user to load a previous interaction with \pate{} without having to re-execute the verifier analysis.
+If the user loads a replay rather than a run configuration, the process is mostly the same, except the command input field is already populated with the recorded user input, and the user just hits ``enter'' to proceed to the next step.
+Editing the input commands will have no effect, as the responses are recorded in the replay file.
+That is, the user cannot deviate from the pre-recorded responses from the \pate{} verifier to perform any analysis other than the one recorded.
+
+\subsection{MCAD Integration}
+
+MCAD\footnote{\url{https://github.com/securesystemslab/LLVM-MCA-Daemon}} is a performance analysis tool that performs static prediction of instruction timings for sequences of instructions such as those identified by \pate{}.
+The details of the MCAD system is outside of the scope of this user guide, but if the MCAD Docker container is available, the \pate{} Binary Ninja plugin will show MCAD-predicted cycle counts next to each instruction in the Instruction Trees view, as shown in Figure~\ref{fig:mcad}.
+Use the \pate{} plugin preference option ``MCAD Docker image name'' to specify the name of the MCAD Docker container on the host in order to enable MCAD integration in the \pate{} plugin.
+
+\begin{figure}[h]
+  \centering
+  \includegraphics[width=\textwidth]{pate-binja-mcad.png}
+  \caption{PATE Binary Ninja MCAD integration showing predicted cycle counts (per instruction, cumulative) for instructions in original (left) and patched (right) basic blocks.}
+  \label{fig:mcad}
+\end{figure}

docs/user-manual/build.tex

@@ -1,31 +1,64 @@
-
-\section{Building the PATE Verifier}
+\section{Installing the \pate{} Verifier}
 \label{sec:build-pate-verif}
 
-The pate tool is written in Haskell and requires the GHC compiler
-(version 8.6-8.10) and the cabal build tool to compile.  Building from
-source can be accomplished as follows:
+\subsection{Recommended: Docker Container Image}
+
+We recommending using \pate{} via Docker.
+
+If available, load the Docker image file from a file using:
+\begin{verbatim}
+  docker load -i /path/to/pate.tar
+\end{verbatim}
+
+Otherwise, build the Docker image from the \pate{} source repo.
+Building \pate{} is a memory-intensive process.
+We build the Docker image in an environment with 16GB of RAM available to Docker.
+Build the image using the following commands:
+
 \begin{verbatim}
   git clone [email protected]:GaloisInc/pate.git
   cd pate
   git submodule update --init
-  cp cabal.project.dist cabal.project
-  cabal configure pkg:pate
-  pate.sh --help
+  docker build . -t pate
 \end{verbatim}
-The verifier also requires an SMT solver to be available in
-``PATH``. The default is ``yices``, but ``z3`` and ``cvc4`` are also
-supported.   The verifier can also be built as a Docker image:
+
+\pate{} may subsequently be used via Docker, such as:
+
 \begin{verbatim}
-  docker build . -t pate
+  docker run --rm -it \
+    --platform linux/amd64 \
+    -v "$(pwd)"/tests/integration/packet/exe:/target \
+    pate \
+    --original /target/packet.exe \
+    --patched /target/packet.patched.exe \
+    -s parse_packet
 \end{verbatim}
-The correctness of the build can be confirmed by
+
+Please see later sections for detailed usage information.
+
+\subsection{Alternative: Building from Source}
+
+Alternatively, \pate{} may be compiled from source and run on a host system.
+The \pate{} tool is written in Haskell and requires the GHC compiler\footnote{\url{https://www.haskell.org/ghc/}} and cabal\footnote{\url{https://www.haskell.org/cabal/}} to build.
+
+The current version of \pate{} is developed using GHC version 9.6.2 and cabal version 3.10.2.0.
+Additionally, the verifier requires a SMT solver to be available in \texttt{PATH}.
+We recommend \texttt{yices}.
+The \texttt{z3} and \texttt{cvc4} solvers may also work but are not regularly tested with \pate{}.
+
+Building from source can be accomplished as follows:
 \begin{verbatim}
-docker run --rm -it -p 5000:5000 -v `pwd`/tests:/tests pate \
-     --original /tests/aarch32/const-args.original.exe \
-     --patched /tests/aarch32/const-args.patched.exe
+  git clone [email protected]:GaloisInc/pate.git
+  cd pate
+  git submodule update --init
+  cp cabal.project.dist cabal.project
+  cabal configure pkg:pate
+  ./pate.sh --help
 \end{verbatim}
 
+Note that \texttt{./pate.sh} should be used to build \pate{} (not \texttt{cabal build} or similar).
+
+Once built, invoke \pate{} locally using the \texttt{pate.sh} script.
 
 %%% Local Variables:
 %%% mode: latex