draperlaboratory / cbat_tools Goto Github PK

Right now, calling

bap foo --pass=wp --wp-inline=true

inlines nothing, since the wp-inline-funcs flag is not set and defaults to the empty list.

Similarly,

bap foo --pass=wp --wp-inline-funcs=foo

does not inline foo since the wp-inline flag is not set!

My feeling is that not specifying a wp-inline-funcs inlines everything rather than nothing, and that wp-inline-funcs should imply wp-inline.

Self explanatory.

In the case of a memory comparison while we are looking for a refuted goal

| Goal g ->
  let goal_val = Expr.substitute g.goal_val olds news in
  let goal_res = Option.value_exn (Z3.Model.eval model goal_val true) in
  if Bool.is_false goal_res then
  ...

is unable to determine when a memory comparison is false.

Running Bool.get_bool_value goal_res results in L_UNDEF.

Some examples of binaries to test wp on:

• zip
• sv-benchmarks
• cJSON

Improve the memory model of the BAP VSA by using CLPs as the keys rather than regular intervals. This should improve handling of items such as structs in memory. Note that the CLPs will have to be treated as regular strided intervals for the purposes of the interval tree. However, this is still a significant improvement.

Given a function call
foo(x, y, z)

Create a predicate Foo_func(x, y, z, mem, out) that represents the relationship between inputs and outputs.

This should allow us to compare subroutines with function calls, and assume that identical calls to identical subroutines should agree on their outputs.

Right now, the freshen_sub function at

The correct solution is to use the existing variable map in Env.t, and freshen those instead.

Alternately, we could save the variable substitution for subroutines in the environment and apply that before analyzing the inlined subroutine, but this is a hack.

We should have a notion of memory in WP represented as a BV64 -> bool stating that an address returns either true or false if it is in a certain region of memory. For example, the address 0x00007FFFFFFFD588 is true in the stack, and false in the heap.

We should add these types to Env.t such that:

type t = {
  stack : BV64 -> bool;
  heap : BV64 -> bool;
   ...
}

We can then define our own stacks and heaps with: Stack(x) := stack_min <= x <= stack_max and Heap(x) := heap_min <= x <= heap_max where stack_min, stack_max, heap_min, and heap_max are concrete values. There should be some buffer between stack_min and heap_max.

With this, we should have a way to compare the memory between the new binaries. We could start off by comparing the heap with ∀x. Heap(x) -> mem_orig[x] == mem_mod[x + d] and the stack with ∀x. Stack(x) -> mem_orig[x] == mem_mod[x]. These should be added to the precondition.

Lastly, we should add the constraint of Stack(SP) to the precondition to assert that the stack pointer is pointing to a valid location on the stack.

Currently in WP, we have specs for chaos-ing RAX if it used on the left hand side of a function being called.

We should add more specs that allow us to:

• always chaos RAX regardless if it was used on the left hand side of the target function
• chaos the x86 caller-saved registers

What it says on the tin.

Every time we run make, it will reinstall everything even if it has already been installed.

Currently for our comparison analysis, different postconditions are built separately in with compare_subs_eq and compare_subs_fun in https://github.com/draperlaboratory/cbat_tools/blob/master/wp/lib/bap_wp/src/compare.ml.

We should add combinator in order to build postconditions that compare multiple properties (ex: compares both the register values and the function calls), giving the user the ability to pick multiple.

We should also move all the variable computation from

As we add more features into wp, Env.t is getting more bloated. Depending on the type of analysis we are running, we do not need all of the fields in the env record such as:

A possible solution is to make env an 'a Env.t type, and have some sort of interface for the functions that relate to the these specific fields.

We should separate out the compare tests in the test_precondition.ml file to a test_compare.ml file, since the main functions we're testing comes from compare.ml.

We need to engineer a system such that we can create and check loop invariants. We have loop unrolling for now, but this is still open. We also need a way to select which loop handler to invoke, and how to tag each SCC.

Right now, the only output register we are comparing in our example is RAX. We should try comparing other registers as well.

