Commit 0f738968 authored by Richard Bonichon's avatar Richard Bonichon
Browse files

Release BINSEC 0.2

parent 15841241
* 0.2 [2018-07-23 Mon]
* 0.2 [2018-10-01 Mon]
- New symbolic execution engine
- New interpreter for binary code
- Improved logical representation for formulas
- New internal control-flow-graph representation
- Action language for symbolic execution goals
- Directive language for symbolic execution control
- Support for new PIN tool xtrasec
- Improved x86 decoder
- Fixed bugs reported by KAIST
- Docker support
- includes Unisim-vp ARM v7 decoder
- includes Unisim-vp ARM v7 decoder
- includes new PIN tool xtrasec
* 0.1 [2017-03-01 Wed]
......
......@@ -26,7 +26,11 @@ CAMLLEXOPTS ?=
CAMLYAC ?=@MENHIR@
CAMLYACOPTS ?=
CAMLDEP ?=@OCAMLDEP@
CAMLWARNINGS ?=-w +a-4-3-18
# Rationale for warning exclusions:
# - 42 is only valid in OCaml < 4.00
# - 4 fragile pattern matching is authorized (can be hard to remove on big ASTs)
# - 3 deprecated feature are ok (sometimes you have a newer compiler than older supported version)
CAMLWARNINGS ?=-w +a-4-3-42
CAMLFLAGS ?=-g -bin-annot
CAMLDOC ?=@OCAMLDOC@
CAMLFIND ?=@OCAMLFIND@
......
0.2beta
\ No newline at end of file
0.2
\ No newline at end of file
......@@ -66,4 +66,4 @@ depends: [
"llvm"
]
available: [ ocaml-version >= "4.04.2" ]
available: [ ocaml-version >= "4.04.2" & ocaml_version < "4.06.0"]
......@@ -51,9 +51,9 @@ BINSEC_LICENSE_CEA += $(DBA_FILES)
UTILS_DIR = utils
UTILS_SRC_FILES = \
action \
colors \
binary_loc \
directive \
cfg \
dhunk \
instruction \
......@@ -67,8 +67,10 @@ UTILS_MLI_FILES = \
BASE_DIR = base
BASE_SRC_FILES = \
logger \
base_logger \
bigint string_utils \
logger fstack \
fstack \
natural \
hashamt \
basic_types \
......@@ -80,7 +82,7 @@ BASE_SRC_FILES = \
mnemonic \
virtual_address \
cli \
list_utils print_utils file_utils \
list_utils print_utils file_utils array_utils \
machine \
worklist \
utils
......@@ -237,6 +239,7 @@ FORMULA_SRC_FILES = \
formula_to_smtlib \
smtlib_to_formula \
formula_pp \
prover \
formula_transformation solver \
formula_main
FORMULA_INT_FILES = $(FORMULA_SRC_FILES)
......@@ -298,7 +301,7 @@ BINSEC_LICENSE_CEA += $(SMT_FILES)
KERNEL_DIR = kernel
# KERNEL_OPTIONS = kernel_options
KERNEL_SRC_FILES = kernel_options kernel_functions kernel_core
KERNEL_SRC_FILES = kernel_options kernel_functions kernel_core
KERNEL_ML_FILES = $(KERNEL_SRC_FILES:%=$(KERNEL_DIR)/%.ml)
KERNEL_MLI_FILES = \
$(KERNEL_ML_FILES:%.ml=%.mli) \
......@@ -469,8 +472,8 @@ EXAMPLE_ML_FILES = $(EXAMPLE_SRC_FILES:%=$(EXAMPLE_DIR)/%.ml)
EXAMPLE_MLI_FILES = $(EXAMPLE_INT_FILES:%=$(EXAMPLE_DIR)/%.mli)
EXAMPLE_FILES = $(EXAMPLE_ML_FILES) $(EXAMPLE_MLI_FILES)
# Not added to BINSEC_DISTRIB_FILES: they are added
# through DYNAMIC_ML_FILES and DYNAMIC_MLI_FILES
# Not added to BINSEC_DISTRIB_FILES: they are added
# through DYNAMIC_ML_FILES and DYNAMIC_MLI_FILES
BINSEC_LICENSE_CEA += $(EXAMPLE_FILES)
......@@ -559,7 +562,7 @@ DPATH_SRC_FILES = \
dse
DPATH_INT_FILES = \
typeCriteriaDSE typeGuideDSE typeHistoryDSE typeTraceDSE \
guideAsPriority guideAsShortestPath
guideAsPriority guideAsShortestPath
DPATH_ML_FILES = $(DPATH_SRC_FILES:%=$(DPATH_DIR)/%.ml)
DPATH_MLI_FILES = \
$(DPATH_INT_FILES:%=$(DPATH_DIR)/%.mli) \
......@@ -682,7 +685,24 @@ BW_FILES = \
BINSEC_DISTRIB_FILES += $(BW_FILES)
BINSEC_LICENSE_CEA += $(BW_FILES)
###
# Xtrasec
##
XTRASEC_DIR = xtrasec
OPTION_FILES += $(XTRASEC_DIR)/xtrasec_options
XTRASEC_SRC_FILES = \
parsepin formula_decoder xtrasec
XTRASEC_INT_FILES = $(XTRASEC_SRC_FILES)
XTRASEC_ML_FILES = $(XTRASEC_SRC_FILES:%=$(XTRASEC_DIR)/%.ml)
XTRASEC_MLI_FILES = $(XTRASEC_INT_FILES:%=$(XTRASEC_DIR)/%.mli)
XTRASEC_FILES = \
$(XTRASEC_ML_FILES) \
$(XTRASEC_MLI_FILES)
BINSEC_DISTRIB_FILES += $(XTRASEC_FILES)
BINSEC_LICENSE_CEA += $(XTRASEC_FILES)
# Server
SERVER_DIR = server
......@@ -826,6 +846,7 @@ LIB_ML_FILES = \
$(DYNAMIC_ML_FILES) \
$(SERVER_ML_FILES) \
$(SSE_ML_FILES) \
$(XTRASEC_ML_FILES) \
$(BW_ML_FILES) \
$(BINPATCHER_ML_FILES)
......@@ -852,6 +873,7 @@ LIB_MLI_FILES = \
$(LLVM_MLI_FILES) \
$(SERVER_MLI_FILES) \
$(SSE_MLI_FILES) \
$(XTRASEC_MLI_FILES) \
$(BW_MLI_FILES) \
$(BINPATCHER_MLI_FILES) \
$(ROOT_MLI_FILES) \
......@@ -902,6 +924,7 @@ DIRS = \
$(BINPATCHER_DIR) \
$(SSE_DIR) \
$(BW_DIR) \
$(XTRASEC_DIR) \
$(KERNEL_DIR)
CAMLINCLUDES = $(DIRS:%=-I %) -I .
......
......@@ -5,6 +5,7 @@ not <piqi/**> : warn(A-4-48)
<ast/**> : include
<base/**> : include
<binpatcher/**> : include
<backwards/**> : include
<dba/**> : include
<disasm/**> : include, inline(10000)
<dynamic/**> : include, package(piqilib,piqirun.ext)
......@@ -15,6 +16,7 @@ not <piqi/**> : warn(A-4-48)
<parser/**> : include
<piqi/**> : include, package(piqilib,piqirun.ext), warn(A-27)
<server/**> : include, package(piqilib,piqirun.ext)
<pintrace/**> : include
<smtlib/**> : include
<sse/**> : include
<static/**> : include
......
......@@ -111,32 +111,6 @@ let make inst_map djumps_map =
in Caddress.Map.fold build_aux inst_map Caddress.Map.empty
(* FIXME : unused *)
let _display_ast ast =
let pp_set fmt addrset =
Dba_types.Caddress.Set.iter
(fun caddress ->
Format.fprintf fmt "%a,@ " Dba_printer.Ascii.pp_code_address caddress)
addrset
in
let f addr stmt =
Logger.info
"@[<v 2>%a %a:@ \
preds: @[<hov 0>%a@]@ \
succs: @[<hov 0>%a@]@ \
closed: %s@ \
binstr: TODO@ \
@]"
Dba_printer.Ascii.pp_code_address addr
Dba_printer.Ascii.pp_instruction stmt.instr
pp_set stmt.preds
pp_set stmt.succs
(string_of_bool stmt.closed_succs)
;
in Dba_types.Caddress.Map.iter f ast
let build_sequences_map ast l0 dba_display =
let ast = ref ast in
......
......@@ -75,6 +75,3 @@ module Dot = struct
close_out oc
end
......@@ -32,150 +32,207 @@ module Value = struct
let equal i1 i2 = i1 = i2
end
module G = Cfg.Make(Key)(Value)
(struct
type t = string
let hash s = Hashtbl.hash s
let equal s1 s2 = s1 = s2
end)
include G
type block = {
leader: V.t;
block : V.t list;
succs : V.t list;
preds : V.t list;
}
module D = Graph.Imperative.Digraph.ConcreteBidirectional
(struct
type t = block
let compare b1 b2 = V.compare b1.leader b2.leader
let hash b = V.hash b.leader
let equal b1 b2 = V.equal b1.leader b2.leader
end)
module L = Graph.Leaderlist.Make(G)
module H = Hashtbl.Make(V)
let get_pred t v =
match pred t v with
| [v] -> Some v
| _ -> None
let get_succ t v =
match succ t v with
| [v] -> Some v
| _ -> None
let rec compare_preds_succs g v pred succ =
match pred, succ with
| None, None -> assert false
| Some _, None -> -1
| None, Some _ -> 1
| Some p, Some s ->
if V.equal v p then -1
else if V.equal v s then 1
else compare_preds_succs g v (get_pred g p) (get_succ g s)
let compare_vertex g v1 v2 =
if G.V.equal v1 v2 then 0
else compare_preds_succs g v1 (get_pred g v2) (get_succ g v2)
let rec diff lst1 lst2 acc =
match lst1, lst2 with
| ls, [] -> List.rev_append ls acc
| [], _ -> acc
| a1 :: ls1, a2 :: ls2 ->
if G.V.compare a1 a2 < 0 then diff ls1 lst2 (a1 :: acc)
else if G.V.compare a1 a2 > 0 then diff lst1 ls2 acc
else diff ls1 ls2 acc
let diff lst1 lst2 = List.rev (diff lst1 lst2 [])
let build_block g block =
let succs,preds =
List.fold_left
(fun (succs, preds) v ->
List.fold_left (fun l e -> e :: l) succs (succ g v),
List.fold_left (fun l e -> e :: l) preds (pred g v))
([], []) block
in
let block = List.sort_uniq V.compare block in
let succs = diff (List.sort_uniq V.compare succs) block in
let preds = diff (List.sort_uniq V.compare preds) block in
let block = List.sort_uniq (compare_vertex g) block in
{ leader = List.hd block; block; succs; preds }
let build_block_graph cfg entry =
let blocks = List.map (build_block cfg) (L.leader_lists cfg entry) in
let htbl = H.create 17 in
List.iter (fun b -> List.iter (fun v -> H.add htbl v b) b.block) blocks;
let t = D.create () in
List.iter
(fun block ->
let vertex = D.V.create block in
D.add_vertex t vertex;
List.iter
(fun succ -> D.add_edge t vertex (H.find htbl succ))
block.succs;
List.iter
(fun pred -> D.add_edge t (H.find htbl pred) vertex)
block.preds)
blocks;
t
let html_block callees block =
let open Format in
let align = "align=\"left\"" in
let border = "border=\"1\"" in
let open Colors in
let color1 = asprintf "bgcolor=\"%a\"" pp FlatUI.greensea in
let color2 = asprintf "bgcolor=\"%a\"" pp FlatUI.silver in
let pp_mnemonic ppf vert =
match V.inst vert with
| None -> ()
| Some inst ->
let a = inst.Instruction.address in
let m = inst.Instruction.mnemonic in
if List.mem a callees then
fprintf ppf "<font color=\"%a\">%a</font>" pp FlatUI.alizarin Mnemonic.pp m
else Mnemonic.pp ppf m
in
block.block
|> List.map
(fun vert ->
asprintf "<tr><td %s %s>0x%x</td><td %s %s %s>%a</td></tr>"
border color1 (V.addr vert :> int)
border color2 align pp_mnemonic vert)
|> String.concat "\n"
|> sprintf "<table border=\"0\" cellspacing=\"0\">\n%s\n</table>"
let output_graph c g ~entry ca =
let g = build_block_graph g entry in
let module Dot =
struct
include Graph.Graphviz.Dot
(struct
include D
module type S = sig
include Cfg.S
val ordered_iter_vertex:
compare:(vertex -> vertex -> int) -> (vertex -> unit) -> t -> unit
val iter_vertex_by_address : (vertex -> unit) -> t -> unit
val output_graph : Pervasives.out_channel ->
t -> entry:vertex -> Virtual_address.t list -> unit
val dump : filename:string -> t -> unit
end
module Make(H:Hashtbl.HashedType) = struct
module G = Cfg.Make(Key)(Value)(H)
include G
type block = {
leader: V.t;
block : V.t list;
succs : V.t list;
preds : V.t list;
}
module D = Graph.Imperative.Digraph.ConcreteBidirectional
(struct
type t = block
let compare b1 b2 = V.compare b1.leader b2.leader
let hash b = V.hash b.leader
let equal b1 b2 = V.equal b1.leader b2.leader
end)
module L = Graph.Leaderlist.Make(G)
module H = Hashtbl.Make(V)
let get_pred t v =
match pred t v with
| [v] -> Some v
| _ -> None
let get_succ t v =
match succ t v with
| [v] -> Some v
| _ -> None
let rec compare_preds_succs g v pred succ =
match pred, succ with
| None, None -> assert false
| Some _, None -> -1
| None, Some _ -> 1
| Some p, Some s ->
if V.equal v p then -1
else if V.equal v s then 1
else compare_preds_succs g v (get_pred g p) (get_succ g s)
let compare_vertex g v1 v2 =
if G.V.equal v1 v2 then 0
else compare_preds_succs g v1 (get_pred g v2) (get_succ g v2)
let rec diff lst1 lst2 acc =
match lst1, lst2 with
| ls, [] -> List.rev_append ls acc
| [], _ -> acc
| a1 :: ls1, a2 :: ls2 ->
if G.V.compare a1 a2 < 0 then diff ls1 lst2 (a1 :: acc)
else if G.V.compare a1 a2 > 0 then diff lst1 ls2 acc
else diff ls1 ls2 acc
let diff lst1 lst2 = List.rev (diff lst1 lst2 [])
let build_block g block =
let succs,preds =
List.fold_left
(fun (succs, preds) v ->
List.fold_left (fun l e -> e :: l) succs (succ g v),
List.fold_left (fun l e -> e :: l) preds (pred g v))
([], []) block
in
let block = List.sort_uniq V.compare block in
let succs = diff (List.sort_uniq V.compare succs) block in
let preds = diff (List.sort_uniq V.compare preds) block in
let block = List.sort_uniq (compare_vertex g) block in
{ leader = List.hd block; block; succs; preds }
let build_block_graph cfg entry =
let blocks = List.map (build_block cfg) (L.leader_lists cfg entry) in
let htbl = H.create 17 in
List.iter (fun b -> List.iter (fun v -> H.add htbl v b) b.block) blocks;
let t = D.create () in
List.iter
(fun block ->
let vertex = D.V.create block in
D.add_vertex t vertex;
List.iter
(fun succ -> D.add_edge t vertex (H.find htbl succ))
block.succs;
List.iter
(fun pred -> D.add_edge t (H.find htbl pred) vertex)
block.preds)
blocks;
t
let html_block callees block =
let open Format in
let align = "align=\"left\"" in
let border = "border=\"1\"" in
let open Colors in
let color1 = asprintf "bgcolor=\"%a\"" pp FlatUI.greensea in
let color2 = asprintf "bgcolor=\"%a\"" pp FlatUI.silver in
let pp_mnemonic ppf vert =
match V.inst vert with
| None -> ()
| Some inst ->
let a = Instruction.address inst in
let m = Instruction.mnemonic inst in
if List.mem a callees then
fprintf ppf "<font color=\"%a\">%a</font>"
pp FlatUI.alizarin Mnemonic.pp m
else Mnemonic.pp ppf m
in
block.block
|> List.map
(fun vert ->
asprintf "<tr><td %s %s>0x%x</td><td %s %s %s>%a</td></tr>"
border color1 (V.addr vert :> int)
border color2 align pp_mnemonic vert)
|> String.concat "\n"
|> sprintf "<table border=\"0\" cellspacing=\"0\">\n%s\n</table>"
let output_graph c g ~entry ca =
let g = build_block_graph g entry in
let module Dot =
struct
include Graph.Graphviz.Dot
(struct
include D
let graph_attributes _ = []
let default_vertex_attributes _ = [`Shape `Plaintext]
let vertex_name b = Printf.sprintf "%i" (Hashtbl.hash b)
let vertex_attributes b = [`HtmlLabel (html_block ca b)]
let get_subgraph _ = None
let default_edge_attributes _ = []
let edge_attributes _ = [`Minlen 1]
end)
end
in Dot.output_graph c g
let dump_oc oc g =
let module Dot =
Graph.Graphviz.Dot(struct
include G
let graph_attributes _ = []
let default_vertex_attributes _ = [`Shape `Plaintext]
let vertex_name b = Printf.sprintf "%i" (Hashtbl.hash b)
let vertex_attributes b = [`HtmlLabel (html_block ca b)]
let default_vertex_attributes _ = []
let vertex_name v =
Format.asprintf "\"%a %a\""
Virtual_address.pp (V.addr v)
(fun ppf v ->
let open Format in
match V.inst v with
| None -> pp_print_string ppf ""
| Some i ->
fprintf ppf "%a"
Mnemonic.pp (Instruction.mnemonic i)
) v
let vertex_attributes _ = []
let get_subgraph _ = None
let default_edge_attributes _ = []
let edge_attributes _ = [`Minlen 1]
let edge_attributes _ = []
end)
end
in Dot.output_graph c g
in Dot.output_graph oc g
let dump ~filename g =
let oc = open_out_bin filename in
dump_oc oc g;
close_out oc
let ordered_iter_vertex ~compare (f:vertex -> unit) g =
(* It is way better to use arrays (and even lists) than trees *)
let dummy_v = G.V.of_addr (Virtual_address.create 0) in
let a = Array.make (G.nb_vertex g) dummy_v in
let i = ref 0 in
iter_vertex (fun v -> a.(!i) <- v; incr i) g;
Array.sort compare a;
Array.iter f a
let iter_vertex_by_address = ordered_iter_vertex ~compare:Key.compare
end
module S =
struct
type t = string
let hash s = Hashtbl.hash s
let equal s1 s2 = s1 = s2
end
let ordered_iter_vertex ~compare (f:vertex -> unit) g =
(* It is way better to use arrays (and even lists) than trees *)
let dummy_v = G.V.of_addr (Virtual_address.create 0) in
let a = Array.make (G.nb_vertex g) dummy_v in
let i = ref 0 in
iter_vertex (fun v -> a.(!i) <- v; incr i) g;
Array.sort compare a;
Array.iter f a
module F = Make(S)
let iter_vertex_by_address = ordered_iter_vertex ~compare:Key.compare
include F
......@@ -19,14 +19,27 @@
(* *)
(**************************************************************************)
include Cfg.S with type addr = Virtual_address.t
and type inst = Instruction.t
and type symb = string
val ordered_iter_vertex:
compare:(vertex -> vertex -> int) -> (vertex -> unit) -> t -> unit
val iter_vertex_by_address : (vertex -> unit) -> t -> unit
module type S = sig
include Cfg.S
val output_graph : Pervasives.out_channel ->
t -> entry:vertex -> Virtual_address.t list -> unit
val ordered_iter_vertex:
compare:(vertex -> vertex -> int) -> (vertex -> unit) -> t -> unit
val iter_vertex_by_address : (vertex -> unit) -> t -> unit
val output_graph : Pervasives.out_channel ->
t -> entry:vertex -> Virtual_address.t list -> unit
val dump : filename:string -> t -> unit
end
module Make(H:Hashtbl.HashedType): S with type addr = Virtual_address.t
and type inst = Instruction.t
and type symb = H.t
include S with type addr = Virtual_address.t
and type inst = Instruction.t
and type symb = string
......@@ -138,16 +138,9 @@ let assert_constraint st e =
mk_assert @@ mk_bv_comp BvEqual bv_term bv_true
;;
let restate st =
let open Sse_symbolic.State in
if has_empty_vinfos st then copy_store st else st
;;
let add_assert_constraint st e =
let open Sse_symbolic in