ivg on master
adds a missing module to the OA… (compare)
ivg on master
loads packages before plugins t… (compare)
ivg on master
allows to use bap instead of ba… (compare)
ivg on master
fixes installation from opam (#… (compare)
ivg on master
improves bap-configurator key h… (compare)
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
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-baseis 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
end (for some reason the loader names it
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
brk is heap, below
endp is static, and below the
--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.
@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!
barwith a call to
barwas identified as a stub in the .plt section