search

eth-sri / securify

[DEPRECATED] Security Scanner for Ethereum Smart Contracts
Apache License 2.0
217 stars 50 forks source link

Running docker image outputs "Error running securify." on macOS #69

Open mihairaulea opened 5 years ago

mihairaulea commented 5 years ago

Using a macOS Mojave. Docker is up to date.

➜ ~ docker version Client: Docker Engine - Community Version: 18.09.0 API version: 1.39 Go version: go1.10.4 Git commit: 4d60db4 Built: Wed Nov 7 00:47:43 2018 OS/Arch: darwin/amd64 Experimental: false

Server: Docker Engine - Community Engine: Version: 18.09.0 API version: 1.39 (minimum version 1.12) Go version: go1.10.4 Git commit: 4d60db4 Built: Wed Nov 7 00:55:00 2018 OS/Arch: linux/amd64 Experimental: true

I have cloned the securify git repository, and ran docker build . -t securify successfully. I have checked that the Docker image was built, and is available.

When running docker run securify as per the project documentation, i get

Error running securify.

Running with a mounted volume yields the same output. I am confident the volume had only one contract in it, which was successfully analyzed with other engines.

Error running securify.

hiqua commented 5 years ago

Hi @mihairaulea , thanks for the report!

Unfortunately I cannot reproduce this with the latest commit on the master branch, are you using the commit b54522ebb5515d9b69a72ac7589cbc2f7cd3d656 as I am?

mihairaulea commented 5 years ago

Hi @hiqua , yes, i am. Cloned the repo yesterday.

While building the image yesterday, had some issues(downloading soufle and other binaries), had to issue the command 3 times before a successful run. I have removed the image, and rebuilt it right now, with no luck.

mihairaulea commented 5 years ago

Okay, run with verbose.

➜  examples docker run -v $(pwd):/tmp securify -p=/tmp -v
Compiling project
Running Securify
Error running securify.
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
    at java.util.HashMap.resize(HashMap.java:704)
    at java.util.HashMap.putVal(HashMap.java:629)
    at java.util.HashMap.put(HashMap.java:612)
    at java.util.HashSet.add(HashSet.java:220)
    at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
    at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
    at ch.securify.analysis.MayImplicitDataflow.varMayDepOn(MayImplicitDataflow.java:49)
    at ch.securify.analysis.Dataflow.varMayDepOn(Dataflow.java:57)
    at ch.securify.patterns.MissingInputValidation.isCompliant(MissingInputValidation.java:96)
    at ch.securify.patterns.AbstractInstructionPattern.checkPattern(AbstractInstructionPattern.java:35)
    at ch.securify.Main.checkInstructions(Main.java:419)
    at ch.securify.Main.checkPatterns(Main.java:384)
    at ch.securify.Main.processHexFile(Main.java:178)
    at ch.securify.Main.processCompilationOutput(Main.java:120)
    at ch.securify.Main.mainFromCompilationOutput(Main.java:99)
    at ch.securify.Main.main(Main.java:229)
hiqua commented 5 years ago

How much memory do you have on your computer? OutOfMemoryError would indicate that you don't have enough.

hiqua commented 5 years ago

Also, docker build . does not require Soufflé.

mihairaulea commented 5 years ago

It seems the docker build requires Souffle. This is from the Dockerfile.

RUN mkdir /souffle
RUN wget -P /souffle/ https://github.com/souffle-lang/souffle/releases/download/1.4.0/souffle_1.4.0-1_amd64.deb &&\
        gdebi --n /souffle/souffle_1.4.0-1_amd64.deb

I have 16GB, should be enough :) Also, ran with docker run --memory=2g securify

hiqua commented 5 years ago

Yes, I meant that it is included in the Dockerfile so you shouldn't have to do anything in particular.

Did you also try without --memory=2g?

mihairaulea commented 5 years ago

Yes, tried without, as well.

hiqua commented 5 years ago

What is the RAM consumption at its peak?

hiqua commented 5 years ago

Maybe you can tell me more about the issues you had while building? Was it a network problem? Everything is downloaded from github, which is obviously not 100% resilient but you would have been quite unlucky to encounter issues right at that moment. What is the full docker build output?

mihairaulea commented 5 years ago

Yep, network problem when building the image, but it never happened again. Here is the output of running the docker image, with -v.

Processing contract: /project/example.sol:MarketPlace
  Attempt to decompile the contract with methods...
  Success. Inlining methods...
[MINL] found 3 methods
[MINL] processing method: method_abi_BC5A6C20
[MINL] processing method: method_abi_3155194C
[MINL] processing method: method_abi_C7961F2A
  Propagating constants...

