To view the man page:
$ bap wp --help
--func=<function_name>— Determines which function to verify. WP verifies a single function, though calling it on the
mainfunction along with the
inlineoption will analyze the whole program. If no function is specified or the function cannot be found in the binary/binaries, WP will exit with an error message.
--inline=<posix-regexp>— Functions specified by the provided POSIX regular expression will inlined. When functions are not inlined, heuristic function summaries are used at function call sites. For example, if you want to inline the functions
bar, you can write
--inline=foo|bar. To inline everything, use
--inline=.*(not generally recommended).
--pointer-reg-list=<reg-list>— This flag specifies a comma delimited list of input registers to be treated as pointers at the start of program execution. This means that these registers are restricted in value to point to memory known to be initialized at the start of the function. For example,
RSI,RDIwould specify that
RDI's values should be restricted to initialized memory at the start of execution.
--num-unroll=<num>— Specifies the number of times to unroll each loop. WP will unroll each loop 5 times by default.
--gdb-output=<filename.gdb>— When WP results in SAT, outputs a
gdbscript to file
filename.gdb. From within
source filename.gdbto set a breakpoint at the function given by
--funcand fill the appropriate registers with the values found in the countermodel. In the case WP returns UNSAT or UNKNOWN, no script will be outputted.
--bildb-output=<filename.yml>— When WP results in SAT, outputs a BILDB initialization script to file
filename.yml. This YAML file sets the registers and memory to the values found in the countermodel, allowing BILDB to follow the same execution trace. In the case the analysis returns UNSAT or UNKNOWN, no script will be outputted.
--use-fun-input-regs— At a function call site, uses all possible input registers as arguments to a function symbol generated for an output register. If this flag is not present, no registers will be used.
--stack-base=<address>— Sets the location of the stack frame for the function under analysis. By default, WP assumes the stack frame for the current function is between
--stack-size=<size>— Sets the size of the stack.
sizeshould be denoted in bytes. By default, the size of the stack is
0x800000, which is 8MB.
--ext-solver-path=</bin/boolector>— Allows the usage of an external SMT solver. This option has only been tested with Boolector version 3.2.1. For other solvers, results may vary.
--show=[bir|refuted-goals|paths|precond-internal|precond-smtlib]— A list of details to print out from the analysis. Multiple options can be specified as a comma-separated list. For example:
--show=bir,refuted-goals. The options are:
bir: The code of the binary/binaries in BAP Intermediate Representation.
refuted-goals: In the case WP results in SAT, a list of goals refuted in the model that contains their tagged names, their concrete values, and their Z3 representation.
paths: The execution path of the binary that results in a refuted goal. The path contains information about the jumps taken, their addresses, and the values of the registers at each jump. This option automatically prints out the refuted goals.
precond-smtlib: The precondition printed out in Z3's SMT-LIB2 format.
precond-internal: The precondition printed out in WP's internal format for the
--debug=[z3-solver-stats|z3-verbose|constraint-stats|eval-constraint-stats]— A list of debugging statistics to display. Multiple statistics may be specified in a comma-separated list. For example:
--debug=z3-solver-stats,z3-verbose. The options are:
z3-solver-stats: Information and statistics about Z3's solver. It includes information such as the maximum amount of memory used and the number of allocations.
z3-verbose: Z3's verbosity level. It outputs information such as the tactics the Z3 solver used.
constraint-stats: Statistics regarding the internal
Constr.tdata structure, including the number of goals, ITEs, clauses, and substitutions.
eval-constraint-stats: Statistics regarding the internal expression lists during evaluation of the
--user-func-specs=<user-spec-list>— List of user-defined subroutine specifications. For each subroutine, it creates the weakest precondition given the name of the subroutine and its pre and post-conditions. Usage:
--user-func-specs="<sub name>,<precondition>,<postcondition>". For example,
--user-func-specs="foo,(assert (= RAX RDI)),(assert (= RAX init_RDI))"means "for subroutine named foo, specify that its precondition is
RAX = RDIand its postcondition is
RAX = init_RDI". Multiple subroutine specifications are delimited with ';'s, i.e.:
--user-func-specs="foo,(assert (= RAX RDI)),(assert (= RAX init_RDI));bar,(assert (= RAX RDI)),(assert (= RAX init_RDI))".
--fun-specs=<spec-list>— List of built-in function summaries to be used at a function call site in order of precedence. A target function will be mapped to a function spec if it fulfills the spec's requirements. All function specs set the target function as called and update the stack pointer. The default specs set are verifier-assume, varifier-nondet, empty, and chaos-caller-saved. Note that if a function is set to be inlined, it will not use any of the following function specs. Available built-in specs:
verifier-error: Used for calls to
__assert_fail. Looks for inputs that would cause execution to reach these functions.
verifier-assume: Used for calls to
__VERIFIER_assume. Adds an assumption to the precondition based on the argument to the function call.
verifier-nondet: Used for calls to nondeterministic functions such as
malloc. Chaoses the output to the function call representing an arbitrary pointer.
afl-maybe-log: Used for calls to
__afl_maybe_log. Chaoses the registers RAX, RCX, and RDX.
arg-terms: Used when BAP's uplifter returns a nonempty list of input and output registers for the target function. Chaoses this list of output registers.
chaos-caller-saved: Used for the x86 architecture. Chaoses the caller-saved registers.
rax-out: Chaos RAX if it can be found on the left-hand side of an assignment in the target function.
chaos-rax: Chaos RAX regardless if it has been used on the left-hand side of an assignment in the target function.
empty: Used for empty subroutines. Performs no actions.
To analyze a single program, the command you want to invoke has this basic form:
$ bap wp \ <-- The command is wp --func=FUNC \ <-- The function to examine [options] \ <-- Any extra options /path/to/exe <-- The path to a binary programThe following options select or adjust the property that will be checked for the function
FUNCin the case of single-program analysis.
--trip-asserts— Looks for inputs to the subroutine that would cause an
__VERIFIER_errorto be reached.
--check-null-derefs— Checks for inputs that would result in dereferencing a NULL address during a memory read or write. This flag can also be used in comparative analysis; see below.
--precond=<smt-lib-string>— Allows you to specify an assertion that WP will assume is true at the beginning of the function it is analyzing. Assertions are specified in the smt-lib2 format. If no precondition is specified, a trivial precondition of
truewill be used. This flag can also be used in comparative analysis; see below.
--postcond=<smt-lib-string>— Allows you to specify an assertion that WP will assume is true at the end of the function it is analyzing, using the smt-lib2 format. If no postcondition is specified, a trivial postcondition of
truewill be used. This flag can also be used in comparative analysis; see below.
(((address <addr>) (invariant <smtlib>)) (...)). Assumes the subroutine contains unnested while loops with one entry point and one exit each. Checks the loop invariant written in smt-lib2 format for the loop with its header at the given address. The address should be written in BAP's bitvector string format. Only supported for a single binary analysis.
To analyze two programs,the command you want to invoke has this basic form:
$ bap wp \ <-- The command is wp --func=FUNC \ <-- The function to examine in both programs [options] \ <-- Any extra options /path/to/exe1 \ <-- The path to the first program /path/to/exe2 <-- The path to the second program
--check-null-derefs— Checks that the modified binary has no additional paths with null dereferences in comparison with the original binary.
--check-invalid-derefs— Checks that the modified binary has no additional paths that result in dereferences to invalid memory locations. That is, all memory dereferences are either on the stack or heap. The stack is defined as the memory region above the current stack pointer, and the heap is defined as the memory region 0x256 bytes below the lowest address of the stack.
--compare-func-calls— Checks that function calls do not occur in the modified binary if they have not occurred in the original binary.
--compare-post-reg-values=<reg-list>— Compares the values stored in the registers specified in
reg-listat the end of the function's execution. For example,
RAX,RDIcompares the values of RAX and RDI at the end of execution. If unsure about which registers to compare, check the architecture's ABI. x86_64 architectures place their output in RAX and ARM architectures place their output in R0.
--mem-offset— Maps the symbols in the data and bss sections from their addresses in the original binary to their addresses in the modified binary. If this flag is not present, WP assumes that memory between both binaries start at the same offsets.
--rewrite-addresses— This flag is only used in a comparative analysis. Rewrites the concrete addresses in the modified binary to the same address in the original binary if they point to the same symbol. This flag should not be used in conjunction with the
--precond=<smt-lib-string>— Allows you to specify an assertion that WP will assume is true at the beginning of the function it is analyzing, using the smt-lib2 format. For comparative predicates, one may refer to variables in the original and modified programs by appending the suffix
_modto variable names in the smt-lib expression. For example,
--precond="(assert (= RDI_mod #x0000000000000003)) (assert (= RDI_orig #x0000000000000003))". If no precondition is specified, a trivial precondition of
truewill be used.
--postcond=<smt-lib-string>— Allows you to specify an assertion that WP will assume is true at the end of the function it is analyzing, using the smt-lib2 format. Similar to
--precond, one may create comparative postconditions on variables by appending
_modto variable names. If no postcondition is specified, a trivial postcondition of
truewill be used.
--func-name-map=<regex-orig>,<regex-mod>— Maps the subroutine names from the original binary to their names in the modified binary based on the regex from the user. Usage:
--func-name-map="<regex for original name>,<regex for modified name>".For example:
--func-name-map="\(.*\),foo_\1"means that all subroutines in the original binary have foo_ prepended in the modified binary. Multiple patterns can be used to map function names and are delimited with ';'s (i.e.
<reg1_orig>,<reg1_mod>;<reg2_orig>,<reg2_mod>"). By default, WP assumes subroutines have the same names between the two binaries.
smt-lib2format. Here we provide a quick reference to commonly used features. In the following, let
E2, and so on refer to
(and E1 E2)
(or E1 E2)
(=> E1 E2)
(= E1 E2)
(not (= E1 E2))
(+ E1 E2)
(- E1 E2)
(* E1 E2)
(< E1 E2)
(<= E1 E2)
(> E1 E2)
(>= E1 E2)
(bvadd E1 E2)
(bvsub E1 E2)
(bvult E1 E2)
(bvule E1 E2)
(bvugt E1 E2)
(bvuge E1 E2)
(bvslt E1 E2)
(bvsle E1 E2)
(bvsgt E1 E2)
(bvsge E1 E2)