The command bap --wp-help used to give a description of the plugin, along with the docstrings associated to the pass-specific options, which it does not do anymore.

We need to either figure out the new command, or file a bug report to get the old behavior back.

Allow the user of the WP to add a number of concrete values for the parts of the input environment, say by giving a set of pairs of expressions and values:
val visit_sub : Env.t -> Constr.t -> Bap.Std.Sub.t -> Constr.t * Env.t

becomes:

val visit_sub : Env.t -> (Exp.t * Val.t) seq -> Constr.t -> Bap.Std.Sub.t -> Constr.t * Env.t

Or maybe modify check to be able to re-run the solver with different possible values.

Alternately just separate this out into a new operation that adds constraints to the pre-condition.

• We should refactor getting a model from the solver to it's own function as there are instances of

 let model = Z3.Solver.get_model solver
              |> Option.value_exn ?here:None ?error:None ?message:None

in constraint.ml, output.ml, precondition.ml, and test_precondition.ml. We should also add a more useful error message for the failure case.

• When returning the result of SAT or UNSAT, in
  

  cbat_tools/wp/lib/bap_wp/src/precondition.ml

  Line 887 in aca7ac6

  let check ?refute:(refute = true) (solver : Z3.Solver.solver) (ctx : Z3.context)

  
  we should return either UNSAT or SAT with a model atomically, possibly by creating our own data type that would mirror an option.

is deprecated with warning message:

main.warning> The deprecated Bap.Std.Log.start function is used.
This function does nothing. Use `Bap_main.init' instead

However, according to the documentation,

Attention: function is only needed when BAP framework is embedded in another
application. It shall not be called in BAP plugins. If you're not sure whether you need
to call it, then don't call it.

Currently, the inline flag (--wp-inline) will inline all of the function calls. We should have a flag that lists which functions we want to inline, ex: --wp-inline-funcs=food,bar,baz.

When the inline flag is set, the wp plugin creates an inline_env which passes in spec_inline as the default function spec: https://github.com/draperlaboratory/cbat_tools/blob/master/wp/lib/bap_wp/src/precondition.ml#L464-L475

When the environment is created, it initializes a handler for each sub in the program. If the subroutine doesn't match the prerequisites for spec_verifier_error, spec_verifier_assume, or spec_verifier_nondet, it will be mapped to spec_inline as seen in https://github.com/draperlaboratory/cbat_tools/blob/master/wp/lib/bap_wp/src/environment.ml#L114-L122

At this point, we can specify exactly which functions we want to be inlined and map other specs to the remaining functions.

BAP flags can be set in the wp.ml plugin file: https://github.com/draperlaboratory/cbat_tools/blob/master/wp/plugin/wp.ml#L142-L161

Currently function calls are summarized by introducing a fresh "chaos" variable. It would be convenient to have those tagged with the tid at its creation point.

• We should at a filename field to the env of string option type in environment.ml.
  

  cbat_tools/wp/lib/bap_wp/src/environment.ml

  Line 30 in aca7ac6

  type t = {

  
  This field should contain the name of the file whose metadata env holds. There is no filename for the tests, and this field should be None in that case.

• We should also add env to the constr type at
  

  cbat_tools/wp/lib/bap_wp/src/constraint.ml

  Lines 57 to 61 in aca7ac6

  	type t =
  	| Goal of goal
  	| ITE of Tid.t * z3_expr * t * t
  	| Clause of t list * t list
  	| Subst of t * z3_expr list * z3_expr list

  
  so that we will be able to reference the different constraints back to the original files that would be added to the env.

Currently, we are printing out the name of the refuted goal and the simplification of its z3_expression. We should also print out more details about the goal so that we have:

• name of goal
• value of goal as a z3_expr
• if the goal is an equality, print out the concrete values of the lhs and the rhs

Thus many BAP users would see it out of the box. And probably more testing and contributing.

We can generate GDB command files (https://sourceware.org/gdb/onlinedocs/gdb/Command-Files.html) to set breakpoints and register values to attempt to exercise concrete counter models of properties in a run-time environment.

With more work, we can extend this to memory values as well.

I don't expect this to be extraordinarily scalable, since the target function needs to be reached in the first place, and there are many constraints on valid memory values which we are not tracking, etc.

It'll be good for debugging and exploration though.

Hi. I have some queries related to results from explicit edge analysis on BAP and CFG generated from BAP.

1. There are some values shown along with function after vsa / explicit-edge analysis? Are they addresses of the function or offset values? (Highlighted in picture below)

2. For a small binary explicit -edge fails/crash for main function where jumptable is . Any pointers to debug?

3. Also for explicit-edge analysis to specify for a particular function I use the command bap ./switch -p explicit-edge --explicit-edge-sub main but it still performs and prints to terminal all outputs for all functions with crashing before main function. Is there some error in my command specification? (sample output listed below)

4. I used this small switch binary to see jumps. After manually extracting and visualizing as xdot .. we could see that there is no edge for jump as shown below . Should it not have an edge for jump?

Related to #93. We initially expressed memory offsets as quantifiers added to the hypothesis, but this created a slowdown with Z3.

Instead, we should be adding hooks to memory reads (currently unsure if we need writes) for both the stack and heap in the form of the constraints:

Heap(x) => init_mem_orig[x] == init_mem_mod[x + d]

and

Stack(x) => init_mem_orig[x] == init_mem_mod[x]

where d is some offset that can be inputted as a parameter.

init_mem_orig and init_mem_mod are fresh variables generated prior to running wp, and init_mem_orig == mem_orig and init_mem_mod == mem_mod should be added to the hypothesis. The user should also be able to use #101 to express precondition about the initial memory.

We still need to assert that Stack(SP) is pointing to a valid location on the stack. It is unclear whether we should say that SP is at the top of the stack, in the top region of the stack, or any other notion of it being valid.

Right now

Path objects are just maps from tids to bools (branches and the paths they take), which are useful, but hard to read in an output. As a result, Constr.print_refuted_goals and Constr.refuted_goal_to_string discard the path.

However, when stepping trough the counter-example with gdb, it's useful to be able to assess whether we're going down the right path with regards to the counter-model, so having a Constr.refuted_goal_path_to_string would be nice.

This function should include the concrete addresses of the branch, which Ivan tells me can be obtained using Term.get_attr address t. Unfortunately this means tracking terms in addition to their tids, or look up the terms each time using Term.find on the whole subroutine.

In strip_final_digits:

We are also stripping out the 8-12 from registers r8 - r12, and as a result we are setting a nonexistent registers, i.e.:

set $r = 0

Currently, hypotheses compare both BIL temporary variables and register values. Ex:

() => (|#350| = |#35076|: (= |#350| |#35076|)|#330| = |#33075|: (= |#330| |#33075|)mem0 = mem074: (= mem0 mem074)ZF0 = ZF073: (= ZF0 ZF073)SF0 = SF072: (= SF0 SF072)RSP0 = RSP071: (= RSP0 RSP071)

At hypothesis generation time, we should filter out the variables that are not registers or memory (such as #33) since temporary variables should be uninitialized at the start of a subroutine, and their types may not match up.

Currently, we handle all operations in bit-precise manners, including shifts, adds, memory reads, etc. It might be a good idea, for specifications like "check that registers were correctly saved" to allow leaving some of these operations undefined, replacing them with uninterpreted functions.

This probably can be implemented by simply generalizing the hook mechanism for expressions:

For the most part, just create a Z3 predicate Valid(n) that takes a memory access, and asserts that it is a valid access.

The tough part is adding Valid(k) assertions, which typically result either from being at some reasonable offset from SP, or being part of an allocation, which would look something like

if malloc(n) was called, then either the result is 0 or forall k <= n, Valid(res + k)

Check preservation of a BAP variable across function calls

This is very X86/X86_64 specific, but I think it's a good idea to have some lower bounds on possible values of RSP, just for sanity's sake, say 0xFFFFFFFF00000000 <= RSP <= 0xFFFFFFFFFFFFFFFF - 0x400.

Not sure it'll help all that much, but it'll be reassuring to have a bit more realistic stack values.

Currently we do not incorporate information that results from branch conditions back into the abstract values. This would improve the accuracy of the analysis. For example, BAP typically guards lifted division with a check that the divisor is not zero, and we can't make use of that check yet.

Update the documentation for loop unrolling in our design decisions file.

Right now in:

We are just printing the Z3 model after running the checker. However, this model contains duplicates such as RDX0 and RDX014, making it difficult to read, i.e.:

(define-fun RDX0 () (_ BitVec 64) 
    #x0000000000000000)
(define-fun RDX014 () (_ BitVec 64) 
    #x0000000000000000)

We could remove duplicates by possibly using

val get_decls : model -> FuncDecl.func_decl list

and then look for the var in the env1, and match that var in env2. Use the corresponding var in the env2 to determine which value is the duplicate.

Right now, the performance test at wp/lib/bap_wp/tests/performance/test_precondition.ml is only testing ocaml's ability to print huge strings. We should do 2 things:

1. Make error printing lazy, so that the string is created only on test failure.
2. Make the test actually a difficult path exploration for Z3, e.g. by taking existing tough examples from C repos or being more clever so that Z3 doesn't have the opportunity to simplify the formula too much.

Check various calling conventions:

• assume function respects calling convention in the summary
  • RSP is the same after the call as its value before it was decremented right before the call

I tried to install cbat_value_set pass on ubuntu 18.04 with BAP 2.0.0. And It fails with dependency problem.

Installing /home/hulk/.opam/4.07.0/lib/cbat_value_set/opam
opam pin add -y .
Package cbat_value_set does not exist, create as a NEW package? [Y/n] y
[cbat_value_set.~dev] synchronised from file:///home/hulk/code/bap/cbat_tools/value_set/lib
cbat_value_set is now pinned to file:///home/hulk/code/bap/cbat_tools/value_set/lib (version 0.1)
The following dependencies couldn't be met:
  - cbat_value_set → bap >= master
      no matching version

[NOTE] Pinning command successful, but your installed packages may be out of sync.
$ bap --version
2.0.0

The version of dependent BAP is master. It was failed because my BAP wasn't built from the master repository. I could successfully installed cbat_value_set by replacing master to 2.0.0.

Should BAP version be master? If not, It is better to fill with actual version number.

Currently in each of the unit tests, we are only checking to see if Z3 returns SAT or UNSAT:

In the switch_cases test, SAT was returned as expected, but the generated model specified RDI = 0 where RDI = 3 was expected. We should add more assertions to our test cases to prevent this:

• Register values:
  • obtain the Z3 model after running check
  • obtain the value of a register
  • use oUnit's assert_equals to compare the register value with the expected value
• Possibly paths?
  • is it feasible/possible to check if we are going down the correct path?

Not sure what's required for this one, hopefully no too much except the BitVector module.

It also sounds like they're moving away from having, for every module M, a sub-module M.Set and M.Map, which I use extensively in WP, so maybe some re-factoring there as well.

Just add a flag to the plugin that allows specifying a set of strings which represent the set of output registers to compare for equivalence.

To reflect WP additions

When wp is run on a single program and results in SAT!, there is no model printed out to the screen.

It seems there is a Z3 model with the correct values, but we lose the values as we are formatting them.

Some samples not working are simple_wp and return_argc.

This is a little tricky because many VCs can be created for a given application, and it's not clear which one contributes to a SAT result.

One possibility is to add a bunch of dummy VCs of the form vc_name = vc_body, at each VC creation time, (where vc_name is some fresh boolean) and maintain the map of actual names to vc_names.

Finally given a SAT result, we could check the assignments to see which one was refuted.

Note, we need to generate (vc_name = vc_body) => vc_body instead of just vc_body to get the intended result.

The opam-repository could be updated so that installation becomes simpler. Also maybe we get more bug fixes.

Currently, we are only comparing the values of the registers at the end of a subroutine. However, this doesn't make much sense for all subroutines (eg. subroutines that reference memory at different offsets that have the values). We should add the option to compare the memory in the WP plugin.