Decompiled contract:
00:     a{Push}{0x80} = 0x80
02:     b{Push}{0x40} = 0x40
04:     mstore(memoffset: b{Push}{0x40}, value: a{Push}{0x80})
05:     c{Push}{0x04} = 0x04
07:     d{CallDataSize}{?} = calldatasize()
08:     e{CallDataSize|Push}{?} = (d{CallDataSize}{?} < c{Push}{0x04})
0C:     if e{CallDataSize|Push}{?}: goto tag_1 [merge @57]
0D:     h{Push}{0x00} = 0x00
0F:     i{Push|CallDataLoad}{?} = calldataload(h{Push}{0x00})
10:     j{Push}{0x0100000000000000000000000000000000000000000000000000000000} = 0x0100000000000000000000000000000000000000000000000000000000
2F:     k{Div|Push|CallDataLoad}{?} = i{Push|CallDataLoad}{?} / j{Push}{0x0100000000000000000000000000000000000000000000000000000000}
30:     l{Push}{0xFFFFFFFF} = 0xFFFFFFFF
35:     m{Div|Push|CallDataLoad}{?} = l{Push}{0xFFFFFFFF} & k{Div|Push|CallDataLoad}{?}
37:     n{Push}{0x3155194C} = 0x3155194C
3C:     o{Div|Push|CallDataLoad}{?} = (n{Push}{0x3155194C} == m{Div|Push|CallDataLoad}{?})
40:     if o{Div|Push|CallDataLoad}{?}: goto tag_2 [merge @5C]
42:     bl{Push}{0xBC5A6C20} = 0xBC5A6C20
47:     bm{Div|Push|CallDataLoad}{?} = (bl{Push}{0xBC5A6C20} == m{Div|Push|CallDataLoad}{?})
4B:     if bm{Div|Push|CallDataLoad}{?}: goto tag_5
4D:     cm{Push}{0xC7961F2A} = 0xC7961F2A
52:     cn{Div|Push|CallDataLoad}{?} = (cm{Push}{0xC7961F2A} == m{Div|Push|CallDataLoad}{?})
56:     if cn{Div|Push|CallDataLoad}{?}: goto tag_8
57:     tag_1: [from @0C]
58:     g{Push}{0x00} = 0x00
5B:     revert(memoffset: g{Push}{0x00}, length: g{Push}{0x00})
5C:     tag_2: [from @40]
5D:     q{CallValue}{?} = callvalue()
5F:     r{CallValue}{?} = !q{CallValue}{?}
63:     if r{CallValue}{?}: goto tag_3 [merge @68]
64:     bk{Push}{0x00} = 0x00
67:     revert(memoffset: bk{Push}{0x00}, length: bk{Push}{0x00})
68:     tag_3: [from @63]
70:     () = method_abi_3155194C()
72:     stop()
73:     tag_5: [from @4B]
74:     bo{CallValue}{?} = callvalue()
76:     bp{CallValue}{?} = !bo{CallValue}{?}
7A:     if bp{CallValue}{?}: goto tag_6 [merge @7F]
7B:     cl{Push}{0x00} = 0x00
7E:     revert(memoffset: cl{Push}{0x00}, length: cl{Push}{0x00})
7F:     tag_6: [from @7A]
87:     () = method_abi_BC5A6C20()
89:     stop()
8A:     tag_8: [from @56]
8B:     cp{CallValue}{?} = callvalue()
8D:     cq{CallValue}{?} = !cp{CallValue}{?}
91:     if cq{CallValue}{?}: goto tag_9 [merge @96]
92:     dl{Push}{0x00} = 0x00
95:     revert(memoffset: dl{Push}{0x00}, length: dl{Push}{0x00})
96:     tag_9: [from @91]
9E:     () = method_abi_C7961F2A()
A0:     stop()

DF:     method_abi_BC5A6C20()
E2:     bu{Address}{?} = address()
E3:     bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
F8:     bw{Address|Push}{?} = bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & bu{Address}{?}
F9:     bx{Address|Balance|Push}{?} = balance(address: bw{Address|Push}{?})
FC:     by{Caller|_AddressType}{?} = caller()
FD:     bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
112:    ca{Caller|_AddressType|Push}{?} = bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & by{Caller|_AddressType}{?}
113:    cb{Push}{0x08FC} = 0x08FC
119:    cc{Address|Balance|Push}{?} = !bx{Address|Balance|Push}{?}
11A:    cd{Address|Balance|Push}{?} = cc{Address|Balance|Push}{?} * cb{Push}{0x08FC}
11C:    ce{Push}{0x40} = 0x40
11E:    cf{Push}{0x80} = mload(memoffset: ce{Push}{0x40})
11F:    cg{Push}{0x00} = 0x00
121:    ch{Push}{0x40} = 0x40
123:    ci{Push}{0x80} = mload(memoffset: ch{Push}{0x40})
126:    cj{Push}{0x00} = cf{Push}{0x80} - ci{Push}{0x80}
12B:    ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
133:    return ()

A1:     method_abi_3155194C()
A4:     w{CallValue}{?} = callvalue()
A7:     x{Caller|_AddressType}{?} = caller()
A8:     y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
BD:     z{Caller|_AddressType|Push}{?} = y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & x{Caller|_AddressType}{?}
BE:     ba{Push}{0x08FC} = 0x08FC
C4:     bb{CallValue}{?} = !w{CallValue}{?}
C5:     bc{CallValue|Push}{?} = bb{CallValue}{?} * ba{Push}{0x08FC}
C7:     bd{Push}{0x40} = 0x40
C9:     be{Push}{0x80} = mload(memoffset: bd{Push}{0x40})
CA:     bf{Push}{0x00} = 0x00
CC:     bg{Push}{0x40} = 0x40
CE:     bh{Push}{0x80} = mload(memoffset: bg{Push}{0x40})
D1:     bi{Push}{0x00} = be{Push}{0x80} - bh{Push}{0x80}
D6:     bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
DE:     return ()

134:    method_abi_C7961F2A()
138:    cv{Push}{0x64} = 0x64
13C:    cw{Push}{0x64} = 0x64
13F:    cx{Push}{0x2710} = cv{Push}{0x64} * cw{Push}{0x64}
142:    cy{Caller|_AddressType}{?} = caller()
143:    cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
158:    da{Caller|_AddressType|Push}{?} = cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & cy{Caller|_AddressType}{?}
159:    db{Push}{0x08FC} = 0x08FC
15F:    dc{Push}{0x00} = !cx{Push}{0x2710}
160:    dd{Push}{0x00} = dc{Push}{0x00} * db{Push}{0x08FC}
162:    de{Push}{0x40} = 0x40
164:    df{Push}{0x80} = mload(memoffset: de{Push}{0x40})
165:    dg{Push}{0x00} = 0x00
167:    dh{Push}{0x40} = 0x40
169:    di{Push}{0x80} = mload(memoffset: dh{Push}{0x40})
16C:    dj{Push}{0x00} = df{Push}{0x80} - di{Push}{0x80}
171:    dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
17A:    return ()
  Verifying patterns...
Analyzing method with 19 instructions:

DF:     method_abi_BC5A6C20()
E2:     bu{Address}{?} = address()
E3:     bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
F8:     bw{Address|Push}{?} = bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & bu{Address}{?}
F9:     bx{Address|Balance|Push}{?} = balance(address: bw{Address|Push}{?})
FC:     by{Caller|_AddressType}{?} = caller()
FD:     bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
112:    ca{Caller|_AddressType|Push}{?} = bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & by{Caller|_AddressType}{?}
113:    cb{Push}{0x08FC} = 0x08FC
119:    cc{Address|Balance|Push}{?} = !bx{Address|Balance|Push}{?}
11A:    cd{Address|Balance|Push}{?} = cc{Address|Balance|Push}{?} * cb{Push}{0x08FC}
11C:    ce{Push}{0x40} = 0x40
11E:    cf{Push}{0x80} = mload(memoffset: ce{Push}{0x40})
11F:    cg{Push}{0x00} = 0x00
121:    ch{Push}{0x40} = 0x40
123:    ci{Push}{0x80} = mload(memoffset: ch{Push}{0x40})
126:    cj{Push}{0x00} = cf{Push}{0x80} - ci{Push}{0x80}
12B:    ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
133:    return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern DAOConstantGas: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Conflicts: 

Checking pattern MissingInputValidation: 
    Violations:
    Warnings: 
    Safe: method_abi_BC5A6C20()
    Conflicts: 

Checking pattern TODAmount: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern TODReceiver: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Conflicts: 

Checking pattern UnhandledException: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedEtherFlow: 
    Violations:
    Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedWrite: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Analyzing method with 16 instructions:

A1:     method_abi_3155194C()
A4:     w{CallValue}{?} = callvalue()
A7:     x{Caller|_AddressType}{?} = caller()
A8:     y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
BD:     z{Caller|_AddressType|Push}{?} = y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & x{Caller|_AddressType}{?}
BE:     ba{Push}{0x08FC} = 0x08FC
C4:     bb{CallValue}{?} = !w{CallValue}{?}
C5:     bc{CallValue|Push}{?} = bb{CallValue}{?} * ba{Push}{0x08FC}
C7:     bd{Push}{0x40} = 0x40
C9:     be{Push}{0x80} = mload(memoffset: bd{Push}{0x40})
CA:     bf{Push}{0x00} = 0x00
CC:     bg{Push}{0x40} = 0x40
CE:     bh{Push}{0x80} = mload(memoffset: bg{Push}{0x40})
D1:     bi{Push}{0x00} = be{Push}{0x80} - bh{Push}{0x80}
D6:     bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
DE:     return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern DAOConstantGas: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Conflicts: 

