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)

Florian Märkl
@thestr4ng3r
2.5.0-alpha+6c1d4c4
Ivan Gotovchits
@ivg
awesome, thanks!
Ivan Gotovchits
@ivg

@thestr4ng3r, I fixed the bug with the empty bil, see #1420, but now we have another problem,

Uncaught exception:

  (Failure "binop type error - 1:32u = 0:1u")

I am currently tracking its source, so I will keep you posted. With that said, in case the error is in bap-veri, may I have your permission to push your https://github.com/thestr4ng3r/bap-veri changes to the upstream master?

Florian Märkl
@thestr4ng3r
Awesome, thank you! Yes, of course feel free to take any code from my forks.
Ivan Gotovchits
@ivg
thanks!
Florian Märkl
@thestr4ng3r
Ivan Gotovchits
@ivg
Yep, I looked at the changes and they look good. Not sure why you added compare, but it won't hurt indeed.
Concerning the results, I am already getting better results (but still tracking the type error - probably it comes from some new Primus Lisp-defined instructions, which has a more lax type system, so it is most likely a bug in the lifter, so it is great that we're reviving the bap-veri).
|-------------------------------|
|             | rel    | abs    |
|-------------+--------+--------|
| overloaded  | 0.00%  | 0      |
| undisasmed  | 0.00%  | 0      |
| misexecuted | 2.29%  | 3720   |
| mislifted   | 0.00%  | 0      |
| damaged     | 0.00%  | 0      |
| successed   | 97.71% | 158977 |
|-------------------------------|
Florian Märkl
@thestr4ng3r
Very nice.
Something was requiring the compare after updating dependencies or so, but I don't remember exactly where it was.
Ivan Gotovchits
@ivg
@thestr4ng3r, so at least BIL is well typed. The problem comes from the trace itself. The bitness of the register is somehow broken, I have flags with 32 bits and registers like R10 that have 0 width.
So which version of qemu and librace you were using?
Ivan Gotovchits
@ivg
Okay, so it was always like this, the size of registers was set to 0 and all words are always 4 bytes long. Now, I am trying to figure out why it was working. I will provide a fix later, after my curiosity is satisfied :)
    oi->bit_length = 0;
    oi->operand_info_specific = ois;
    oi->operand_usage = ou;
    oi->value.len = 4;
Florian Märkl
@thestr4ng3r
Yeah I noticed those 0s too. This is relevant I think: https://github.com/BinaryAnalysisPlatform/bap-frames/blob/86019d81a381de1b77ff14aacdf0d2e7c65b2645/lib/frame_events.ml#L63-L64
If it's 0, it just uses the length of the given data times 8.
But at the same time it seems to use the 0 as-is here: https://github.com/BinaryAnalysisPlatform/bap-frames/blob/86019d81a381de1b77ff14aacdf0d2e7c65b2645/lib/frame_events.ml#L79
Regarding the trace, I used this container since the old qemu only runs on ancient ubuntu: https://github.com/rizinorg/rz-tracetest/tree/master/qemu-bap-docker
Ivan Gotovchits
@ivg
nice, thanks! Yeah, the reader is fair, but it can't do anything as the information is indeed missing.
Ivan Gotovchits
@ivg

Okay, I finished my historic research :) The last time we were running bap-veri on arm targets was April, 2017, on BAP 1.2. In August of the same year, in BAP 1.3 release we made BAP more strict and added a type check of each operation (before that the evaluator was happily accepting 0:32 = 0.1).

Now, when it is cleary why it did work and doesn't work any more, I will now work on a solution :)

For the reference this is the commit the broke bap-veri on arm #688
Benjamin Mourad
@bmourad01
@ivg How would one use the monads library to compose, say, the State and Result monads together? I'm a bit confused about the interface
Ivan Gotovchits
@ivg
Something like, this,
module M = Monad.State.Make(Doc)(struct
    include Monad.Result.Error.T(B)         (* adds types *)
    include Monad.Result.Error.Make(B)      (* adds functions and modules *)
  end)
