Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Feb 07 22:27

    ivg on master

    Relax the restrictions on the e… (compare)

  • Feb 07 22:27
    ivg closed #1578
  • Feb 07 20:46
    ivg edited #1578
  • Feb 07 19:53
    bmourad01 opened #1578
  • Feb 03 14:53
    Heersin opened #1577
  • Jan 26 13:56
    ivg edited #1576
  • Jan 26 13:56
    NicolaasWeideman opened #1576
  • Jan 12 17:07

    ivg on master

    adds a missing module to the OA… (compare)

  • Jan 12 17:07
    ivg closed #1574
  • Jan 12 15:58
    ivg review_requested #1574
  • Jan 12 15:58
    ivg assigned #1574
  • Jan 12 15:58
    ivg opened #1574
  • Jan 11 19:38

    ivg on master

    loads packages before plugins t… (compare)

  • Jan 11 19:38
    ivg closed #1573
  • Jan 11 19:38

    ivg on master

    allows to use bap instead of ba… (compare)

  • Jan 11 19:38
    ivg closed #1572
  • Jan 11 18:26
    ivg review_requested #1573
  • Jan 11 18:26
    ivg assigned #1573
  • Jan 11 18:26
    ivg opened #1573
  • Jan 11 17:45
    ivg review_requested #1572
Ivan Gotovchits
@ivg
well, any hash by definition will have collisions.
mpmfrans
@mpmfrans
your machine must be way faster than mine because I still not have a solution
(executor-debug "0: Client is finished, master is resumed")
(executor-debug "0: We have some tasks")
(executor-debug "30: Forked a new machine")
(executor-debug "30: SAT")
(executor-debug "30: afl_inputs/b-desc = #x0000000000000003")
(executor-debug "30: afl_inputs/b-size = #x0000000000000028")
(executor-debug "30: afl_inputs/b[0] = #xa0")
(executor-debug "30: afl_inputs/b[1] = #x2b")
(executor-debug "30: afl_inputs/b[2] = #x84")
(executor-debug "30: afl_inputs/b[3] = #x99")
(executor-debug "30: afl_inputs/b[4] = #x7b")
(executor-debug "30: afl_inputs/b[5] = #x00")
(executor-debug "30: afl_inputs/b[6] = #x00")
(executor-debug "30: afl_inputs/b[8] = #x00")
(executor-debug "30: afl_inputs/b[9] = #x00")
(executor-debug "30: afl_inputs/b[0xA] = #x00")
(executor-debug "30: afl_inputs/b[0xB] = #x00")
(executor-debug "30: afl_inputs/b[0xC] = #x00")
(executor-debug "30: afl_inputs/b[0xD] = #x00")
(executor-debug "30: afl_inputs/b[0xE] = #x00")
(executor-debug "30: afl_inputs/b[0x11] = #x0a")
(executor-debug "30: afl_inputs/b[0x13] = #x0a")
(executor-debug "30: afl_inputs/b[0x14] = #x0a")
(executor-debug "30: afl_inputs/b[0x15] = #x0a")
(executor-debug "30: afl_inputs/b[0x20] = #x00")
(executor-debug "30: afl_inputs/b[0x21] = #x00")
(executor-debug "30: afl_inputs/b[0x22] = #x0a")
(executor-debug "30: afl_inputs/b[0x23] = #x00")
(executor-debug "30: afl_inputs/b[0x24] = #x00")
(executor-debug "30: afl_inputs/b[0x25] = #x00")
(executor-debug "30: afl_inputs/b[0x26] = #x00")
(executor-debug "30: afl_inputs/b[0x27] = #x00")
(executor-debug "30: afl_inputs/b[0x28] = #x00")
(executor-debug "30: afl_inputs/b[0x29] = #x00")
(executor-debug "30: afl_inputs/b[0x2A] = #x00")
(executor-debug "30: afl_inputs/b[0x2B] = #x00")
access granted
(executor-debug "0: Client is finished, master is resumed")
Ivan Gotovchits
@ivg
yay, welcome to the club)
mpmfrans
@mpmfrans
:D
Still, it is of importance that I find the correct value that granted us access. Preferably 445305947 not necessarily the pre-image.
Ivan Gotovchits
@ivg
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;
}
mpmfrans
@mpmfrans
For testing purposes and finding the right value.. should I convert the integers to a string and memcmp or strcmp them?
Ivan Gotovchits
@ivg
I didn't get the question? which integers?
mpmfrans
@mpmfrans
or maybe lower the cutoff and try branches less often
the gen_hash
Ivan Gotovchits
@ivg

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)
mpmfrans
@mpmfrans
aaaaah I see
so what the SE did output even if its not the exact number as we said.. multiple lead to the same hash..
Ivan Gotovchits
@ivg
yes, it outputs the input file
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 # 1276
here 0x1a8ad45b is your 445305947
mpmfrans
@mpmfrans
yes! that is the orig_hash
Ivan Gotovchits
@ivg
Also, with cutoff 1024 and timeout 1000 (1 sec) I get the result in a couple of seconds
mpmfrans
@mpmfrans
thank you!
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?
Ivan Gotovchits
@ivg
In fact, I can't confirm this anymore, so it looks like that I was just lucky. Unfortunately, z3 is not really deterministic
mpmfrans
@mpmfrans
I have to read about Z3 and what it is :)
Ivan Gotovchits
@ivg

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.

mpmfrans
@mpmfrans
@ivg thank you so much for all your help!
Ivan Gotovchits
@ivg
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)
mpmfrans
@mpmfrans
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")
mpmfrans
@mpmfrans
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

mpmfrans
@mpmfrans
jeeeeej, it worked :)
Ivan Gotovchits
@ivg
No, it is just generating random names for files)
Kenneth Adam Miller
@KennethAdamMiller
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)
Ivan Gotovchits
@ivg
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.
Kenneth Adam Miller
@KennethAdamMiller

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.

Kenneth Adam Miller
@KennethAdamMiller
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.
mpmfrans
@mpmfrans
@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?
mpmfrans
@mpmfrans
Ok so yes it is due to the getline(buf,len,stdin). If i comment this line the symbolic executor is running.
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?
mpmfrans
@mpmfrans
and therefore quits symbolically executing after only one fork?
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.
mpmfrans
@mpmfrans
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.