Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • 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)

  • Oct 29 01:04

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

    (compare)

  • Oct 27 14:51
    bmourad01 synchronize #1556
  • Oct 22 02:41

    github-actions[bot] on master

    77d09fe (compare)

Kenneth Adam Miller
@KennethAdamMiller
I think I get what it does, but perhaps my foresight is fuzzy. Seems like you could facilitate language meaning support. I suppose I think that because part of BAP's fundamental objectives is to support decoding to a programming language, so therefore decompilation.
mpmfrans
@mpmfrans
@ivg Ok so I did modify the harness. For the fuzzer I had to do the input for stdin otherwise it would freak out. Somehow, when I run the symbolic executor it outputs (what you mentioned earlier) that there is only one fork and the message stating that there is no more work to do. The hash function etc. is exactly the same, I only changed the way input files are handled. I am wondering what could be the problem now.. I tried increasing both the cutoff and timeout.
is it because its reading from stdin?
with getline(buf,len,stdin)
the variables from IO are turned into symbolic values right?
mpmfrans
@mpmfrans
Ok so yes it is due to the getline(buf,len,stdin). If i comment this line the symbolic executor is running.
But I need this piece of code in order for the program to work properly.
Maybe a weird remark.. because the symbolic executor is printing debug information.. is this read by the binary via IO?
mpmfrans
@mpmfrans
and therefore quits symbolically executing after only one fork?
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