
\section{Invoking the \pate{} Verifier}
\label{sec:run-pate-verif}

Once \pate{} has been built as described in Section~\ref{sec:build-pate-verif}, use the Docker container (or \texttt{pate.sh} script if building locally from source) to invoke \pate{}.

Invoking \pate{} presents the user with an interactive terminal user interface for analyzing a pair of binaries.
Users provide at least the paths to two (the ``original'' and ``patched'') binaries at the command line when invoking \pate{}.
Additionally, we recommend also specifying the desired entry point, using \texttt{-s <symbol>}.
Providing the specific function of interest will enable \pate{} to begin reasoning closer to the relevant functionality of interest, greatly reducing the total analysis time required compared to starting from the program entry point.
An example invocation using Docker looks like:

\begin{verbatim}
  docker run --rm -it \
    --platform linux/amd64 \
    -v "$(pwd)"/z:/z \
    pate \
    --original /z/my.original.exe \
    --patched /z/my.patched.exe \
    -s start_function_name
\end{verbatim}

Users may also wish to provide ``hint'' inputs that provide metadata that maps symbol names to addresses, easing analysis of stripped binaries.
Please see the listing below for details.

The verifier accepts the following command line arguments:
\begin{verbatim}
  -h,--help                Show this help text
  -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
  -d,--nodiscovery         Don't dynamically discover function pairs based on
                           calls.
  --solver ARG             The SMT solver to use to solve verification
                           conditions. One of CVC4, Yices, or Z3
                           (default: Yices)
  --goal-timeout ARG       The timeout for verifying individual goals in seconds
                           (default: 300)
  --heuristic-timeout ARG  The timeout for verifying heuristic goals in seconds
                           (default: 10)
  --original-anvill-hints ARG
                           Parse an Anvill specification for code discovery
                           hints
  --patched-anvill-hints ARG
                           Parse an Anvill specification for code discovery
                           hints
  --original-probabilistic-hints ARG
                           Parse a JSON file containing probabilistic function
                           name/address hints
  --patched-probabilistic-hints ARG
                           Parse a JSON file containing probabilistic function
                           name/address hints
  --original-csv-function-hints ARG
                           Parse a CSV file containing function name/address
                           hints
  --patched-csv-function-hints ARG
                           Parse a CSV file containing function name/address
                           hints
  --original-bsi-hints ARG Parse a JSON file containing function name/address
                           hints
  --patched-bsi-hints ARG  Parse a JSON file containing function name/address
                           hints
  --no-dwarf-hints         Do not extract metadata from the DWARF information in
                           the binaries
  -V,--verbosity ARG       The verbosity of logging output (default: Info)
  --save-macaw-cfgs DIR    Save macaw CFGs to the provided directory
  --solver-interaction-file FILE
                           Save interactions with the SMT solver during symbolic
                           execution to this file
  --proof-summary-json FILE
                           A file to save interesting proof results to in JSON
                           format
  --log-file FILE          A file to save debug logs to
  -e,--errormode ARG       Verifier error handling mode
                           (default: ThrowOnAnyFailure)
  -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
  --assume-stack-scope     Add additional assumptions about stack frame 
                           scoping during function calls (unsafe)
  --ignore-warnings ARG    Don't raise any of the given warning types
\end{verbatim}

\subsection{--assume-stack-scope}

This flag causes \pate{} to assume that out-of-scope stack slots 
(i.e. slots that are past the current stack pointer) are always equal between
the two binaries.
Although in actuality they may have differing out-of-scope stack
contents, programs that exercise proper stack hygiene should never
access those values. By assuming they are equal, \pate{} avoids 
creating spurious counter-examples where under-specified pointers
alias inequivalent, but out-of-scope, stack slots.
This is a fairly strong assumption that can have unintended side-effects,
including assuming \emph{false} when out-of-scope stack contents are
\emph{provably} inequivalent.


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "user-manual"
%%% End:
