Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • 01:28

    github-actions[bot] on master

    e9f8a90 (compare)

  • 01:09

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

    fixes a knowledge base race con… (compare)

  • Sep 21 20:37

    ivg on master

    fixes a knowledge base race con… (compare)

  • Sep 21 20:37
    ivg closed #1347
  • Sep 21 19:13
    ivg opened #1347
  • Sep 18 01:33

    github-actions[bot] on master

    8a9bf35 (compare)

  • Sep 18 00:59

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

    fixes bapdoc (#1345) Despite t… nightly tests are failing due t… (compare)

  • Sep 17 13:13

    ivg on master

    uses the env files for instead … (compare)

  • Sep 16 21:01

    ivg on master

    nightly tests are failing due t… (compare)

  • Sep 16 21:01
    ivg closed #1346
  • Sep 16 21:00
    ivg opened #1346
  • Sep 16 20:39

    ivg on master

    installs ghidra in the doc-buil… (compare)

  • Sep 16 19:31

    ivg on master

    fixes bapdoc (#1345) Despite t… (compare)

  • Sep 16 19:31
    ivg closed #1345
  • Sep 16 19:31
    ivg opened #1345
  • Sep 15 15:27

    ivg on master

    fixes markup (compare)

  • Sep 15 15:09

    ivg on master

    adds the lifter tutorial (compare)

  • Sep 11 00:57

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

    (compare)

  • Sep 07 14:30
    ivg closed #1315
  • Sep 04 00:56

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

    Introduces context variables to… uses context variables to store… adds register aliases to the Co… and 1 more (compare)

Ivan Gotovchits
@ivg
Next, if you have bap 1.4 installed in opam 2.x then it should be because for some reason it wasn't able to install the latest bap. Probably it is because you have some other packages installed that are not compatible with the modern bap or because you chose a compiler version for which the newest version of bap is 1.4. Most likely the latter. Can you also show the output of opam switch?

~/bap-toolkit# eval $(opam env)
[WARNING] Running as root is not recommended

I meant to repeat those two commands after you have activated opam, e.g.,

eval $(opam env)
which bap
which ocamlfind
cL0und
@cL0und
root@105c05d3d265:~/bap-toolkit# eval $(opam env)
[WARNING] Running as root is not recommended
root@105c05d3d265:~/bap-toolkit# which bap
/root/.opam/system/bin/bap
root@105c05d3d265:~/bap-toolkit# which ocamlfind
/root/.opam/system/bin/ocamlfind
Ivan Gotovchits
@ivg
but in any case, bap-tookit doesn't work with bap 1.4, and indeed bap-main appeared only in bap 2.something.
So yes, you're using a too old version of the compiler.
and now if you will type bap --version you will get 1.4.0 not 2.4.0 right?
and for the sake of interest what is your ocaml --version?
cL0und
@cL0und
you right before I use the command you provide my bap version 2.4.0,however after this it's 1.4.0.
root@105c05d3d265:~/bap-toolkit# ocaml --version
The OCaml toplevel, version 4.05.0
Ivan Gotovchits
@ivg
yes, because before that you didn't run eval $(opam switch)
So, anyways, the minimum version of OCaml that you need to get the modern bap is 4.09.0
let's pick the latest released version of OCaml, it is 4.11.2. You need to either create a new switch, e.g.,
opam switch create 4.11.2
eval $(opam env)
opam install bap
or, if you're doing this in a dockerfile, then you should start with the right switch, when you init it, e.g., opam init --comp=4.11.2
also, when you install bap look carefully that it indeed installs the latest version of bap (e.g., bap 2.3.0, which is currently the latest released stable version)
cL0und
@cL0und
ok, I am executing the first line command.
Ivan Gotovchits
@ivg
if it again tries to downgrade it something prehistoric, then ask opam why, by explicitly constraining it, e.g., opam install bap.2.3.0 and it will tell you why it decided to install an older version. This is just a tip, I don't think that you will have any issues with 4.11.2
also, as another tip, if bap performace matter to you more than bap installation performance, you can use 4.11.2+flambda compiler. It will compile a much more efficient version of bap (more than twice as faster) but will take twice as much time to build it and many times more of disk space.
cL0und
@cL0und
My internet speed seems like too slow, it may take some time.Thanks for your tips.
Ivan Gotovchits
@ivg
oh, it will take some time, expect 20 to 40 minutes :)
cL0und
@cL0und
Yes,I don't know what's time in your location, but for me ,it's time to say good night(pray that this will be resolved when I wake up (≥﹏ ≤) ).
Ivan Gotovchits
@ivg
It should, don't worry) And have a good night)
Philip Zucker
@philzook58
Ok thanks! I think I understand. So would this be a fair stripped down version of the idea?
type 'a k = ..
type 'a k += StringKey : string k
type 'a t = U : 'd k * 'd -> 'a t

let get (type d) (key : d k) (t : 'a t) : d = match key, t with
   | StringKey, U (StringKey, x) -> x
let put key t v = U (key, v)

module StringExpr = struct
  let int x : int t = U (StringKey, string_of_int x)
  let (+) (x : int t) (y : int t) : int t =
       let x = get StringKey x in
       let y = get StringKey y in
       U (StringKey, sprintf "%s + %s" x y)
  (* and so on *)
end
Ivan Gotovchits
@ivg
yep! (though in KB, the 'a k is kept abstract, also ensures the domain structure, and provides you the get and put functions).
Ivan Gotovchits
@ivg
here's a short primer on how it could be implemented. Also, in KB we have a universal extensible record, rather than a variant, basically see the next slide :)

Is this type the analog of 'a k?

it is a wrapper over 'a k ('a k is 'a typeid), and the wrapper includes some additional information, such as the oridnal number (for comparison and hashing), the name of the slot and the introspection function,

    type 'a t = {
      ord : Uid.t;
      key : 'a typeid;
      name : Name.t;
      show : 'a -> Sexp.t;
    }
Philip Zucker
@philzook58
But the domain information is kept elsewhere?
Ivan Gotovchits
@ivg
and this is how this table is extended,
  let register_domain
    : type p. p Key.t -> p Domain.t -> unit =
    fun key dom ->
    let vtable = {
      order = begin fun (type a) (k : a key) (x : a) (y : a) ->
        let T = eq k key in
        dom.order x y
      end;
      inspect = begin fun (type a) (k : a key) (x : a) ->
        let T = eq k key in
        dom.inspect x;
      end;
      join = begin fun (type a) (k : a key) (x : a) (y : a) :
        (a,conflict) result ->
        let T = eq k key in
        dom.join x y
      end;
    } in
    Hashtbl.add_exn vtables ~key:(uid key) ~data:vtable
Philip Zucker
@philzook58
Ok I think I see. So Dict is an extensible record, and Record is a Dict + domain lookup information so that they can be merged.
Ivan Gotovchits
@ivg
that's correct, there are basically three refinements Dict <: Record <: Value
The value finally adds the static type information (the sort in the slides). In KB it is a class, where a class is a set of sorts
Philip Zucker
@philzook58

So the "sort" parameter of the value is itself a class. And this class parameter tags in essence what fields there are in this Value? I think there are perhaps multiple uses of the word "sort" being used here which is confusing me. This definition makes me think that class is in some sense a single sort and not a set of sorts?

module Class = struct
  type +'s info = {
    name : Name.t;
    sort : 's;
  }
  let id {name} = name

  type (+'a,+'s) t = 's info

I see that in for example Theory.Value it is defined as

type 'a t = (cls, 'a sort) KB.cls KB.value