Checking pattern MissingInputValidation: 
    Violations:
    Warnings: 
    Safe: method_abi_BC5A6C20()
        method_abi_3155194C()
    Conflicts: 

Checking pattern TODAmount: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Warnings: bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Safe: 
    Conflicts: 

Checking pattern TODReceiver: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Conflicts: 

Checking pattern UnhandledException: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedEtherFlow: 
    Violations:
    Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedWrite: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Analyzing method with 18 instructions:

134:    method_abi_C7961F2A()
138:    cv{Push}{0x64} = 0x64
13C:    cw{Push}{0x64} = 0x64
13F:    cx{Push}{0x2710} = cv{Push}{0x64} * cw{Push}{0x64}
142:    cy{Caller|_AddressType}{?} = caller()
143:    cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
158:    da{Caller|_AddressType|Push}{?} = cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & cy{Caller|_AddressType}{?}
159:    db{Push}{0x08FC} = 0x08FC
15F:    dc{Push}{0x00} = !cx{Push}{0x2710}
160:    dd{Push}{0x00} = dc{Push}{0x00} * db{Push}{0x08FC}
162:    de{Push}{0x40} = 0x40
164:    df{Push}{0x80} = mload(memoffset: de{Push}{0x40})
165:    dg{Push}{0x00} = 0x00
167:    dh{Push}{0x40} = 0x40
169:    di{Push}{0x80} = mload(memoffset: dh{Push}{0x40})
16C:    dj{Push}{0x00} = df{Push}{0x80} - di{Push}{0x80}
171:    dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
17A:    return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern DAOConstantGas: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
        dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
    Conflicts: 

Checking pattern MissingInputValidation: 
    Violations:
    Warnings: 
    Safe: method_abi_BC5A6C20()
        method_abi_3155194C()
        method_abi_C7961F2A()
    Conflicts: 

Checking pattern TODAmount: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Warnings: bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Safe: dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
    Conflicts: 

Checking pattern TODReceiver: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
        dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
    Conflicts: 

Checking pattern UnhandledException: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
        dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedEtherFlow: 
    Violations:dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
    Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedWrite: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Computing global dataflow fixpoint over the entire contract...

Checking pattern LockedEther: 
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
    at java.util.HashMap.resize(HashMap.java:704)
    at java.util.HashMap.putVal(HashMap.java:629)
    at java.util.HashMap.put(HashMap.java:612)
    at java.util.HashSet.add(HashSet.java:220)
    at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
    at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
    at ch.securify.analysis.MustExplicitDataflow.varMustDepOn(MustExplicitDataflow.java:54)
    at ch.securify.analysis.Dataflow.varMustDepOn(Dataflow.java:97)
    at ch.securify.patterns.LockedEther.isSafe(LockedEther.java:45)
    at ch.securify.patterns.AbstractContractPattern.checkPattern(AbstractContractPattern.java:34)
    at ch.securify.Main.checkInstructions(Main.java:423)
    at ch.securify.Main.checkPatterns(Main.java:404)
    at ch.securify.Main.processHexFile(Main.java:174)
    at ch.securify.Main.processCompilationOutput(Main.java:121)
    at ch.securify.Main.mainFromCompilationOutput(Main.java:101)
    at ch.securify.Main.main(Main.java:233)
Error running Securify
mihairaulea commented 5 years ago

I bet you have a memory leak, investigating.

mihairaulea commented 5 years ago

Modified project.py, allocated 4GB of heap memory(hardcoded).

Line 79 in project.py

