Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Dec 06 19:42
    ivg opened #1562
  • Dec 03 01:56

    github-actions[bot] on master

    1077911 (compare)

  • Dec 03 01:07

    github-actions[bot] on v2.6.0-alpha

    (compare)

  • Nov 26 02:04

    github-actions[bot] on master

    1077911 (compare)

  • Nov 26 01:12

    github-actions[bot] on v2.6.0-alpha

    (compare)

  • Nov 22 05:05
    andrewj-brown synchronize #1546
  • Nov 19 02:21

    github-actions[bot] on master

    1077911 (compare)

  • Nov 19 01:20

    github-actions[bot] on v2.6.0-alpha

    (compare)

  • Nov 14 15:16
    kit-ty-kate opened #1561
  • Nov 12 02:30

    github-actions[bot] on master

    1077911 (compare)

  • Nov 12 01:04

    github-actions[bot] on v2.6.0-alpha

    Corrected primus_dictionary_mai… Fix not propagating term attrs … (compare)

  • Nov 10 21:03
    bmourad01 synchronize #1559
  • Nov 10 20:14
    bmourad01 opened #1559
  • Nov 10 19:58

    ivg on master

    Fix not propagating term attrs … (compare)

  • Nov 10 19:58
    ivg closed #1556
  • Nov 08 18:37
    ivg closed #1558
  • Nov 08 18:36

    ivg on master

    Corrected primus_dictionary_mai… (compare)

  • Nov 05 02:25

    github-actions[bot] on master

    77d09fe (compare)

  • Oct 31 17:22
    A-Benlolo opened #1558
  • Oct 29 02:37

    github-actions[bot] on master

    77d09fe (compare)

mpmfrans
@mpmfrans
In that case I should tell the symbolic executor not to do IO
Ok removing symbolic-stdio from --primus-lisp-load doesnt have any effect.
mpmfrans
@mpmfrans
Yes, everything is working. The SE gives me multiple solutions. The solutions do make the program branch the if-statement and output "access granted". The only question left is why the SE is not functioning properly (starting, fork one and quit) when I add the line getline(buf,len,stdin) to the program.
Matt Griffin
@matt.griffin_gitlab

Hi, I've been using BAP to analyse Windows binaries as follows:

bap ./binary.dll -dbir --optimization-level=3

After upgrading to BAP 2.5.0 yesterday (late to the game I know) I get the following error:

Failed to build the project: attribute "llvm:symbol-entry" didn't provide a
value for the field "value"

This is definitely new :(

For reference this is the output of file binary.dll

binary.dll: PE32+ executable (DLL) (GUI) x86-64, for MS Windows
Benjamin Mourad
@bmourad01
@mpmfrans For getline maybe there is no API and stub for it: https://github.com/BinaryAnalysisPlatform/bap/blob/master/plugins/api/api/c/posix.h
You can find these headers installed in ~/.opam/<my-switch>/share/bap/api/c/
Additionally you would want to stub out the functionality of getline using Primus Lisp
Try with the option --primus-print-observations=linker-unresolved and see if it does that when it tries to call getline
mpmfrans
@mpmfrans
Indeed there is no implementation for that function. For getchar() there is though.
Ivan Gotovchits
@ivg

Yes, everything is working. The SE gives me multiple solutions. The solutions do make the program branch the if-statement and output "access granted". The only question left is why the SE is not functioning properly (starting, fork one and quit) when I add the line getline(buf,len,stdin) to the program.

Probably because it covered everything. If you didn't have a branch then what do you expect? SE will not just reran randomly if there is no control-flow dependency on the symbolic input. Also, don't forget that SE will search not only for the bug that you want it to search, but for any other bug in your code. So make sure that you check the return codes of all functions.

And yes, indeed, getline is not supported
mpmfrans
@mpmfrans
Thanks again @ivg I implemented fgetc(stdin) and it is working properly. I am so excited about this field or research!
Matt Griffin
@matt.griffin_gitlab

Hi, I've been using BAP to analyse Windows binaries as follows:

bap ./binary.dll -dbir --optimization-level=3

After upgrading to BAP 2.5.0 yesterday (late to the game I know) I get the following error:

Failed to build the project: attribute "llvm:symbol-entry" didn't provide a
value for the field "value"

This is definitely new :(

For reference this is the output of file binary.dll

binary.dll: PE32+ executable (DLL) (GUI) x86-64, for MS Windows

I'm not sure how I managed to do this in the past as it fails with the same error in all the previous versions (2.2., 2.3., 2.4.*). I guess it has something to do with the llvm version?

Ivan Gotovchits
@ivg

@matt.griffin_gitlab, can you clean the caches (bap --cache-clean) and try again. Most likely it won't help, but just to be sure. If it will not help, then please create an issue and don't forget to inlude bap --llvm-version output. It would be nice, if you will attach the binary for reproduction. If it is not possible, then attach the output of bap specification binary.dll (you may redact sensitive data, if you need).

As a workaround, you can experiment with llvm versions. As a hacky workaround, you can remove llvm:symbol-entries, e.g.,

bap specification binary.dll | grep -v llvm:symbol-entry > binary.ogre
bap ./binary.dll --loader=./binary.ogre

though it may result in an incomplete disassembly. A more sophisticated workaround with some sed magic, is to add a dummy 0 value for each llvm:symbol-entry.

Matt Griffin
@matt.griffin_gitlab
Sure, I can do the above. FYI I ran the command using the BAP docker image in case the issue was with my machine and it succeeded!
Ivan Gotovchits
@ivg
ha, so it should be definitely something wrong with llvm
can you compare bap --llvm-version on your machine and in the docker container?
2 replies
Benjamin Mourad
@bmourad01
@ivg I think I observed the real bottleneck when loading large programs in Primus: https://github.com/BinaryAnalysisPlatform/bap/blob/master/plugins/primus_loader/primus_loader_basic.ml#L206
Though I'm not sure if we can do much to optimize it
Ivan Gotovchits
@ivg
@bmourad01, I have an idea how we can make it faster. We should turn into names only tids that correspond to blocks and subroutines. Because only those could be called via linker (individual defs and jumps are not allowed, so we shouldn't link them, or add them to the environment)
Benjamin Mourad
@bmourad01
What is the intended purpose of that init_names pass? I think the linking of the names is done elsewhere, but here it seems that the names are being made available in the Primus environment
Ivan Gotovchits
@ivg
So that you can do @malloc or %deadbeef and corresponding tids will be evaluated to their addresses and you can do transfer control flow to those addresses
mpmfrans
@mpmfrans
What is the default cutoff? For timeout its 16 ms.
ah found it, its 1.
Benjamin Mourad
@bmourad01
@ivg Indeed making that change cut the loading time in half
Kenneth Adam Miller
@KennethAdamMiller
Upon running upgrades when installing from master, I am hitting a lot of errors because certain META files remain past the uninstall during the upgrade cycle. An example META file:
~/.opam/4.13.1/lib/bap-mips/META
Ivan Gotovchits
@ivg
yeah, upgrade never works for bap and opam, you have to start a new switch
Kenneth Adam Miller
@KennethAdamMiller
Oh ok
mpmfrans
@mpmfrans

I run the command with
--primus-print-obs=executor-debug

--primus-print-out=trace.log
In the terminal multiple "Access Granted" appear so SE found multiple solutions. However If I search the trace.log I can't find that specific string to see what input lead to solving that constrain and therefore executes puts("Access Granted"). How do I search the solutions? How did you yesterday find the bytes:
"\x28\x10\xc5\x2f\x46\xe1\xf0\xda\x90\xd9\x5c\xd7\x00\n" I know where to look when I do not trace.log and just stop the SE so the solution is visible in the terminal..

there is also a -dbir:example.bir
Ivan Gotovchits
@ivg

The solution is printed like this, <file>[<offset>] = <value>,e.g.,

(executor-debug "30: afl_inputs/b-desc = #x0000000000000003")
(executor-debug "30: afl_inputs/b-size = #x0000000000000028")
(executor-debug "30: afl_inputs/b[0] = #xa0")
(executor-debug "30: afl_inputs/b[1] = #x2b")
(executor-debug "30: afl_inputs/b[2] = #x84")
(executor-debug "30: afl_inputs/b[3] = #x99")
(executor-debug "30: afl_inputs/b[4] = #x7b")
(executor-debug "30: afl_inputs/b[5] = #x00")
(executor-debug "30: afl_inputs/b[6] = #x00")
(executor-debug "30: afl_inputs/b[8] = #x00")
(executor-debug "30: afl_inputs/b[9] = #x00")

So the first byte is \0xa0 the second is \x2b and so on.

If a byte is missing in the solution, then it could be anything.
mpmfrans
@mpmfrans
Yes, I did understand, thank you! However, the trace.log is very long and I can find "Access Granted". How do I find the solution?
Or is this done by hand or some custom wrapper that searches the trace.log?
Ivan Gotovchits
@ivg
@mpmfrans, I added the call observation to the trace log, so that I can find the puts call and search back for the last SAT.
Kenneth Adam Miller
@KennethAdamMiller
Is there anywhere in the Primus API way to get the Target or CPU module? I need the abstract interface for determining if a variable is a stack pointer, val is_sp : var -> bool. I'm having difficulty because the code I think is valid OCaml is giving me a syntax error:
  let original_sp =
    Machine.arch >>= fun arch -> 
    let module Target = target_of_arch arch in
    Machine.return @@
    object(self)
      inherit [exp Var.Map.t] Term.visitor
      method visit_sub sub bounds =
        match Seq.hd (Term.enum blk_t sub) with
        | None -> bounds
        | Some blk ->
          Seq.find_map (Term.enum def_t blk) ~f:(fun d ->
              if Target.is_sp @@ Def.lhs d then Some d else None
            )
    end
Ivan Gotovchits
@ivg
@KennethAdamMiller, use Machine.gets Project.target and then work with Theory.Target, it has everything you need, including registers and abi and all the stuff.
The Bap.Std.Arch module and Bap.Std.Target are deprecated.
Kenneth Adam Miller
@KennethAdamMiller
Oh
Ivan Gotovchits
@ivg
For example, to get a stack pointer,
  let stack_pointer =
    Machine.gets Project.target >>| fun t ->
    match Theory.Target.reg t Theory.Role.Register.stack_pointer with
    | None -> None
    | Some sp -> Some (Var.reify sp)
Benjamin Mourad
@bmourad01
I wonder if it would have advantage for graphlib to compute the worklist order this way instead of reverse DFS postorder
Ivan Gotovchits
@ivg
Only an experiment can show, but I doubt that there will be any significant improvement.
Benjamin Mourad
@bmourad01
@ivg If you get a chance, would you be able to review #1554 ?
Ivan Gotovchits
@ivg
@bmourad01, merged! Besides, how significant was the speed up?
Benjamin Mourad
@bmourad01
Very. On one particular example i got 2x speedup in loading time
I would imagine that linking all the def terms associated with an address took up a bulk of the time since there are so many of them
Ivan Gotovchits
@ivg
:+1: awesome!
Kenneth Adam Miller
@KennethAdamMiller

Ok ok. let me rephrase my last question as a discussion instead, which you saw but I deleted. I think it was a trivial question according to how to use the API currently. However, it isn't a stupid question if you want to make sure that the code quality is good. I was just trying to point out that I think a general solution could be done much better. From that perspective it ought to be made more clear.

Often, in a given analysis, the callbacks give a view that is a brief peek at a small cross section of variables that is too small in order for the desired scenario to be identified. In this case, one can define local machine state such that the conditions can accumulate as they are checked for. This results in something that is somewhat messy though, because there may be many analyses needing this kind of work, each with their own group of required conditions for the trigger searched for. It's almost as though bare might need to be run within the context of a primus machine at each step; but the information given to bare has to be all of the latest information yielded by a given trail. Every trail is unique, so it seems to me that somehow allowing more than one observation to accumulate information, allowing a contiguous cross-section of execution, or any complete set of related requirements, to line up with a given bare rule that has matched. After that point the function triggered might receive that entire context. This practice, which is often needed in an analysis, is a lot better of a way to manage with analyses that require some trail of events before being run, so it kind of deserves to be factored into something reusable.

That's all I was trying to point out. I just meant to do it a bit interactively.

Benjamin Mourad
@bmourad01
@ivg Not to bug, but is there a chance for a final review of #1547 soon?
Ivan Gotovchits
@ivg
Yes, I think we reviewed and re-iterated it many times, so it is time to merge it :)