Which is another notion of sort?

Ivan Gotovchits
@ivg

Well, 'a t is not a single type, but a collection of types, i.e., a type scheme. So we say that 'a t is a class, i.e., a collection of sorts.

So (Value.cls,'a) KB.cls is a class. And (Value.cls, Bool.t) KB.cls is a particular sort of the Value.cls.

And, (Value.cls, 'a sort) KB.cls KB.value is a type for values of class Value.cls which denotes an infinite number of meta-language types, each corresponding to a target language sort.

Also, a comment from the documentation that describes this on a higher level.

      A class [k] is denoted by an indexed type [(k,s) cls], where
      [s] is a sort.

      A class denotes a set of properties that describe objects and
      values of the given class. Thus, a class fully defines the
      structure of an object or a value. Sorts could be used to
      further partition the class into subsets, if needed.

From the practical perspective, class denotes the set of valid operations in the meta language, where sort denotes the set of valid operations on the object language.

E.g., with sorts we define that a well-formed msb operation takes a bitvector and returns a boolean,

  val msb : 'a bitv -> bool

but both 'a bitv and bool belong to the same class and have the same properties, so on the meta level we treat them equally (polymorphically) and can access to the same properties and even store in the same set.

Philip Zucker
@philzook58
The metalanguage is ocaml? And the object language is a particular interpretation like a pretty printed string?
Ivan Gotovchits
@ivg
Yes, the meta language (ML) is OCaml, the host language of embedding. The target language is the theory itself, i.e., the signature, e.g., the Core Theory, not the denotation (but the denotation could be the language itself). Here, a language is a set of formation rules and the vocabulary.
Philip Zucker
@philzook58
In the finally tagless encoding that packs in the carrier type to the module, would you still consider this metalanguage, object language, denotation distinction, or would it collapse into just a language (the types in the signature) and denotation (the values in the struct) ? Or is it that all of ocaml is the metalanguage, the types in the signature are the object language, and a denotation is a struct implementation?
Philip Zucker
@philzook58
Ok I think I understand. I got too hung up on the terms meta/object language. Classes are things that can be treated uniformly for some purposes. What this means is up to taste but this can be things that perhaps can reasonably be placed together in a Set data structure. Sorts are a refinement that are nice for making a more type safe interface for operations (although classes already do this too, since some operations may take/produce Theory.Value and Theory.Effect is different positions) .
Ivan Gotovchits
@ivg

Yes, it is a general notion in logic, that the language that is used to describe another language is called the meta language and the language that is described is called the object language.

The difference between representing a type as OCaml's abstract type captured in the structure vs. using a universal type is purely notational and mechanical. Mathematically speaking they are the same. So there's no difference between the classical representation vs our representation, except that we just reified the OCaml notion of an abstract type using existential.

And much like the OCaml itself as a language is not the compiler, but the set of formation rules, the same is true about Core Theory, which is a language, and corresponding denotations of this language could be seen as compilers or implementations.

Also, about the terminlogy. OCaml (and all ML family) using Universal Algebra with signatures and structures. In BAP, we employ more model theoretic approach, where signatures are called theories and their structures are called models/interpretations. There are two reasons for that, to eliminate clashing with the meta language (words like sig and struct and module are keywords, moreover, if we will choose the same names it will be always ambiguous whether we reference the meta structure or the object structure) and because the design is heavily influenced by SMTLib in particular and mathematical logic in general, which is an appropriate source of inspiration in our domain.

With that said, in the talk I stick to the Universal Algebra terminology, as it is targeted to the OCaml programmers audience, and I assumed that it would be a more comfortable abstraction. But in the reality, in BAP, we use model-theoretic notation everywhere, hence the theory and hence the core.

Hope this helps :)

Ivan Gotovchits
@ivg
P.S. the same as with sort vs type vs class. We reserve types for the meta language and sorts and classes for the object language. But conceptually they define the same idea - a set of values. With class bearing an additional constraint that the classes are disjoint, i.e., a value belongs to one and only one class. Sorts in our representations are little bit more general as Core Theory has subtyping, i.e., sorts form hierarchies and the same value belong to several sorts (all belonging to the same hierarchy).
cL0und
@cL0und

It should, don't worry) And have a good night)

Nice, it works,Thx.

Jasmin Jahic
@jahic

Hello
I was wondering, did anyone of you tried to execute Value Set Analysis from https://github.com/draperlaboratory/cbat_tools ?
I cannot compile it, although I tried from both master and release:
Master:
[ERROR] Installation of cbat_value_set.0.1 failed

Release:

  • ocamlc src/.cbat_value_set.objs/byte/cbat_value_set__Cbat_lattice_intf.{cmi,cmo,cmt} (exit 2)
  • Error: Signature mismatch: ...
Ivan Gotovchits
@ivg

@jahic
We tried, and yes it works with the latest version of BAP. And should compile with any version of BAP (as BAP keeps its interfaces stable).

The Signature mismatch... error occurs when you have some build artifacts that were built for an older version of an interface (e.g., library) and you want to link those artifacts with the newly built artifacts that uses the newer version of a library, so they contradict on this version and this error is emitted.

Using a package manager usually prevents such errors, as it is the package manager responsibility to keep track of dependencies. But if you build manually this can rarely occur, especially if you upgrade.

To help you more I need more information on what did you do before getting this error. E.g., how did you install opam and how did you try to install cbat.

9 replies
Ivan Gotovchits
@ivg
@jahic, here is the patch above that will let you build cbat's value set analysis
gitter can only attach things to the main thread :)
Philip Zucker
@philzook58
I'm using primus to record paths through a program and collecting them in a local state. I setup callbacks for jmp observation by using the ~start field of Jobs.enqueue (this setup also Linker.exec the tid of interest). When I switched to the symbolic executor, I believe I'm reregistering the for this jmp observation every time the symbolic executor forks, which starts from the top and re-emits start? This is giving me more and more duplicate addresses in my local state on each machine fork. How might I go about not having this duplication occur? Detecting if the observation is already being wtached? Using something other that ~start?
Ivan Gotovchits
@ivg
Yes, you should either register an observer as a component and add it to your system or use ~init, not sure about init, have to re-read the documentation about the lifetime of the system, but yes start is called every time a system is started so this is what happens. And the convention is to pack things that do observations into components.
Philip Zucker
@philzook58
Thank you. Moving the jmp observation to init and keeping linker.exec in start seems to have worked on cursory glance. I'll look into packaging this as a component.