github-actions[bot] on v2.6.0-alpha
Corrected primus_dictionary_mai… Fix not propagating term attrs … (compare)
ivg on master
Fix not propagating term attrs … (compare)
ivg on master
Corrected primus_dictionary_mai… (compare)
--primus-print-observations=linker-unresolvedand see if it does that when it tries to call
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.
getlineis not supported
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
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?
@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
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.
bap --llvm-versionon your machine and in the docker container?
I run the command with
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..
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 = #xa0") (executor-debug "30: afl_inputs/b = #x2b") (executor-debug "30: afl_inputs/b = #x84") (executor-debug "30: afl_inputs/b = #x99") (executor-debug "30: afl_inputs/b = #x7b") (executor-debug "30: afl_inputs/b = #x00") (executor-debug "30: afl_inputs/b = #x00") (executor-debug "30: afl_inputs/b = #x00") (executor-debug "30: afl_inputs/b = #x00")
So the first byte is
\0xa0 the second is
\x2b and so on.
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.