See also #1354
Benjamin Mourad
@bmourad01
I see, thanks!
Florian Märkl
@thestr4ng3r
@ivg Thanks for the insight, I am looking forward to the fix :-)
Judging only by manual inspection of the traces, the updated qemu now seems to work well enough for arm after a lot of smaller fixes. I have squashed it all together since a lot of stuff just went back and forth without much value in the history: https://github.com/thestr4ng3r/bap-qemu/commits/tracewrap-6.1.1
What is your plan for merging this into the https://github.com/BinaryAnalysisPlatform/qemu repo? With the diverged history, a pr in the classical sense may not make sense since merging it mess everything up. Instead, I could for example imagine tagging (or creating a new branch from) the current state of the tracewrap branch, so it won't get lost, and then force-pushing the updated one. Or alternatively, the new one could be pushed to a new branch and made the "default" branch.
Florian Märkl
@thestr4ng3r
Looks like I missed the qemu 6.2.0 release. So here it is rebased on top of that: https://github.com/thestr4ng3r/bap-qemu/commits/tracewrap-6.2.0
Ivan Gotovchits
@ivg
awesome! The fix will be soon)
Philip Zucker
@philzook58
Can one dump the herbrand theory from the command line?
Ivan Gotovchits
@ivg
yes, enable it via --core-theory-herbrand and the use -dknowledge (the same for bap-mc, but you can also use --show-sema)
Philip Zucker
@philzook58
Is there a slot for it in Label.t ? I'm unclear on where Effect.t and Value.t go if they don't get attached to a Program.t. I sort of thought they might just get garbage collected away
No wait. What I'm saying doesn't make sense.
Ivan Gotovchits
@ivg

No, the slot is not published (and it is not in the program class but in the semantics one).

I'm unclear on where Effect.t and Value.t go if they don't get attached to a Program.t.

It's indeed unclear :) Can you reveal more context, why effects and values are going away?

Philip Zucker
@philzook58
When I dump -dknowledge I see Program.t and it's semantics, but not the individual Effect.t/Value.t as entries. At least I don't think I do. There is a lot to sift through
Ivan Gotovchits
@ivg
The semantics of an instruction is stored in the core:semantics slot, and the Herbrand denotation fo the effect is stored in the core:eff field of the semantics property. Finally, the Herbrand denotation of the value is stored in the core:val of the core:value slot of the core:semantics slot. E.g., here is the snippet from the -dknowledge output with enabled Herbrand theory,
(0x5ee
  ((bap:lisp-args
    ((((core:val (R2)) (lisp-symbol (R2)) (bap:exp R2))
      ((core:val (SP)) (lisp-symbol (SP)) (bap:exp SP))
      ((core:val (0xe)) (bap:static-value (0xe)) (bap:exp 0xE))
      ((core:val (Nil)) (lisp-symbol (Nil)) (bap:exp Nil)))))
   (bap:lisp-name (llvm-thumb:tMOVr))
   (bap:insn ((tMOVr R2 SP 0xe Nil)))
   (bap:mem ("5ee: 6a 46"))
   (bap:arch armv7)
   (core:semantics
    ((core:eff ((set R2 SP)))
     (bap:ir-graph "000003d1:
                    000003d2: R2 := SP")
     (bap:insn-dests (()))
     (bap:insn-ops ((R2 SP 14 Nil)))
     (bap:insn-asm "mov r2, sp")
     (bap:insn-opcode tMOVr)
     (bap:insn-properties
      ((:invalid false)
       (:jump false)
       (:cond false)
       (:indirect false)
       (:call false)
       (:return false)
       (:barrier false)
       (:affect-control-flow false)
       (:load false)
       (:store false)))
     (bap:bir (%000003d1))
     (bap:bil "{
                 R2 := SP
               }")
     (core:insn-code ("6a 46"))
     (core:value ()))) 
   (core:label-addr (0x5ee))
   (core:label-unit (3))
   (core:encoding bap:llvm-thumb)))
One thing that you might encounter is that you need to disable cache, since enabling a theory might not trigger recompilation and the knowledge base is just read from the cache. I will look into this, if that is true then we need to change the core plugin tags, so that the change in configuration will result in the change of the context digest.
Philip Zucker
@philzook58
Yes, I needed to do --no-cache to see this
I guess that's a disadvantage of often using /bin/true all the time
Ivan Gotovchits
@ivg
No, it is just because I didn't specify correctly semantic tags for the core theory plugin, it mentions a lot of things, but missing the most important ones, i.e., that it provides semantics and symbolization) I will push a quick fix, so that you don't need to bother about cache anymore. Now, whenever you change any parameter in the --core-theory plugin it will change the cache digest.
Philip Zucker
@philzook58
I guess my other question was, suppose I make an Effect.t object, but it is not the child of any Program.t. Does this persist in the KB? Would it show up in -dknowledge? Do I need to keep a reference to it somewhere or else is gets GCed away?
Ivan Gotovchits
@ivg
No, it will not be persisted nor would it be displayed, since it was never stored in the knowledge base. The knowledge base stores properties of objects. So, unless you have created an object and set the semantics property of it to some effect it won't be in the knowledge base.
also see #1421
Philip Zucker
@philzook58
Thanks! But can an Effect not be an object? Like if I called KB.Object.create Theory.Effect.cls >>= fun obj -> (* do something *)?
Ivan Gotovchits
@ivg

We are not storing effects in the Core Theory knowledge base.

As an aside, in general, you can store anything in the knowledge base, aka Bap_knowledge, since it is only the engine. But when we speak about the Core Theory (Bap_core_theory) and BAP as a framework, we speak about a particular set of ontological commitments that describe the bap position on the terms in which we should think about program semantics. Of course, these commitments by no means are carved in stone and open for discussion and amendments. So in the K&R (knowledge and representation) system of BAP we prefer not to create objects that represent semantics. The motivation behind this decision is that semantics, whether it represents an effect or a computation value, are value objects. They are abstract entities, not concrete, much like a number. As any abstract entities, they should be immutable. Contrary to values, objects are denoted by their identity and a set of properties. Objects are mutable (though our knowledge base allows only monotonic mutability, i.e., the value of an object could only be refined). That is why, we refrain from ever creating an object of the semantics class, as this will denote semantics as a concrete mutable entity. It would be the same logical error, as representing a Number as a class with a mutable field called, value, e.g.,

class number x = object
  val mutable value : int = x
  method change x = value <- x
  method value = value
end

let seven = new number 7 
seven#change 3
assert (seven#value = 7)

End of aside.
So if you now don't want to create objects of the semantics class, and I hope you don't :), and you want to store some semantics in the knowledge base, then you should create an object of the program class, and set its semantics property to the desired effect. Alternatively, you can store a rule in the knowledge base that will compute the semantics of an object, possibly deriving it from the other fields.

Ivan Gotovchits
@ivg
@thestr4ng3r, okay the fix is out, see #1422. I decided to take a radical approach but it took me some time to persuade myself that this is the right approach.
Philip Zucker
@philzook58
This distinction between objects and values makes sense. It is a part of the design I had not understood. Thank you.
Florian Märkl
@thestr4ng3r
@ivg Nice, thanks! Does this imply zero or sign extension? From what I can tell it depends on is_signed of the bv, which seems weird to me to have a signedness property as part of the bitvector (rather than signedness being defined purely by operations on them), but according to https://github.com/BinaryAnalysisPlatform/bap/blob/e52449ec0c9f0d4e664934ada8aa87bcd67a373b/lib/bap_types/bap_bitvector.ml#L14-L16 this seems to be old behavior anyway, so is the change only affecting code using these legacy apis?
Ivan Gotovchits
@ivg
Yes, while not described clearly in the comments it will properly sign-extend if one of the operands is signed and smaller than another.
Ivan Gotovchits
@ivg

I will wait until the tests pass and update the comment to make it clear.

this seems to be old behavior anyway

This was a rather misleading comment) It is not an old behavior but rather historical. But it is still there and will be there for the foreseeable future. The Bap.Std.Bitvector.t also known under its aliases word and addr, carries signedness and size as parts of its representation. And operations over words are overloaded depending on the representation, so a signed bitvector behaves differently from the unsigned when it is compared, divided, etc. The same is true for the size, so that addition operation is actually overloaded and have different behavior depending on the size. A sort of an ad-hoc polymorphism.

