This repository implements a tool to verify that patches are assured up to trace equivalence (PATE).
The goal is to prove that security patches applied to binaries only remove bad behaviors, or otherwise characterize them precisely for the developer of the patch. The verifier supports PowerPC and AArch32 binaries (currently requiring statically linked ELF binaries).
The fastest way to get started is to build the Docker image and use the tool via Docker. For more in-depth build instructions, see the Development section, below.
First, build the Docker image with the command:
docker build --platform linux/amd64 . -t pate
Next, run the verifier on an example:
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
The verifier accepts the following command line arguments:
-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
--always-classify-return Always resolve classifier failures by assuming
function returns, if possible.
The quick start section described a command to run the verifier on a test case using the Docker container. This section will cover some useful commands for other scenarios.
If you have a tar file of a Docker image of the verifier, you can install it using the command:
docker load -i /path/to/pate.tar
To run the verifier via Docker after this:
docker run --rm -it --platform linux/amd64 pate --help
To make use of the verifier with Docker, it is useful to map a directory on your local filesystem into the Docker container to be able to save output files. Assuming that your original and patched binaries are original.exe and patched.exe, respectively:
mkdir VerifierData
cp original.exe patched.exe VerifierData/
docker run --rm -it --platform linux/amd64 \
-v `pwd`/VerifierData`:/VerifierData pate \
--original /VerifierData/original.exe \
--patched /VerifierData/patched.exe \
--proof-summary-json /VerifierData/report.json \
--log-file /VerifierData/pate.log \
--save-macaw-cfgs /VerifierData/cfgs
This command will run the verifier on the two binaries and drop you into a read-eval-print loop, where you can interactively explore the verifier's output.
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).
While it is unsound, it is sometimes useful to treat a function call as a no-op. For example, ignoring large functions that have not changed and are unlikely to have an effect on correctness (e.g., large cryptographic functions from trusted libraries) can significantly improve performance. To use this feature, pass a configuration file to the verifier using the --blockinfo option, ensuring that the configuration file includes the following directives:
ignore-original-functions = [ <ADDRESS>, ... ] ignore-patched-functions = [ <ADDRESS>, ... ]
where each of the lists is a list of addresses of functions to ignore. While the two lists are specified separately, they should almost certainly be "aligned" between the two binaries (i.e., ignoring a function in the original binary probably means that the corresponding function in the patched binary also needs to be ignored).
The verifier benefits from DWARF metadata in two ways:
- It improves code discovery by identifying function entry points that the verifier could otherwise miss
- It improves some diagnostics where references to machine state can be rendered as references to named program constructs, with names provided by DWARF
To inject DWARF metadata into binaries without it (e.g., stripped binaries), we recommend using the dwarf-writer tool. As an example of using dwarf-writer through its Docker image assuming the existence of a target (target-binary.exe) and metadata in the Anvill JSON format (target-binary.exe.json):
docker load -i dwarf-writer-docker.tar
mkdir DwarfWriterData
cp target-binary.exe target-binary.exe.json DwarfWriterData/
docker run --rm -it -v `pwd`/DwarfWriterData:/DwarfWriterData dwarf-writer \
--anvill /DwarfWriterData/target-binary.exe.json \
/DwarfWriterData/target-binary.exe \
/DwarfWriterData/target-binary-dwarf.exe
This will produce a version of the binary annotated with DWARF metadata in DwarfWriterData/target-binary-dwarf.exe.
If you have the llvm-dwarfdump tool, you can use it to inspect the generated DWARF metadata. The pate verifier will automatically take advantage of DWARF metadata hints unless it is directed to ignore them.
The verifier takes two binaries as input: an original binary and a patched binary. The assumption is that some security-oriented patch has been applied to the original binary that largely preserves its behavior, but may fix some undesirable behaviors. The verifier then attempts to prove that the two binaries exhibit the same observable behavior; if it cannot, it produces a differential summary that describes the conditions under which the patched binary exhibits different behavior from the original. This enables patch developers to understand the impact of their patches on the program semantics and evaluate if the impact is restricted to the execution paths that they intended.
The verifier does not require a manually-provided specification from users; instead, it treats the original program as the desired behavioral specification. This arrangement makes pate a relational verifier, as it relates the patched binary to the original. The verifier is based on a number of existing libraries for binary code discovery and symbolic execution of programs (including machine code programs). Roughly, the verifier works by:
- Performing code discovery on both binaries
- Breaking the binaries into slices, which are collections of basic blocks with control flow between them, but without backedges; it also breaks regions at function call boundaries
- It aligns slices based on control flow and under the heuristic assumption that machine states will be similar after each pair of corresponding slices in the original and patched binaries
- It infers frame conditions (in the form of pre- and post- conditions) for each slice that are sufficient to prove that the original slice has the same behavior as the patched slice
- It attempts to verify that all of the slice pairs satisfy their frame conditions by symbolically executing both slices on the same inputs (under the set of inferred preconditions) and verifying that the patched program satisfies its required inferred postcondition
- If a pair of slices fails to satisfy the frame condition, it computes a differential summary describing the conditions under which they exhibit different behaviors
- ghc (9.6 suggested)
- cabal
- yices
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
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.
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.