cmd = ["java", f"-Xmx4G", "-jar", str(self.securify_jar),

Here is the output now:

Processing contract: /project/example.sol:MarketPlace
  Attempt to decompile the contract with methods...
  Success. Inlining methods...
[MINL] found 3 methods
[MINL] processing method: method_abi_BC5A6C20
[MINL] processing method: method_abi_3155194C
[MINL] processing method: method_abi_C7961F2A
  Propagating constants...

Decompiled contract:
00:     a{Push}{0x80} = 0x80
02:     b{Push}{0x40} = 0x40
04:     mstore(memoffset: b{Push}{0x40}, value: a{Push}{0x80})
05:     c{Push}{0x04} = 0x04
07:     d{CallDataSize}{?} = calldatasize()
08:     e{CallDataSize|Push}{?} = (d{CallDataSize}{?} < c{Push}{0x04})
0C:     if e{CallDataSize|Push}{?}: goto tag_1 [merge @57]
0D:     h{Push}{0x00} = 0x00
0F:     i{Push|CallDataLoad}{?} = calldataload(h{Push}{0x00})
10:     j{Push}{0x0100000000000000000000000000000000000000000000000000000000} = 0x0100000000000000000000000000000000000000000000000000000000
2F:     k{Div|Push|CallDataLoad}{?} = i{Push|CallDataLoad}{?} / j{Push}{0x0100000000000000000000000000000000000000000000000000000000}
30:     l{Push}{0xFFFFFFFF} = 0xFFFFFFFF
35:     m{Div|Push|CallDataLoad}{?} = l{Push}{0xFFFFFFFF} & k{Div|Push|CallDataLoad}{?}
37:     n{Push}{0x3155194C} = 0x3155194C
3C:     o{Div|Push|CallDataLoad}{?} = (n{Push}{0x3155194C} == m{Div|Push|CallDataLoad}{?})
40:     if o{Div|Push|CallDataLoad}{?}: goto tag_2 [merge @5C]
42:     bl{Push}{0xBC5A6C20} = 0xBC5A6C20
47:     bm{Div|Push|CallDataLoad}{?} = (bl{Push}{0xBC5A6C20} == m{Div|Push|CallDataLoad}{?})
4B:     if bm{Div|Push|CallDataLoad}{?}: goto tag_5
4D:     cm{Push}{0xC7961F2A} = 0xC7961F2A
52:     cn{Div|Push|CallDataLoad}{?} = (cm{Push}{0xC7961F2A} == m{Div|Push|CallDataLoad}{?})
56:     if cn{Div|Push|CallDataLoad}{?}: goto tag_8
57:     tag_1: [from @0C]
58:     g{Push}{0x00} = 0x00
5B:     revert(memoffset: g{Push}{0x00}, length: g{Push}{0x00})
5C:     tag_2: [from @40]
5D:     q{CallValue}{?} = callvalue()
5F:     r{CallValue}{?} = !q{CallValue}{?}
63:     if r{CallValue}{?}: goto tag_3 [merge @68]
64:     bk{Push}{0x00} = 0x00
67:     revert(memoffset: bk{Push}{0x00}, length: bk{Push}{0x00})
68:     tag_3: [from @63]
70:     () = method_abi_3155194C()
72:     stop()
73:     tag_5: [from @4B]
74:     bo{CallValue}{?} = callvalue()
76:     bp{CallValue}{?} = !bo{CallValue}{?}
7A:     if bp{CallValue}{?}: goto tag_6 [merge @7F]
7B:     cl{Push}{0x00} = 0x00
7E:     revert(memoffset: cl{Push}{0x00}, length: cl{Push}{0x00})
7F:     tag_6: [from @7A]
87:     () = method_abi_BC5A6C20()
89:     stop()
8A:     tag_8: [from @56]
8B:     cp{CallValue}{?} = callvalue()
8D:     cq{CallValue}{?} = !cp{CallValue}{?}
91:     if cq{CallValue}{?}: goto tag_9 [merge @96]
92:     dl{Push}{0x00} = 0x00
95:     revert(memoffset: dl{Push}{0x00}, length: dl{Push}{0x00})
96:     tag_9: [from @91]
9E:     () = method_abi_C7961F2A()
A0:     stop()

DF:     method_abi_BC5A6C20()
E2:     bu{Address}{?} = address()
E3:     bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
F8:     bw{Address|Push}{?} = bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & bu{Address}{?}
F9:     bx{Address|Balance|Push}{?} = balance(address: bw{Address|Push}{?})
FC:     by{Caller|_AddressType}{?} = caller()
FD:     bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
112:    ca{Caller|_AddressType|Push}{?} = bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & by{Caller|_AddressType}{?}
113:    cb{Push}{0x08FC} = 0x08FC
119:    cc{Address|Balance|Push}{?} = !bx{Address|Balance|Push}{?}
11A:    cd{Address|Balance|Push}{?} = cc{Address|Balance|Push}{?} * cb{Push}{0x08FC}
11C:    ce{Push}{0x40} = 0x40
11E:    cf{Push}{0x80} = mload(memoffset: ce{Push}{0x40})
11F:    cg{Push}{0x00} = 0x00
121:    ch{Push}{0x40} = 0x40
123:    ci{Push}{0x80} = mload(memoffset: ch{Push}{0x40})
126:    cj{Push}{0x00} = cf{Push}{0x80} - ci{Push}{0x80}
12B:    ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
133:    return ()

A1:     method_abi_3155194C()
A4:     w{CallValue}{?} = callvalue()
A7:     x{Caller|_AddressType}{?} = caller()
A8:     y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
BD:     z{Caller|_AddressType|Push}{?} = y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & x{Caller|_AddressType}{?}
BE:     ba{Push}{0x08FC} = 0x08FC
C4:     bb{CallValue}{?} = !w{CallValue}{?}
C5:     bc{CallValue|Push}{?} = bb{CallValue}{?} * ba{Push}{0x08FC}
C7:     bd{Push}{0x40} = 0x40
C9:     be{Push}{0x80} = mload(memoffset: bd{Push}{0x40})
CA:     bf{Push}{0x00} = 0x00
CC:     bg{Push}{0x40} = 0x40
CE:     bh{Push}{0x80} = mload(memoffset: bg{Push}{0x40})
D1:     bi{Push}{0x00} = be{Push}{0x80} - bh{Push}{0x80}
D6:     bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
DE:     return ()

134:    method_abi_C7961F2A()
138:    cv{Push}{0x64} = 0x64
13C:    cw{Push}{0x64} = 0x64
13F:    cx{Push}{0x2710} = cv{Push}{0x64} * cw{Push}{0x64}
142:    cy{Caller|_AddressType}{?} = caller()
143:    cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
158:    da{Caller|_AddressType|Push}{?} = cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & cy{Caller|_AddressType}{?}
159:    db{Push}{0x08FC} = 0x08FC
15F:    dc{Push}{0x00} = !cx{Push}{0x2710}
160:    dd{Push}{0x00} = dc{Push}{0x00} * db{Push}{0x08FC}
162:    de{Push}{0x40} = 0x40
164:    df{Push}{0x80} = mload(memoffset: de{Push}{0x40})
165:    dg{Push}{0x00} = 0x00
167:    dh{Push}{0x40} = 0x40
169:    di{Push}{0x80} = mload(memoffset: dh{Push}{0x40})
16C:    dj{Push}{0x00} = df{Push}{0x80} - di{Push}{0x80}
171:    dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
17A:    return ()
  Verifying patterns...
Analyzing method with 19 instructions:

DF:     method_abi_BC5A6C20()
E2:     bu{Address}{?} = address()
E3:     bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
F8:     bw{Address|Push}{?} = bv{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & bu{Address}{?}
F9:     bx{Address|Balance|Push}{?} = balance(address: bw{Address|Push}{?})
FC:     by{Caller|_AddressType}{?} = caller()
FD:     bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
112:    ca{Caller|_AddressType|Push}{?} = bz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & by{Caller|_AddressType}{?}
113:    cb{Push}{0x08FC} = 0x08FC
119:    cc{Address|Balance|Push}{?} = !bx{Address|Balance|Push}{?}
11A:    cd{Address|Balance|Push}{?} = cc{Address|Balance|Push}{?} * cb{Push}{0x08FC}
11C:    ce{Push}{0x40} = 0x40
11E:    cf{Push}{0x80} = mload(memoffset: ce{Push}{0x40})
11F:    cg{Push}{0x00} = 0x00
121:    ch{Push}{0x40} = 0x40
123:    ci{Push}{0x80} = mload(memoffset: ch{Push}{0x40})
126:    cj{Push}{0x00} = cf{Push}{0x80} - ci{Push}{0x80}
12B:    ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
133:    return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern DAOConstantGas: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Conflicts: 

Checking pattern MissingInputValidation: 
    Violations:
    Warnings: 
    Safe: method_abi_BC5A6C20()
    Conflicts: 

Checking pattern TODAmount: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern TODReceiver: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Conflicts: 

Checking pattern UnhandledException: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedEtherFlow: 
    Violations:
    Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedWrite: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Analyzing method with 16 instructions:

A1:     method_abi_3155194C()
A4:     w{CallValue}{?} = callvalue()
A7:     x{Caller|_AddressType}{?} = caller()
A8:     y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
BD:     z{Caller|_AddressType|Push}{?} = y{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & x{Caller|_AddressType}{?}
BE:     ba{Push}{0x08FC} = 0x08FC
C4:     bb{CallValue}{?} = !w{CallValue}{?}
C5:     bc{CallValue|Push}{?} = bb{CallValue}{?} * ba{Push}{0x08FC}
C7:     bd{Push}{0x40} = 0x40
C9:     be{Push}{0x80} = mload(memoffset: bd{Push}{0x40})
CA:     bf{Push}{0x00} = 0x00
CC:     bg{Push}{0x40} = 0x40
CE:     bh{Push}{0x80} = mload(memoffset: bg{Push}{0x40})
D1:     bi{Push}{0x00} = be{Push}{0x80} - bh{Push}{0x80}
D6:     bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
DE:     return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern DAOConstantGas: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Conflicts: 

Checking pattern MissingInputValidation: 
    Violations:
    Warnings: 
    Safe: method_abi_BC5A6C20()
        method_abi_3155194C()
    Conflicts: 

Checking pattern TODAmount: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
    Warnings: bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Safe: 
    Conflicts: 

Checking pattern TODReceiver: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Conflicts: 

Checking pattern UnhandledException: 
    Violations:ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedEtherFlow: 
    Violations:
    Warnings: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
    Safe: 
    Conflicts: 

Checking pattern UnrestrictedWrite: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Analyzing method with 18 instructions:

134:    method_abi_C7961F2A()
138:    cv{Push}{0x64} = 0x64
13C:    cw{Push}{0x64} = 0x64
13F:    cx{Push}{0x2710} = cv{Push}{0x64} * cw{Push}{0x64}
142:    cy{Caller|_AddressType}{?} = caller()
143:    cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
158:    da{Caller|_AddressType|Push}{?} = cz{Push}{0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF} & cy{Caller|_AddressType}{?}
159:    db{Push}{0x08FC} = 0x08FC
15F:    dc{Push}{0x00} = !cx{Push}{0x2710}
160:    dd{Push}{0x00} = dc{Push}{0x00} * db{Push}{0x08FC}
162:    de{Push}{0x40} = 0x40
164:    df{Push}{0x80} = mload(memoffset: de{Push}{0x40})
165:    dg{Push}{0x00} = 0x00
167:    dh{Push}{0x40} = 0x40
169:    di{Push}{0x80} = mload(memoffset: dh{Push}{0x40})
16C:    dj{Push}{0x00} = df{Push}{0x80} - di{Push}{0x80}
171:    dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
17A:    return ()
Computing dataflow fixpoint over the method body...

Checking pattern DAO: 
    Violations:
    Warnings: 
    Safe: 
    Conflicts: 

Checking pattern DAOConstantGas: 
    Violations:
    Warnings: 
    Safe: ck{Address|Balance|Caller|Call|_AddressType|Push}{?} = call(gas: cd{Address|Balance|Push}{?}, to_addr: ca{Caller|_AddressType|Push}{?}, value: bx{Address|Balance|Push}{?}, in_offset: ci{Push}{0x80}, in_size: cj{Push}{0x00}, out_offset: ci{Push}{0x80}, out_size: cg{Push}{0x00})
        bj{Caller|Call|_AddressType|CallValue|Push}{?} = call(gas: bc{CallValue|Push}{?}, to_addr: z{Caller|_AddressType|Push}{?}, value: w{CallValue}{?}, in_offset: bh{Push}{0x80}, in_size: bi{Push}{0x00}, out_offset: bh{Push}{0x80}, out_size: bf{Push}{0x00})
        dk{Caller|Call|_AddressType|Push}{?} = call(gas: dd{Push}{0x00}, to_addr: da{Caller|_AddressType|Push}{?}, value: cx{Push}{0x2710}, in_offset: di{Push}{0x80}, in_size: dj{Push}{0x00}, out_offset: di{Push}{0x80}, out_size: dg{Push}{0x00})
    Conflicts: 

Checking pattern MissingInputValidation: 
    Violations:
    Warnings: 
    Safe: method_abi_BC5A6C20()
        method_abi_3155194C()
        method_abi_C7961F2A()
    Conflicts: 

Checking pattern TODAmount: 
Error running Securify
hiqua commented 5 years ago

It's very possible that there's a memory leak (actually I'd be surprised if there isn't any!), but I still don't understand why I cannot reproduce this. How big is your swap partition? I have 16GB of memory and my swap is 16GB.

mihairaulea commented 5 years ago

Try with docker system prune -a . Re memory: exactly same config. Thanks for the time and patience so far.

hiqua commented 5 years ago

I ran your command, but I still cannot reproduce your bug after building the image from scratch. It runs fine with 11GB available in memory, and an empty swap.

charles-lei commented 5 years ago

@mihairaulea I have met the same issue, do you have any new discoveries?

0x3bfc commented 5 years ago

I am experiencing the same issue: Truffle version: v5.0.0 Solc version: 0.4.25 Docker version 18.09.0

ahmeds-mbp-2:securify ahmed$ docker run --memory=16g -v $(pwd):/project securify
Compiling project
Running Securify
Processing contract: /project/contracts/Migrations.sol:Migrations
  Attempt to decompile the contract with methods...
  Success. Inlining methods...
  Propagating constants...
  Verifying patterns...
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
    at java.util.HashMap.resize(HashMap.java:704)
    at java.util.HashMap.putVal(HashMap.java:629)
    at java.util.HashMap.put(HashMap.java:612)
    at java.util.HashSet.add(HashSet.java:220)
    at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
    at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
    at ch.securify.analysis.MayImplicitDataflow.mayFollow(MayImplicitDataflow.java:44)
    at ch.securify.analysis.Dataflow.mayFollow(Dataflow.java:49)
    at ch.securify.patterns.MissingInputValidation.isViolation(MissingInputValidation.java:67)
    at ch.securify.patterns.AbstractInstructionPattern.checkPattern(AbstractInstructionPattern.java:38)
    at ch.securify.Main.checkInstructions(Main.java:443)
    at ch.securify.Main.checkPatterns(Main.java:408)
    at ch.securify.Main.processHexFile(Main.java:185)
    at ch.securify.Main.processCompilationOutput(Main.java:132)
    at ch.securify.Main.mainFromCompilationOutput(Main.java:108)
    at ch.securify.Main.main(Main.java:244)
Error running Securify
hiqua commented 5 years ago

@aabdulwahed you're using macOS right? And @charles-lei as well?

I don't, so that could explain why I cannot reproduce it. I'm not sure what the root issue is for now though.

charles-lei commented 5 years ago

yes, I'm using macOS and docker toolbox OS version: Mojave 10.14

0x3bfc commented 5 years ago

Thanks @hiqua for swift reply, yes I am using MacOS.. Does it work for Ubuntu 18.04 LTS ?

hiqua commented 5 years ago

@aabdulwahed it works for me on Debian, I assume it will work on Ubuntu as well. It really seems to be related to macOS or at least to Docker on macOS.

0x3bfc commented 5 years ago

@hiqua thanks, I will move to Ubuntu

mihairaulea commented 5 years ago

Seems to be related to MacOS, specifically Mojave. okay, will run in a vm.

Ramarti commented 5 years ago

Same here.

Mac Os Mojave: 10.14 Docker Desktop Community Version 2.0.0.2 (30215) Truffle version: 4.1.15 (changed in Dockerfile)

platform-contracts git:(earlyreturn) docker run --memory=16g -v $(pwd):/project securify --truffle
Compiling project
Running Securify
Processing contract: /project/contracts/user/EthicHubUser.sol:EthicHubUser
  Attempt to decompile the contract with methods...
  Failed to decompile methods. Attempt to decompile the contract without identifying methods...
  Propagating constants...
  Verifying patterns...
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
    at java.util.HashMap.resize(HashMap.java:704)
    at java.util.HashMap.putVal(HashMap.java:629)
    at java.util.HashMap.put(HashMap.java:612)
    at java.util.HashSet.add(HashSet.java:220)
    at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
    at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
    at ch.securify.analysis.MustExplicitDataflow.mustPrecede(MustExplicitDataflow.java:44)
    at ch.securify.analysis.Dataflow.mustPrecede(Dataflow.java:89)
    at ch.securify.patterns.LockedEther.isSafe(LockedEther.java:54)
    at ch.securify.patterns.AbstractContractPattern.checkPattern(AbstractContractPattern.java:38)
    at ch.securify.Main.checkInstructions(Main.java:443)
    at ch.securify.Main.checkPatterns(Main.java:388)
    at ch.securify.Main.processHexFile(Main.java:185)
    at ch.securify.Main.processCompilationOutput(Main.java:132)
    at ch.securify.Main.mainFromCompilationOutput(Main.java:108)
    at ch.securify.Main.main(Main.java:244)
Error running Securify
instabridge-thomas commented 5 years ago

Ditto

Truffle: 5.0.1 Docker: Community 18.09.1 MacOSX: 10.14.2

ThomasTGWUTWAs-MacBook-Pro:smart-contracts thomasinstabridge$ docker run -v $(pwd) --memory=16g chainsecurity/securify
Compiling project
Running Securify
Processing contract: /project/example.sol:MarketPlace
  Attempt to decompile the contract with methods...
  Success. Inlining methods...
  Propagating constants...
  Verifying patterns...
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
    at java.util.HashMap.resize(HashMap.java:704)
    at java.util.HashMap.putVal(HashMap.java:629)
    at java.util.HashMap.put(HashMap.java:612)
    at java.util.HashSet.add(HashSet.java:220)
    at ch.securify.analysis.AbstractDataflow.readFixedpoint(AbstractDataflow.java:217)
    at ch.securify.analysis.AbstractDataflow.runQuery(AbstractDataflow.java:226)
    at ch.securify.analysis.MustExplicitDataflow.varMustDepOn(MustExplicitDataflow.java:54)
    at ch.securify.analysis.Dataflow.varMustDepOn(Dataflow.java:97)
    at ch.securify.patterns.TODAmount.isViolation(TODAmount.java:56)
    at ch.securify.patterns.AbstractInstructionPattern.checkPattern(AbstractInstructionPattern.java:38)
    at ch.securify.Main.checkInstructions(Main.java:443)
    at ch.securify.Main.checkPatterns(Main.java:408)
    at ch.securify.Main.processHexFile(Main.java:185)
    at ch.securify.Main.processCompilationOutput(Main.java:132)
    at ch.securify.Main.mainFromCompilationOutput(Main.java:108)
    at ch.securify.Main.main(Main.java:244)
Error running Securify
hiqua commented 5 years ago

If those having problems with macOS can try with a VM on Ubuntu and see whether they have the same problems, that'd be great! So far I haven't seen anyone claiming that they could reproduce this issue on an OS different from macOS.