In the more modern parts of BAP, namely in the Core Theory representation, we are not using Bap.Std.Bitvector.t but instead rely on Bitvec.t in which these things are removed and the bitvector is nothing more than a sequence of bits. And the semantics of the bitvector operations in Bitvec is purely defined by the operation name, which is much more natural from the mathematical point of view. But the Bap.Std interface is still there and will be for a long time.

and representation-wise, Bap.Std.Bitvector.t is just a Bitvec.t with concatenated size and signedness,
   word format:
     +-----------+------+---+
     |  payload  | size | s |
     +-----------+------+---+
      size+15  15 14       0
Florian Märkl
@thestr4ng3r
I see, thanks for the clarification!
Florian Märkl
@thestr4ng3r
Starts to look pretty good:
|-------------------------------|
|             | rel    | abs    |
|-------------+--------+--------|
| overloaded  | 0.00%  | 0      |
| undisasmed  | 0.00%  | 0      |
| misexecuted | 2.50%  | 4445   |
| mislifted   | 0.00%  | 0      |
| damaged     | 0.00%  | 0      |
| successed   | 97.50% | 173001 |
|-------------------------------|
Ivan Gotovchits
@ivg
hmm, is that the same trace that you gave me yesterday? My results are:
|-------------------------------|
|             | rel    | abs    |
|-------------+--------+--------|
| overloaded  | 0.00%  | 0      |
| undisasmed  | 0.00%  | 0      |
| misexecuted | 1.82%  | 2958   |
| mislifted   | 0.00%  | 0      |
| damaged     | 0.00%  | 0      |
| succeeded   | 98.18% | 159739 |
|-------------------------------|
Ivan Gotovchits
@ivg
Judging by the total number of instructions I tend to conclude that you have a different trace. Besides, the number of missing instructions is still a little bit higher than I would expect. Some of them are indeed errors, that I am planning to fix soonish. But some are still fishy, that is what I am currently investigating. Will keep you posted.
Florian Märkl
@thestr4ng3r
No, this is a new trace from qemu 6.2.0, so some of these errors might also still be qemu's fault.