So mine is happening earlier and the generated input is different,
(executor-debug "20: afl_inputs/b-desc = #x0000000000000003")
(executor-debug "20: afl_inputs/b[0] = #x28")
(executor-debug "20: afl_inputs/b[1] = #x10")
(executor-debug "20: afl_inputs/b[2] = #xc5")
(executor-debug "20: afl_inputs/b[3] = #x2f")
(executor-debug "20: afl_inputs/b[4] = #x46")
(executor-debug "20: afl_inputs/b[5] = #xe1")
(executor-debug "20: afl_inputs/b[6] = #xf0")
(executor-debug "20: afl_inputs/b[7] = #xda")
(executor-debug "20: afl_inputs/b[8] = #x90")
(executor-debug "20: afl_inputs/b[9] = #xd9")
(executor-debug "20: afl_inputs/b[0xA] = #x5c")
(executor-debug "20: afl_inputs/b[0xB] = #xd7")
(executor-debug "20: afl_inputs/b[0xC] = #x00")
(executor-debug "20: afl_inputs/b[0xD] = #x00")
(executor-debug "20: afl_inputs/b[0xE] = #x00")
(executor-debug "20: afl_inputs/b[0x1C] = #x00")
(executor-debug "20: afl_inputs/b[0x1D] = #x00")
(executor-debug "20: afl_inputs/b[0x1E] = #x00")
(executor-debug "20: afl_inputs/b[0x1F] = #x00")
(executor-debug "20: afl_inputs/b[0x20] = #x00")
(executor-debug "20: afl_inputs/b[0x21] = #x00")
(executor-debug "20: afl_inputs/b[0x22] = #x00")
(executor-debug "20: afl_inputs/b[0x23] = #x00")
(executor-debug "20: afl_inputs/b[0x24] = #x00")
(executor-debug "20: afl_inputs/b[0x25] = #x00")
(executor-debug "20: afl_inputs/b[0x26] = #x00")
(executor-debug "20: afl_inputs/b[0x27] = #x00")
(executor-debug "20: afl_inputs/b[0x2A] = #x0a")
but I presume it is because my program is slightly different (and the compiler could also generate different programs).
#include <unistd.h>
#include <string.h>
#include <stdlib.h>
int main(int argc, char **argv){
char buf[45];
FILE *input;
(input = fopen("afl_inputs/b", "r"));
fgets(buf, sizeof(buf), input);
unsigned int gen_hash = 0;
unsigned int i = 0;
const char* str = buf;
for (i = 0; i < 40 && *str; ++str, ++i){
gen_hash = (*str) + (gen_hash << 6) + (gen_hash << 16) - gen_hash;
}
unsigned int orig_hash = 445305947;
if(orig_hash == gen_hash){
puts("access granted");
*(int*)0=0;
}
return 0;
}
the gen_hash
Still, it is of importance that I find the correct value that granted us access. Preferably 445305947 not necessarily the pre-image.
But this is the correct answer!
printf "\x28\x10\xc5\x2f\x46\xe1\xf0\xda\x90\xd9\x5c\xd7\x00\n" > afl_inputs/b
$ ./example
access granted
Segmentation fault (core dumped)
so what the SE did output even if its not the exact number as we said.. multiple lead to the same hash..
the exact number is directly in the binary
1250: c7 45 ac 5b d4 8a 1a movl $0x1a8ad45b, -0x54(%rbp)
1257: 8b 45 ac movl -0x54(%rbp), %eax
125a: 3b 45 a4 cmpl -0x5c(%rbp), %eax
125d: 75 17 jne 0x17 # 12760x1a8ad45b is your 445305947
does this mean that determining a cutoff and timeout should be done for each binary?
because in this case we did not now at initially to increase.. so there is no cutoff and timeout that fits all binaries right?
because in this case we did not now at initially to increase.. so there is no cutoff and timeout that fits all binaries right?
The bigger the better. The more cutoff the more time you will spend on the same branch (but you will progress forward slower), the more timeout the more complex formulas you will be able to solve, but you will again progress slower. So if you have an infinite amount of time you can put both to infinity.
I would suggest experimenting with your test suite. For timeouts, to my experience, 16 ms is probably not enough. But anything greater than 10 seconds is overkill. I would stick somewhere between one second and ten seconds. Concerning cutoff, it should be roughly proportional to the size of the input problem. If you're hashing a file with 1k bytes, it should be 1k times N, where N is some overhead coefficient due to compiler inefficiencies. Take it equal to 10 at least, so for 1k input set it to 10k
you're welcome)
It the following is in the output, does this mean the symbolic executor is freaking out?
(executor-debug "46: Forked a new machine")
(executor-debug "46: SAT")
(executor-debug "46: &-desc = #xffffffffffffffff")
(executor-debug "46: *-desc = #xffffffffffffffff")
(executor-debug "46: \\\b-desc = #xffffffffffffffff")
(executor-debug "46: \\\
\n-desc = #xffffffffffffffff")
(executor-debug "46: \\\014-desc = #xffffffffffffffff")
(executor-debug "46: \\ -desc = #xffffffffffffffff")
(executor-debug "46: \\\127ELF\\\002\\\001\\\001-desc = #x0000000000000003")
(executor-debug "46: \\\127ELF\\\002\\\001\\\001-size = #x0000000000000000")
(executor-debug "46: \\\135-desc = #xffffffffffffffff")
(executor-debug "46: \\\136-desc = #xffffffffffffffff")
(executor-debug "46: \\\137-desc = #xffffffffffffffff")
(executor-debug "46: \\\148-desc = #xffffffffffffffff")
(executor-debug "46: \\\149-desc = #xffffffffffffffff")
(executor-debug "46: \\\152-desc = #xffffffffffffffff")
(executor-debug "46: \\\161-desc = #xffffffffffffffff")
(executor-debug "46: \\\167-desc = #xffffffffffffffff")
(executor-debug "46: \\\173-desc = #xffffffffffffffff")
(executor-debug "46: \\\177-desc = #xffffffffffffffff")
(executor-debug "46: \\\184-desc = #xffffffffffffffff")
(executor-debug "46: \\\185-desc = #xffffffffffffffff")
(executor-debug "46: \\\188-desc = #xffffffffffffffff")
(executor-debug "46: \\\197-desc = #xffffffffffffffff")
(executor-debug "46: \\\226-desc = #xffffffffffffffff")
(executor-debug "46: \\\231-desc = #xffffffffffffffff")
(executor-debug "46: \\\236-desc = #xffffffffffffffff")
(executor-debug "46: \\\237-desc = #xffffffffffffffff")
(executor-debug "46: \\\239-desc = #xffffffffffffffff")
(executor-debug "46: \\\240-desc = #xffffffffffffffff")
(executor-debug "46: \\\243-desc = #xffffffffffffffff")
(executor-debug "46: ]-desc = #xffffffffffffffff")
(executor-debug "46: _-desc = #xffffffffffffffff")
(executor-debug "46: _8-desc = #xffffffffffffffff")
(executor-debug "46: A-desc = #xffffffffffffffff")
(executor-debug "46: E-desc = #xffffffffffffffff")
(executor-debug "46: f-desc = #xffffffffffffffff")
(executor-debug "46: M-desc = #xffffffffffffffff")
(executor-debug "46: S-desc = #xffffffffffffffff")
(executor-debug "46: t-desc = #xffffffffffffffff")
(executor-debug "46: u-desc = #xffffffffffffffff")
(executor-debug "46: Z-desc = #xffffffffffffffff")
(executor-debug "46: mem[0x40C9] = #x01")
(executor-debug "46: mem[0x40CA] = #x01")
(executor-debug "46: mem[0x40CB] = #x01")
(executor-debug "46: mem[0x40CC] = #x01")
(executor-debug "46: mem[0x40CD] = #x01")
(executor-debug "46: mem[0x40CE] = #x01")
I did change the code quite a bit. Instead of a hardcoded path (but SE doesnt do anything with it) I provide the input via argv. I also initialize the buffer a bit different and I check if the buffer is not NULL so malloc succeeded. Also, yesterday, the length of the for-loop for the hash was hardcoded. now It is variable. So probably I have to increase the cutoff and timeout again because the SE has to solve the length variable as well..
Yesterday it was:
for (i = 0; i < 40 && *str; ++str, ++i){
gen_hash = (*str) + (gen_hash << 6) + (gen_hash << 16) - gen_hash;
}Now it is:
for (i = 0; i < len && *str; ++str, ++i){
gen_hash = (*str) + (gen_hash << 6) + (gen_hash << 16) - gen_hash;
}The len variable is determined when a file is opened based upon what contents that file has
I hope that you aren't annoyed by me, but I have another question. I was reading up on the Theory library again, and I was wondering how that all fits in. I don't see a lisp theory plugin anywhere, and I wondered what use cases Theory was intended to support. I suppose I thought it might have facilitated some kind of dynamically acquired language. Like, say let the language form as a part of some computational engineering or machine learning. I am not sure that that is the right use case though. What do you have in store for Theory?
(this is just curiosity)
I am not, I am just not working at CMU anymore, so I can spend as much time on BAP as when it was my only job. The Theory library is the tagless-final program representation. I am surprised with your question, as we discussed this many times and you even read the draft paper and saw my presentation, where it is described. Maybe I totally misunderstood your question, though.
Possibly I am rusty after some time of having not read those papers. I didn't know you weren't at CMU anymore.
I am familiar with your paper and tagless final style and the Theory documentation. I suppose I haven't exercised Theory as much as I have a lot of the rest of the BAP API. So, although I see it, I don't see it in use. Let's say you were familiar with a particular car part. Well, in that case, you could know what could be done with it from what it's functionality is. Theory seems really general with many use cases, so it's not quite like a specific car part. I just wasn't sure what your exact use case was.
I think I get what it does, but perhaps my foresight is fuzzy. Seems like you could facilitate language meaning support. I suppose I think that because part of BAP's fundamental objectives is to support decoding to a programming language, so therefore decompilation.
@ivg Ok so I did modify the harness. For the fuzzer I had to do the input for stdin otherwise it would freak out. Somehow, when I run the symbolic executor it outputs (what you mentioned earlier) that there is only one fork and the message stating that there is no more work to do. The hash function etc. is exactly the same, I only changed the way input files are handled. I am wondering what could be the problem now.. I tried increasing both the cutoff and timeout.
is it because its reading from stdin?
with
getline(buf,len,stdin)
the variables from IO are turned into symbolic values right?
But I need this piece of code in order for the program to work properly.
Maybe a weird remark.. because the symbolic executor is printing debug information.. is this read by the binary via IO?
In that case I should tell the symbolic executor not to do IO
Ok removing symbolic-stdio from --primus-lisp-load doesnt have any effect.
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.
Hi, I've been using BAP to analyse Windows binaries as follows:
bap ./binary.dll -dbir --optimization-level=3After 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 file binary.dll
binary.dll: PE32+ executable (DLL) (GUI) x86-64, for MS Windows
@mpmfrans For
getline maybe there is no API and stub for it: https://github.com/BinaryAnalysisPlatform/bap/blob/master/plugins/api/api/c/posix.h
You can find these headers installed in
~/.opam/<my-switch>/share/bap/api/c/
Additionally you would want to stub out the functionality of
getline using Primus Lisp
Try with the option
--primus-print-observations=linker-unresolved and see if it does that when it tries to call getline