Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 14 additions & 8 deletions src/exploit/reportExploit.ml
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ open Transaction
open Feature
open ExecTran
open Semantics
open Sys

let event_lib =
"library SmarTest_event {" ^ "\n" ^
Expand Down Expand Up @@ -290,12 +291,13 @@ let get_rcv_eth : Z3.Model.model -> vformula -> string * string
let (rcv,eth) = get_rcv_eth' model sc in
(rcv,eth)

let mk_tx_output : int -> Query.kind -> int -> Z3.Model.model -> vformula -> (string * bool) BatSet.t -> (string * string) BatSet.t -> attack list -> Yojson.Basic.t list -> unit
= fun i kind loc model vc trusted invested attacks tx_json ->
let mk_tx_output : int -> Query.kind -> int -> Z3.Model.model -> vformula -> (string * bool) BatSet.t -> (string * string) BatSet.t -> attack list -> Yojson.Basic.t list -> string -> unit
= fun i kind loc model vc trusted invested attacks tx_json outdir ->
if not (Sys.file_exists outdir) then Sys.mkdir outdir 0o777;
let t_lst = List.map (fun (addr,b) -> (addr, `Bool b)) (BatSet.to_list trusted) in
let in_lst = List.map (fun (addr,eth) -> (addr, `String eth)) (BatSet.to_list invested) in
let (_,fbase) = BatString.replace (Filename.basename !inputfile) ".sol" "" in
let out = "./validation-files/" ^ fbase ^ "_" ^ Vocab.zfill 2 (string_of_int i) ^ ".json" in
let out = outdir ^ fbase ^ "_" ^ Vocab.zfill 2 (string_of_int i) ^ ".json" in
let f = open_out out in
let solc_ver = if !Options.solc_ver = "0.4" then "0.4.25" else !Options.solc_ver in
let this_address = eval_model model (snd this_addr) (vexp_to_z3exp (VVar this_addr)) in
Expand Down Expand Up @@ -352,11 +354,12 @@ let gen_wrapping_contract : Global.t -> string list -> string -> string
string_of_list ~first:"" ~last:"" ~sep:"\n" Vocab.id lines ^ "\n" ^ contract


let mk_test_sol : Global.t -> Query.kind -> int -> string list -> int -> string -> string -> string -> unit
= fun global kind i lines loc safety_cond attacker stolen_money ->
let mk_test_sol : Global.t -> Query.kind -> int -> string list -> int -> string -> string -> string -> string -> unit
= fun global kind i lines loc safety_cond attacker stolen_money outdir ->
if not (Sys.file_exists outdir) then Sys.mkdir outdir 0o777;
let (success,fbase) = BatString.replace (Filename.basename !inputfile) ".sol" "" in
let _ = assert success in
let out = "./validation-files/" ^ fbase ^ "_" ^ Vocab.zfill 2 (string_of_int i) ^ ".sol" in
let out = outdir ^ fbase ^ "_" ^ Vocab.zfill 2 (string_of_int i) ^ ".sol" in
if kind = ERC20 then
let _ = assert (loc < 0) in
let res = gen_wrapping_contract global lines safety_cond in
Expand Down Expand Up @@ -393,8 +396,9 @@ let report ~pathnum : Global.t -> QMap.t -> string list -> unit
let attacks,json = retrieve global tseq (remove_some mop) loc in
let trusted = get_trusted_account global tseq (remove_some mop) in
let invested = get_invested global tseq (remove_some mop) in
let _ = mk_tx_output (i+1) kind loc (remove_some mop) vc trusted invested attacks json in
let _ = mk_test_sol global kind (i+1) lines loc sc_src attacker_src stolen_eth_src in
let outdir = "./validation-files/" in
let _ = mk_tx_output (i+1) kind loc (remove_some mop) vc trusted invested attacks json outdir in
let _ = mk_test_sol global kind (i+1) lines loc sc_src attacker_src stolen_eth_src outdir in
print_endline (to_string_attacks attacks)
else print_endline ""
) vul_qs;
Expand All @@ -418,6 +422,8 @@ let report ~pathnum : Global.t -> QMap.t -> string list -> unit

let json : Global.t -> QMap.t -> unit
= fun global qmap ->
let outdir = "./output" in
if not (Sys.file_exists outdir) then Sys.mkdir outdir 0o777;
let vul_qs = QMap.bindings qmap in
let vul_found = List.filter (fun ((kind,_,_),(stat,_,_,_,_,_,_,_,_)) -> stat = Disproven) vul_qs in
let summary =
Expand Down