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.
--llvm-base is implemented in bap_llvm_loader.ml
So you are not going to share the bug unless I answer your question?) Okay, fair.
How would I use the primus api to differentiate static memory from the stack or heap?
Primus is an abstract machine and its abstraction doesn't include such notions. It has multiple memories, and each memory is segmented into regions with different permissions. In other words Primus Machine works on the CPU/MMU level, while the notions of static memory, stack, and heap, belong to the OS level.
However, the primus loader, when it loads a binary, follows the linux abstractions and sets etext, edata, and end (for some reason the loader names it endp), see man etext (it covers all three pointers). It also sets the brk variable, see man brk for more information. In short, etext points to the end of the text section, edata to the end of the data section, end endp to the upper bound of the static memory. Finally, brk points to the top of the heap.
So that everything between endp and brk is heap, below endp is static, and below the stack_base (see --primus-loader-stack-base) is considered the stack.
Hey, "this is a stickup" over a bug isn't for doing against friends, just organizations. :D hahaha :D
I mean, if you answer, that will help and save me some time. But I can test things out too. I know you are busy, so don't always have time to answer. I appreciate every time you answer.
I think there is something strange about an execution trace that I'm reviewing... I am looking at the entrance to a function being evaluated in the incidents log, and it looks like the body of a def is evaluated twice... Interpreter.exp appears to also behave the way that Eval.get does in that it triggers evaluation as though the interpreter has been given something that it treats as part of the subject.
I didn't think that the Interpreter.Make would return something that would correspond to anything in regards to programming the internals of the interpreter. I had thought that I could use it to do some background propagation during interpretation. At a def, I have to copy terms from the rhs value to the lhs value. Without it, when the lhs is used later, I think during a lookup in my machine state the lhs value won't be found. I was using Interpreter.exp to obtain a value for the rhs.
pos function
I need to 1) prove that some variable (reg or memory) value depends on another variable
2) execution path from p1 to p2 does not depend of the value of some variable
Can someone tell me, which plugins or modules to use to accomplish this?
@ogre2007:matrix.org, sorry for the late reply, I am traveling right now. This could be accomplished using our Taint Analysis Framework. It wouldn't be a proof per ce, since it is built on top of microxecution (think of it like dynamic analysis made statically). You can check into https://github.com/BinaryAnalysisPlatform/bap/tree/master/plugins/primus_taint/lisp for the example code. TThese files define a framework for tracking dependencies between things returned by a function and consumed by another function.
Concerning point 2, you need to build a program dependence graph. When we were doing spectre vulnerability analysis, we were building such dynamically (because we care very much about precision), you can look into it in the implementation.
This is for starters, don't hesitate to ask questions, I know it could be overwhelming!
4 replies
2 replies
bar with a call to bar@5b2
bar was identified as a stub in the .plt section
address attribute for bar@5b2, we didn't populate its aliases when resolving the stub so it thought that there was no implementation of bar to resolve to
6 replies
rep lodsb (%rsi), %al fails to lift to any BIL statements.$ bap mc --show-{insn=asm,bil} -- f3 ac
rep lodsb (%rsi), %al
{
}
$ bap --version
2.6.0-alpha+77d09felet query_relocs spec =
let query = Ogre.Query.(select @@ from Image.Scheme.relocation) in
Ogre.(eval (collect query) spec) |> Result.ok
let apply_relocs_for_unit target spec =
match query_relocs spec with
| None -> !!() | Some relocations ->
let endian = endian_of_target target in
let width = Theory.Target.code_addr_size target in
Machine.Seq.iter relocations ~f:(fun (fixup, addr) ->
let fixup = Addr.of_int64 ~width fixup in
let addr = Word.of_int64 ~width addr in
save_word endian addr fixup >>| ignore)