Skip to content

Use access events in useAfterFree analysis #1864

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: issue_1861
Choose a base branch
from
+34 −97
Draft

Use access events in useAfterFree analysis #1864

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 1 addition & 1 deletion src/analyses/accessAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ struct
let init _ =
collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
let activated = get_string_list "ana.activated" in
emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated

let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) =
if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;
Expand Down
129 changes: 33 additions & 96 deletions src/analyses/useAfterFree.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,87 +85,6 @@ struct
M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom"
end

(**
[is_free] indicates that the lval is passed to free, i.e., whether we consider a call [free(lval)].
*)
let rec warn_lval_might_contain_freed ?(is_implicitly_derefed = false) ?(is_free = false) (transfer_fn_name:string) man (lval:lval) =
match is_implicitly_derefed, is_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 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 man e;
offset_might_contain_freed o
in
let (lval_host, o) = lval in
offset_might_contain_freed o; (* Check the lval's offset *)

let freed_heap_vars = snd man.local in
let undefined_behavior = if is_free then Undefined DoubleFree else Undefined UseAfterFree in
let cwe_number = if is_free then 415 else 416 in

let check_adress adresses =
let warn_for_heap_var v =
if HeapVars.mem v freed_heap_vars then begin
if is_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
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
end
in
let pointed_to_heap_vars =
Queries.AD.fold (fun addr vars ->
match addr with
| Queries.AD.Addr.Addr (v,_) when man.ask (Queries.IsAllocVar v) -> v :: vars
| _ -> vars
) adresses []
in
if not (Queries.AD.is_top adresses) then begin
(* 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 man ~is_free heap_var undefined_behavior cwe_number) pointed_to_heap_vars
end
in
let addresses = man.ask (Queries.MayPointTo (Lval lval)) in
check_adress addresses;
match lval_host with
| Var _ -> ()
| Mem exp ->
(* We have (\*x).o', so we check recursively whether x has been freed. *)
warn_exp_might_contain_freed ~is_implicitly_derefed:true ~is_free:false transfer_fn_name man exp

(** [is_free] indicates that the exp is passed to free, i.e., we consider a call [free(exp)]*)
and warn_exp_might_contain_freed ?(is_implicitly_derefed = false) ?(is_free = false) (transfer_fn_name:string) man (exp:exp) =
match exp with
(* Base recursion cases *)
| Const _
| SizeOf _
| SizeOfStr _
| AlignOf _
| AddrOfLabel _ -> ()
(* Non-base cases *)
| Real e
| Imag e
| SizeOfE e
| AlignOfE e
| UnOp (_, e, _)
| CastE (_, e) -> warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e
| BinOp (_, e1, e2, _) ->
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e1;
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e2
| Question (e1, e2, e3, _) ->
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e1;
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e2;
warn_exp_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man e3
(* Lval cases (need [warn_lval_might_contain_freed] for them) *)
| Lval lval
| StartOf lval
| AddrOf lval -> warn_lval_might_contain_freed ~is_implicitly_derefed ~is_free transfer_fn_name man lval

let side_effect_mem_free man freed_heap_vars threadid joined_threads =
let side_effect_globals_to_heap_var heap_var =
let current_globals = man.global heap_var in
Expand All @@ -178,21 +97,16 @@ struct
(* TRANSFER FUNCTIONS *)

let assign man (lval:lval) (rval:exp) : D.t =
warn_lval_might_contain_freed "assign" man lval;
warn_exp_might_contain_freed "assign" man rval;
man.local

let branch man (exp:exp) (tv:bool) : D.t =
warn_exp_might_contain_freed "branch" man exp;
man.local

let return man (exp:exp option) (f:fundec) : D.t =
Option.iter (fun x -> warn_exp_might_contain_freed "return" man x) exp;
man.local

let enter man (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
let caller_state = man.local in
List.iter (fun arg -> warn_exp_might_contain_freed "enter" man arg) args;
(* TODO: The 2nd component of the callee state needs to contain only the heap vars from the caller state which are reachable from: *)
(* * Global program variables *)
(* * The callee arguments *)
Expand All @@ -208,21 +122,11 @@ struct
(caller_stack_state, HeapVars.join caller_heap_state callee_combined_state)

let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t =
Option.iter (fun x -> warn_lval_might_contain_freed "enter" man x) lval;
man.local

let special man (lval:lval option) (f:varinfo) (arglist:exp list) : D.t =
let state = man.local in
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) man x) lval;
List.iter (fun arg -> warn_exp_might_contain_freed ~is_implicitly_derefed:(is_arg_implicitly_derefed arg) ~is_free:(match desc.special arglist with Free _ -> true | _ -> false) ("special: " ^ f.vname) man arg) arglist;
match desc.special arglist with
| Free ptr ->
begin match man.ask (Queries.MayPointTo ptr) with
Expand Down Expand Up @@ -251,6 +155,39 @@ struct
let startstate v = D.bot ()
let exitstate v = D.top ()

let event man e oman =
match e with
| Events.Access {exp; ad; kind; reach} ->
(* must use original (pre-assign, etc) man queries *)
let check_adress adresses =
let freed_heap_vars = snd oman.local in
let undefined_behavior = Undefined UseAfterFree in
let cwe_number = 416 in
let warn_for_heap_var v =
if HeapVars.mem v freed_heap_vars then begin
set_mem_safety_flag InvalidDeref;
M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname "event"
end
in
let pointed_to_heap_vars =
Queries.AD.fold (fun addr vars ->
match addr with
| Queries.AD.Addr.Addr (v,_) when oman.ask (Queries.IsAllocVar v) -> v :: vars
| _ -> vars
) adresses []
in
if not (Queries.AD.is_top adresses) then begin
(* 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 oman ~is_free:false heap_var undefined_behavior cwe_number) pointed_to_heap_vars
end
in
check_adress ad;
man.local
| _ ->
man.local

end

let _ =
Expand Down
Loading