Skip to content

Commit

Permalink
Merge pull request #1123 from mrstanb/improve-uaf-analysis
Browse files Browse the repository at this point in the history 
Improve multi-threaded UAF analysis and add SVComp result generation
  • Loading branch information
@michael-schwarz
michael-schwarz authored Sep 29, 2023
2 parents 91ea3b9 + cb29ecd commit 67160fe
Show file tree
Hide file tree
Showing 13 changed files with 296 additions and 81 deletions.
168 changes: 104 additions & 64 deletions src/analyses/useAfterFree.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ open Analyses
open MessageCategory

module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
module ThreadIdSet = SetDomain.Make(ThreadIdDomain.ThreadLifted)
module ThreadIdToJoinedThreadsMap = MapDomain.MapBot(ThreadIdDomain.ThreadLifted)(ConcDomain.MustThreadSet)

module Spec : Analyses.MCPSpec =
struct
Expand All @@ -15,7 +15,7 @@ struct

module D = ToppedVarInfoSet
module C = Lattice.Unit
module G = ThreadIdSet
module G = ThreadIdToJoinedThreadsMap
module V = VarinfoV

(** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *)
Expand All @@ -24,83 +24,110 @@ struct

(* HELPER FUNCTIONS *)

let set_global_svcomp_var is_double_free =
if is_double_free then
AnalysisState.svcomp_may_invalid_free := true
else
AnalysisState.svcomp_may_invalid_deref := true

let get_current_threadid ctx =
ctx.ask Queries.CurrentThreadId

let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number =
let get_joined_threads ctx =
ctx.ask Queries.MustJoinedThreads

let warn_for_multi_threaded_access ctx ?(is_double_free = false) (heap_var:varinfo) behavior cwe_number =
let freeing_threads = ctx.global heap_var in
(* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *)
if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || ThreadIdSet.is_empty freeing_threads then ()
if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || G.is_empty freeing_threads then ()
else begin
let possibly_started current = function
let possibly_started current tid joined_threads =
match tid with
| `Lifted tid ->
let threads = ctx.ask Queries.CreatedThreads in
let not_started = MHP.definitely_not_started (current, threads) tid in
let created_threads = ctx.ask Queries.CreatedThreads in
let not_started = MHP.definitely_not_started (current, created_threads) tid in
let possibly_started = not not_started in
possibly_started
(* If [current] is possibly running together with [tid], but is also joined before the free() in [tid], then no need to WARN *)
let current_joined_before_free = ConcDomain.MustThreadSet.mem current joined_threads in
possibly_started && not current_joined_before_free
| `Top -> true
| `Bot -> false
in
let equal_current current = function
let equal_current current tid joined_threads =
match tid with
| `Lifted tid ->
ThreadId.Thread.equal current tid
| `Top -> true
| `Bot -> false
in
let bug_name = if is_double_free then "Double Free" else "Use After Free" in
match get_current_threadid ctx with
| `Lifted current ->
let possibly_started = ThreadIdSet.exists (possibly_started current) freeing_threads in
if possibly_started then
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. Use-After-Free might occur" CilType.Varinfo.pretty heap_var
let possibly_started = G.exists (possibly_started current) freeing_threads in
if possibly_started then begin
set_global_svcomp_var is_double_free;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. %s might occur" CilType.Varinfo.pretty heap_var bug_name
end
else begin
let current_is_unique = ThreadId.Thread.is_unique current in
let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in
if not current_is_unique && any_equal_current freeing_threads then
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var
else if D.mem heap_var ctx.local then
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Use-After-Free might occur in current unique thread %a for heap variable %a" ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
let any_equal_current threads = G.exists (equal_current current) threads in
if not current_is_unique && any_equal_current freeing_threads then begin
set_global_svcomp_var is_double_free;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var
end
else if D.mem heap_var ctx.local then begin
set_global_svcomp_var is_double_free;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
end
end
| `Top ->
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. A Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var
set_global_svcomp_var is_double_free;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. %s might occur for heap variable %a" bug_name CilType.Varinfo.pretty heap_var
| `Bot ->
M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom"
end

let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) =
let state = ctx.local in
let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in
let cwe_number = if is_double_free then 415 else 416 in
let rec offset_might_contain_freed offset =
match offset with
| NoOffset -> ()
| Field (f, o) -> offset_might_contain_freed o
| Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name ctx e; offset_might_contain_freed o
in
let (lval_host, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *)
let lval_to_query =
match lval_host with
| Var _ -> Lval lval
| Mem _ -> mkAddrOf lval (* Take the lval's address if its lhost is of the form *p, where p is a ptr *)
in
match ctx.ask (Queries.MayPointTo lval_to_query) with
| ad when not (Queries.AD.is_top ad) ->
let warn_for_heap_var v =
if D.mem v state then
M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name
let rec warn_lval_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) =
match is_implicitly_derefed, is_double_free, lval with
(* If we're not checking for a double-free and there's no deref happening, then there's no need to check for an invalid deref or an invalid free *)
| false, false, (Var _, NoOffset) -> ()
| _ ->
let state = ctx.local in
let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in
let cwe_number = if is_double_free then 415 else 416 in
let rec offset_might_contain_freed offset =
match offset with
| NoOffset -> ()
| Field (f, o) -> offset_might_contain_freed o
| Index (e, o) -> warn_exp_might_contain_freed transfer_fn_name ctx e; offset_might_contain_freed o
in
let pointed_to_heap_vars =
Queries.AD.fold (fun addr vars ->
match addr with
| Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) -> v :: vars
| _ -> vars
) ad []
let (lval_host, o) = lval in offset_might_contain_freed o; (* Check the lval's offset *)
let lval_to_query =
match lval_host with
| Var _ -> Lval lval
| Mem _ -> mkAddrOf lval (* Take the lval's address if its lhost is of the form *p, where p is a ptr *)
in
List.iter warn_for_heap_var pointed_to_heap_vars; (* Warn for all heap vars that the lval possibly points to *)
(* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *)
List.iter (fun heap_var -> warn_for_multi_threaded_access ctx heap_var undefined_behavior cwe_number) pointed_to_heap_vars
| _ -> ()
begin match ctx.ask (Queries.MayPointTo lval_to_query) with
| ad when not (Queries.AD.is_top ad) ->
let warn_for_heap_var v =
if D.mem v state then
M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name
in
let pointed_to_heap_vars =
Queries.AD.fold (fun addr vars ->
match addr with
| Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) -> v :: vars
| _ -> vars
) ad []
in
(* Warn for all heap vars that the lval possibly points to *)
List.iter warn_for_heap_var pointed_to_heap_vars;
(* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *)
List.iter (fun heap_var -> warn_for_multi_threaded_access ctx ~is_double_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars
| _ -> ()
end

and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) =
and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) =
match exp with
(* Base recursion cases *)
| Const _
Expand All @@ -114,22 +141,27 @@ struct
| SizeOfE e
| AlignOfE e
| UnOp (_, e, _)
| CastE (_, e) -> warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e
| CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e
| BinOp (_, e1, e2, _) ->
warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e1;
warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e2
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e1;
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e2
| Question (e1, e2, e3, _) ->
warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e1;
warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e2;
warn_exp_might_contain_freed ~is_double_free transfer_fn_name ctx e3
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e1;
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e2;
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx e3
(* Lval cases (need [warn_lval_might_contain_freed] for them) *)
| Lval lval
| StartOf lval
| AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name ctx lval
| AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_double_free transfer_fn_name ctx lval

let side_effect_mem_free ctx freed_heap_vars threadid joined_threads =
let side_effect_globals_to_heap_var heap_var =
let current_globals = ctx.global heap_var in
let globals_to_side_effect = G.add threadid joined_threads current_globals in
ctx.sideg heap_var globals_to_side_effect
in
D.iter side_effect_globals_to_heap_var freed_heap_vars

let side_effect_mem_free ctx freed_heap_vars threadid =
let threadid = G.singleton threadid in
D.iter (fun var -> ctx.sideg var threadid) freed_heap_vars


(* TRANSFER FUNCTIONS *)
Expand Down Expand Up @@ -175,9 +207,16 @@ struct

let special ctx (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
let state = ctx.local in
Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) ctx x) lval;
List.iter (fun arg -> warn_exp_might_contain_freed ~is_double_free:(f.vname = "free") ("special: " ^ f.vname) ctx arg) arglist;
let desc = LibraryFunctions.find f in
let is_arg_implicitly_derefed arg =
let read_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = false } arglist in
let read_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Read; deep = true } arglist in
let write_shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } arglist in
let write_deep_args = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } arglist in
List.mem arg read_shallow_args || List.mem arg read_deep_args || List.mem arg write_shallow_args || List.mem arg write_deep_args
in
Option.iter (fun x -> warn_lval_might_contain_freed ("special: " ^ f.vname) ctx x) lval;
List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_double_free:(match desc.special arglist with Free _ -> true | _ -> false) ("special: " ^ f.vname) ctx arg) arglist;
match desc.special arglist with
| Free ptr ->
begin match ctx.ask (Queries.MayPointTo ptr) with
Expand All @@ -190,8 +229,9 @@ struct
) ad (D.empty ())
in
(* Side-effect the tid that's freeing all the heap vars collected here *)
side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx);
D.join state (pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *)
side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx) (get_joined_threads ctx);
(* Add all heap vars, which ptr points to, to the state *)
D.join state (pointed_to_heap_vars)
| _ -> state
end
| _ -> state
Expand Down
7 changes: 7 additions & 0 deletions src/autoTune.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -219,6 +219,13 @@ let focusOnSpecification () =
| NoOverflow -> (*We focus on integer analysis*)
set_bool "ana.int.def_exc" true;
set_bool "ana.int.interval" true
| ValidFree -> (* Enable the useAfterFree analysis *)
let uafAna = ["useAfterFree"] in
print_endline @@ "Specification: ValidFree -> enabling useAfterFree analysis \"" ^ (String.concat ", " uafAna) ^ "\"";
enableAnalyses uafAna
(* TODO: Finish these two below later *)
| ValidDeref
| ValidMemtrack -> ()

(*Detect enumerations and enable the "ana.int.enums" option*)
exception EnumFound
Expand Down
6 changes: 6 additions & 0 deletions src/framework/analysisState.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,15 @@ let should_warn = ref false
(** Whether signed overflow or underflow happened *)
let svcomp_may_overflow = ref false

(** Whether an invalid free happened *)
let svcomp_may_invalid_free = ref false

(** Whether an invalid pointer dereference happened *)
let svcomp_may_invalid_deref = ref false

(** Whether an invalid memtrack happened *)
let svcomp_may_invalid_memtrack = ref false

(** A hack to see if we are currently doing global inits *)
let global_initialization = ref false

Expand Down
3 changes: 3 additions & 0 deletions src/witness/svcomp.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,9 @@ struct
| UnreachCall _ -> "unreach-call"
| NoOverflow -> "no-overflow"
| NoDataRace -> "no-data-race" (* not yet in SV-COMP/Benchexec *)
| ValidFree -> "valid-free"
| ValidDeref -> "valid-deref"
| ValidMemtrack -> "valid-memtrack"
in
"false(" ^ result_spec ^ ")"
| Unknown -> "unknown"
Expand Down
37 changes: 30 additions & 7 deletions src/witness/svcompSpec.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,15 @@ type t =
| UnreachCall of string
| NoDataRace
| NoOverflow
| ValidFree
| ValidDeref
| ValidMemtrack

let of_string s =
let s = String.strip s in
let regexp = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
if Str.string_match regexp s 0 then
let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in
let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
if Str.string_match regexp_negated s 0 then
let global_not = Str.matched_group 1 s in
if global_not = "data-race" then
NoDataRace
Expand All @@ -23,6 +27,16 @@ let of_string s =
UnreachCall f
else
failwith "Svcomp.Specification.of_string: unknown global not expression"
else if Str.string_match regexp s 0 then
let global = Str.matched_group 1 s in
if global = "valid-free" then
ValidFree
else if global = "valid-deref" then
ValidDeref
else if global = "valid-memtrack" then
ValidMemtrack
else
failwith "Svcomp.Specification.of_string: unknown global expression"
else
failwith "Svcomp.Specification.of_string: unknown expression"

Expand All @@ -38,9 +52,18 @@ let of_option () =
of_string s

let to_string spec =
let global_not = match spec with
| UnreachCall f -> "call(" ^ f ^ "())"
| NoDataRace -> "data-race"
| NoOverflow -> "overflow"
let print_output spec_str is_neg =
if is_neg then
Printf.sprintf "CHECK( init(main()), LTL(G ! %s) )" spec_str
else
Printf.sprintf "CHECK( init(main()), LTL(G %s) )" spec_str
in
let spec_str, is_neg = match spec with
| UnreachCall f -> "call(" ^ f ^ "())", true
| NoDataRace -> "data-race", true
| NoOverflow -> "overflow", true
| ValidFree -> "valid-free", false
| ValidDeref -> "valid-deref", false
| ValidMemtrack -> "valid-memtrack", false
in
"CHECK( init(main()), LTL(G ! " ^ global_not ^ ") )"
print_output spec_str is_neg
Loading

0 comments on commit 67160fe

Please sign in to comment.