You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

576 lines
26 KiB

(*
* Copyright (c) 2016 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*)
open! IStd
module F = Format
module L = Logging
(** Create a taint analysis from a specification *)
module Make (TaintSpecification : TaintSpec.S) = struct
module TraceDomain = TaintSpecification.Trace
module TaintDomain = TaintSpecification.AccessTree
module IdMapDomain = IdAccessPathMapDomain
module Summary = Summary.Make(struct
type payload = QuandarySummary.t
let update_payload quandary_payload (summary : Specs.summary) =
{ summary with payload = { summary.payload with quandary = Some quandary_payload }}
let read_payload (summary : Specs.summary) =
summary.payload.quandary
end)
module Domain = TaintDomain
let is_global (var, _) = match var with
| Var.ProgramVar pvar -> Pvar.is_global pvar
| Var.LogicalVar _ -> false
let is_return (var, _) = match var with
| Var.ProgramVar pvar -> Pvar.is_return pvar
| Var.LogicalVar _ -> false
let is_footprint (var, _) = match var with
| Var.ProgramVar _ -> false
| Var.LogicalVar id -> Ident.is_footprint id
let make_footprint_var formal_index =
Var.of_id (Ident.create_footprint Ident.name_spec formal_index)
let make_footprint_access_path formal_index access_path =
let _, base_typ = fst (AccessPath.extract access_path) in
AccessPath.with_base (make_footprint_var formal_index, base_typ) access_path
type extras = { formal_map : FormalMap.t; summary : Specs.summary; }
module TransferFunctions (CFG : ProcCfg.S) = struct
module CFG = CFG
module Domain = Domain
type nonrec extras = extras
(* get the node associated with [access_path] in [access_tree] *)
let access_path_get_node access_path access_tree (proc_data : extras ProcData.t) =
match TaintDomain.get_node access_path access_tree with
| Some _ as node_opt ->
node_opt
| None ->
let make_footprint_trace footprint_ap =
let trace =
TraceDomain.of_source
(TraceDomain.Source.make_footprint footprint_ap proc_data.pdesc) in
Some (TaintDomain.make_normal_leaf trace) in
let root, _ = AccessPath.extract access_path in
match FormalMap.get_formal_index root proc_data.extras.formal_map with
| Some formal_index ->
make_footprint_trace (make_footprint_access_path formal_index access_path)
| None ->
if is_global root
then make_footprint_trace access_path
else None
(* get the trace associated with [access_path] in [access_tree]. *)
let access_path_get_trace access_path access_tree proc_data =
match access_path_get_node access_path access_tree proc_data with
| Some (trace, _) -> trace
| None -> TraceDomain.empty
let exp_get_node_ ~abstracted raw_access_path access_tree proc_data =
let access_path =
if abstracted
then AccessPath.Abstracted raw_access_path
else AccessPath.Exact raw_access_path in
access_path_get_node access_path access_tree proc_data
(* get the node associated with [exp] in [access_tree] *)
let hil_exp_get_node ?(abstracted=false) (exp : HilExp.t) access_tree proc_data =
match exp with
| AccessPath access_path -> exp_get_node_ ~abstracted access_path access_tree proc_data
| _ -> None
let add_return_source source ret_base access_tree =
let trace = TraceDomain.of_source source in
let id_ap = AccessPath.Exact (ret_base, []) in
TaintDomain.add_trace id_ap trace access_tree
let add_actual_source source index actuals access_tree proc_data =
match List.nth_exn actuals index with
| HilExp.AccessPath actual_ap_raw ->
let actual_ap = AccessPath.Exact actual_ap_raw in
let trace = access_path_get_trace actual_ap access_tree proc_data in
TaintDomain.add_trace actual_ap (TraceDomain.add_source source trace) access_tree
| _ ->
access_tree
| exception (Failure _) ->
failwithf "Bad source specification: index %d out of bounds" index
let endpoints = String.Set.of_list (QuandaryConfig.Endpoint.of_json Config.quandary_endpoints)
let is_endpoint source =
match CallSite.pname (TraceDomain.Source.call_site source) with
| Typ.Procname.Java java_pname ->
String.Set.mem endpoints (Typ.Procname.java_get_class_name java_pname)
| _ ->
false
(** log any new reportable source-sink flows in [trace] *)
let report_trace trace cur_site (proc_data : extras ProcData.t) =
let trace_of_pname pname =
if Typ.Procname.equal pname (Procdesc.get_proc_name proc_data.pdesc)
then
(* read_summary will trigger ondemand analysis of the current proc. we don't want that. *)
TraceDomain.empty
else
match Summary.read_summary proc_data.pdesc pname with
| Some summary ->
TaintDomain.trace_fold
(fun acc _ trace -> TraceDomain.join trace acc)
(TaintSpecification.of_summary_access_tree summary)
TraceDomain.empty
| None ->
TraceDomain.empty in
let pp_path_short fmt (_, sources_passthroughs, sinks_passthroughs) =
let original_source = fst (List.hd_exn sources_passthroughs) in
let final_sink = fst (List.hd_exn sinks_passthroughs) in
F.fprintf
fmt
"%a -> %a%s"
TraceDomain.Source.pp original_source
TraceDomain.Sink.pp final_sink
(if is_endpoint original_source then ". Note: source is an endpoint." else "") in
let report_error path =
let msg = Localise.to_issue_id Localise.quandary_taint_error in
let trace_str = F.asprintf "%a" pp_path_short path in
let ltr = TraceDomain.to_loc_trace path in
let exn = Exceptions.Checkers (msg, Localise.verbatim_desc trace_str) in
Reporting.log_error_from_summary
proc_data.extras.summary ~loc:(CallSite.loc cur_site) ~ltr exn in
List.iter ~f:report_error (TraceDomain.get_reportable_paths ~cur_site trace ~trace_of_pname)
let add_sinks sinks actuals access_tree proc_data callee_site =
(* add [sink] to the trace associated with the [formal_index]th actual *)
let add_sink_to_actual access_tree_acc (sink_param : TraceDomain.Sink.parameter) =
match List.nth_exn actuals sink_param.index with
| HilExp.AccessPath actual_ap_raw ->
let actual_ap =
let is_array_typ =
match AccessPath.Raw.get_typ actual_ap_raw proc_data.ProcData.tenv with
| Some
({ desc=(
Typ.Tptr ({desc=Tarray _}, _) (* T* [] (Java-style) *)
| Tptr ({desc=Tptr _}, _) (* T** (C/C++ style 1) *)
| Tarray _ )}) (* T[] C/C++ style 2 *) ->
true
| _ ->
false in
(* conisder any sources that are reachable from an array *)
if sink_param.report_reachable || is_array_typ
then AccessPath.Abstracted actual_ap_raw
else AccessPath.Exact actual_ap_raw in
begin
match access_path_get_node actual_ap access_tree_acc proc_data with
| Some (actual_trace, _) ->
let actual_trace' = TraceDomain.add_sink sink_param.sink actual_trace in
report_trace actual_trace' callee_site proc_data;
TaintDomain.add_trace actual_ap actual_trace' access_tree_acc
| None ->
access_tree_acc
end
| _ ->
access_tree_acc in
List.fold ~f:add_sink_to_actual ~init:access_tree sinks
let apply_summary
ret_opt
(actuals : HilExp.t list)
summary
caller_access_tree
(proc_data : extras ProcData.t)
callee_site =
let get_caller_ap formal_ap =
let apply_return ret_ap = match ret_opt with
| Some base_var -> AccessPath.with_base base_var ret_ap
| None -> failwith "Have summary for retval, but no ret id to bind it to!" in
let get_actual_ap formal_index =
Option.value_map
~f:(function
| HilExp.AccessPath access_path -> Some access_path
| _ -> None)
~default:None
(List.nth actuals formal_index) in
let project ~formal_ap ~actual_ap =
let projected_ap = AccessPath.append actual_ap (snd (AccessPath.extract formal_ap)) in
if AccessPath.is_exact formal_ap
then AccessPath.Exact projected_ap
else AccessPath.Abstracted projected_ap in
let base_var, _ = fst (AccessPath.extract formal_ap) in
match base_var with
| Var.ProgramVar pvar ->
if Pvar.is_return pvar
then Some (apply_return formal_ap)
else Some formal_ap
| Var.LogicalVar id when Ident.is_footprint id ->
begin
(* summaries store the index of the formal parameter in the ident stamp *)
match get_actual_ap (Ident.get_stamp id) with
| Some actual_ap ->
let projected_ap = project ~formal_ap ~actual_ap in
Some projected_ap
| None ->
None
end
| _ ->
None in
let get_caller_ap_node_opt ap access_tree =
let get_caller_node caller_ap =
let caller_node_opt = access_path_get_node caller_ap access_tree proc_data in
let caller_node = Option.value ~default:TaintDomain.empty_node caller_node_opt in
caller_ap, caller_node in
Option.map (get_caller_ap ap) ~f:get_caller_node in
let replace_footprint_sources callee_trace caller_trace access_tree =
let replace_footprint_source source acc =
match TraceDomain.Source.get_footprint_access_path source with
| Some footprint_access_path ->
begin
match get_caller_ap_node_opt footprint_access_path access_tree with
| Some (_, (caller_ap_trace, _)) -> TraceDomain.join caller_ap_trace acc
| None -> acc
end
| None ->
acc in
TraceDomain.Sources.fold
replace_footprint_source (TraceDomain.sources callee_trace) caller_trace in
let instantiate_and_report callee_trace caller_trace access_tree =
let caller_trace' = replace_footprint_sources callee_trace caller_trace access_tree in
let appended_trace = TraceDomain.append caller_trace' callee_trace callee_site in
report_trace appended_trace callee_site proc_data;
appended_trace in
let add_to_caller_tree access_tree_acc callee_ap callee_trace =
match get_caller_ap_node_opt callee_ap access_tree_acc with
| Some (caller_ap, (caller_trace, caller_tree)) ->
let trace = instantiate_and_report callee_trace caller_trace access_tree_acc in
TaintDomain.add_node caller_ap (trace, caller_tree) access_tree_acc
| None ->
ignore (instantiate_and_report callee_trace TraceDomain.empty access_tree_acc);
access_tree_acc in
TaintDomain.trace_fold
add_to_caller_tree
(TaintSpecification.of_summary_access_tree summary)
caller_access_tree
let exec_instr (astate : Domain.astate) (proc_data : extras ProcData.t) _ (instr : HilInstr.t) =
let exec_write lhs_access_path rhs_exp astate=
let rhs_node =
Option.value
(hil_exp_get_node rhs_exp astate proc_data)
~default:TaintDomain.empty_node in
TaintDomain.add_node (AccessPath.Exact lhs_access_path) rhs_node astate in
match instr with
| Assign (((Var.ProgramVar pvar, _), []), HilExp.Exception _, _) when Pvar.is_return pvar ->
(* the Java frontend translates `throw Exception` as `return Exception`, which is a bit
wonky. this translation causes problems for us in computing a summary when an
exception is "returned" from a void function. skip code like this for now, fix via
t14159157 later *)
astate
| Assign (((Var.ProgramVar pvar, _), []), rhs_exp, _)
when Pvar.is_return pvar && HilExp.is_null_literal rhs_exp &&
Typ.equal_desc Tvoid (Procdesc.get_ret_type proc_data.pdesc).desc ->
(* similar to the case above; the Java frontend translates "return no exception" as
`return null` in a void function *)
astate
| Assign (lhs_access_path, rhs_exp, _) ->
exec_write lhs_access_path rhs_exp astate
| Call (ret_opt, Direct called_pname, actuals, call_flags, callee_loc) ->
let handle_unknown_call callee_pname access_tree =
let is_variadic = match callee_pname with
| Typ.Procname.Java pname ->
begin
match List.rev (Typ.Procname.java_get_parameters pname) with
| (_, "java.lang.Object[]") :: _ -> true
| _ -> false
end
| _ -> false in
let should_taint_typ typ = is_variadic || TaintSpecification.is_taintable_type typ in
let exp_join_traces trace_acc exp =
match hil_exp_get_node ~abstracted:true exp access_tree proc_data with
| Some (trace, _) -> TraceDomain.join trace trace_acc
| None -> trace_acc in
let propagate_to_access_path access_path actuals access_tree =
let initial_trace =
access_path_get_trace access_path access_tree proc_data in
let trace_with_propagation =
List.fold ~f:exp_join_traces ~init:initial_trace actuals in
let filtered_sources =
TraceDomain.Sources.filter (fun source ->
match TraceDomain.Source.get_footprint_access_path source with
| Some access_path ->
Option.exists
(AccessPath.Raw.get_typ (AccessPath.extract access_path) proc_data.tenv)
~f:should_taint_typ
| None ->
true)
(TraceDomain.sources trace_with_propagation) in
if TraceDomain.Sources.is_empty filtered_sources
then
access_tree
else
let trace' = TraceDomain.update_sources trace_with_propagation filtered_sources in
TaintDomain.add_trace access_path trace' access_tree in
let handle_unknown_call_ astate_acc propagation =
match propagation, actuals, ret_opt with
| _, [], _ ->
astate_acc
| TaintSpec.Propagate_to_return, actuals, Some ret_ap ->
propagate_to_access_path (AccessPath.Exact (ret_ap, [])) actuals astate_acc
| TaintSpec.Propagate_to_receiver,
AccessPath receiver_ap :: (_ :: _ as other_actuals),
_ ->
propagate_to_access_path (AccessPath.Exact receiver_ap) other_actuals astate_acc
| TaintSpec.Propagate_to_actual actual_index, _, _ ->
begin
match List.nth actuals actual_index with
| Some (HilExp.AccessPath actual_ap) ->
propagate_to_access_path (AccessPath.Exact actual_ap) actuals astate_acc
| _ ->
astate_acc
end
| _ ->
astate_acc in
match Typ.Procname.get_method callee_pname with
| "operator=" when not (Typ.Procname.is_java callee_pname) ->
(* treat unknown calls to C++ operator= as assignment *)
begin
match actuals with
| [AccessPath lhs_access_path; rhs_exp] ->
exec_write lhs_access_path rhs_exp access_tree
| _ ->
failwithf "Unexpected call to operator= %a" HilInstr.pp instr
end
| _ ->
let propagations =
TaintSpecification.handle_unknown_call
callee_pname
(Option.map ~f:snd ret_opt)
actuals
proc_data.tenv in
List.fold ~f:handle_unknown_call_ ~init:access_tree propagations in
let analyze_call astate_acc callee_pname =
let call_site = CallSite.make callee_pname callee_loc in
let sinks = TraceDomain.Sink.get call_site actuals proc_data.ProcData.tenv in
let astate_with_sink = match sinks with
| [] -> astate
| sinks -> add_sinks sinks actuals astate proc_data call_site in
let source = TraceDomain.Source.get call_site proc_data.tenv in
let astate_with_source =
match source, ret_opt with
| Some { TraceDomain.Source.source; index=None; }, Some ret_base ->
add_return_source source ret_base astate_with_sink
| Some { TraceDomain.Source.source; index=Some index; }, _ ->
add_actual_source source index actuals astate_with_sink proc_data
| Some { TraceDomain.Source.source; index=None; }, None ->
let warn_invalid_source () =
L.stderr
"Warning: %a is marked as a source, but has no return value"
Typ.Procname.pp callee_pname;
astate_with_sink in
if not (Typ.Procname.is_java callee_pname)
then
(* the C++ frontend handles returns of non-pointers by adding a dummy
pass-by-reference variable as the last actual, then returning the value
by assigning to it. make sure we understand this pattern *)
match List.last actuals with
| Some (HilExp.AccessPath ((Var.ProgramVar pvar, _) as ret_base, []))
when Pvar.is_frontend_tmp pvar ->
add_return_source source ret_base astate_with_sink
| _ ->
warn_invalid_source ()
else
warn_invalid_source ()
| None, _ ->
astate_with_sink in
let astate_with_summary =
(* hack for default C++ constructors, which get translated as an empty body (and
will thus have an empty summary). We don't want that because we want to be able to
propagate taint from comstructor parameters to the constructed object. so we treat
the empty constructor as a skip function instead *)
let is_dummy_cpp_constructor summary pname =
Typ.Procname.is_c_method pname &&
Typ.Procname.is_constructor pname &&
TaintDomain.BaseMap.is_empty (TaintSpecification.of_summary_access_tree summary) in
if sinks <> [] || Option.is_some source
then
(* don't use a summary for a procedure that is a direct source or sink *)
astate_with_source
else
match Summary.read_summary proc_data.pdesc callee_pname with
| Some summary when not (is_dummy_cpp_constructor summary callee_pname) ->
apply_summary ret_opt actuals summary astate_with_source proc_data call_site
| _ ->
handle_unknown_call callee_pname astate_with_source in
Domain.join astate_acc astate_with_summary in
(* highly polymorphic call sites stress reactive mode too much by using too much memory.
here, we choose an arbitrary call limit that allows us to finish the analysis in
practice. this is obviously unsound; will try to remove in the future. *)
let max_calls = 3 in
let targets =
if List.length call_flags.cf_targets <= max_calls
then
called_pname :: call_flags.cf_targets
else
begin
L.out
"Skipping highly polymorphic call site for %a@." Typ.Procname.pp called_pname;
[called_pname]
end in
(* for each possible target of the call, apply the summary. join all results together *)
List.fold ~f:analyze_call ~init:Domain.empty targets
| _ ->
astate
end
module Analyzer =
AbstractInterpreter.Make (ProcCfg.Exceptional) (LowerHil.Make(TransferFunctions))
let make_summary { ProcData.pdesc; extras={ formal_map; } } access_tree =
let is_java = Typ.Procname.is_java (Procdesc.get_proc_name pdesc) in
(* if a trace has footprint sources, attach them to the appropriate footprint var *)
let access_tree' =
TaintDomain.fold
(fun access_tree_acc _ ((trace, _) as node) ->
if TraceDomain.Sinks.is_empty (TraceDomain.sinks trace)
then
(* if this trace has no sinks, we don't need to attach it to anything *)
access_tree_acc
else
TraceDomain.Sources.fold
(fun source acc ->
match TraceDomain.Source.get_footprint_access_path source with
| Some footprint_access_path ->
let node' =
match TaintDomain.get_node footprint_access_path acc with
| Some n -> TaintDomain.node_join node n
| None -> node in
TaintDomain.add_node footprint_access_path node' acc
| None ->
acc)
(TraceDomain.sources trace)
access_tree_acc)
access_tree
access_tree in
(* should only be used on nodes associated with a footprint base *)
let is_empty_node (trace, tree) =
(* In C++, we can reassign the value pointed to by a pointer type formal, and we can assign
to a value type passed by reference. these mechanisms can be used to associate a source
directly with a formal. In Java this can't happen, so we only care if the formal flows to
a sink *)
(if is_java
then TraceDomain.Sinks.is_empty (TraceDomain.sinks trace)
else TraceDomain.is_empty trace) &&
match tree with
| TaintDomain.Subtree subtree -> TaintDomain.AccessMap.is_empty subtree
| TaintDomain.Star -> true in
(* replace formal names with footprint vars for their indices. For example, for `foo(o)`, we'll
replace `o` with FP(1) *)
let with_footprint_vars =
AccessPath.BaseMap.fold
(fun base ((trace, subtree) as node) acc ->
if is_global base || is_return base
then AccessPath.BaseMap.add base node acc
else if is_footprint base
then
if is_empty_node node
then
acc
else
let node' =
if TraceDomain.Sinks.is_empty (TraceDomain.sinks trace)
then TraceDomain.empty, subtree
else node in
AccessPath.BaseMap.add base node' acc
else
match FormalMap.get_formal_index base formal_map with
| Some formal_index ->
let base' = make_footprint_var formal_index, snd base in
let joined_node =
try TaintDomain.node_join (AccessPath.BaseMap.find base' acc) node
with Not_found -> node in
if is_empty_node joined_node
then acc
else AccessPath.BaseMap.add base' joined_node acc
| None ->
(* base is a local var *)
acc)
access_tree'
TaintDomain.empty in
TaintSpecification.to_summary_access_tree with_footprint_vars
module Interprocedural = AbstractInterpreter.Interprocedural(Summary)
let checker ({ Callbacks.tenv; summary; } as callback) : Specs.summary =
(* bind parameters to a trace with a tainted source (if applicable) *)
let make_initial pdesc =
let pname = Procdesc.get_proc_name pdesc in
let access_tree =
List.fold ~f:(fun acc (name, typ, taint_opt) ->
match taint_opt with
| Some source ->
let base_ap = AccessPath.Exact (AccessPath.of_pvar (Pvar.mk name pname) typ) in
TaintDomain.add_trace base_ap (TraceDomain.of_source source) acc
| None ->
acc)
~init:TaintDomain.empty
(TraceDomain.Source.get_tainted_formals pdesc tenv) in
access_tree, IdAccessPathMapDomain.empty in
let compute_post (proc_data : extras ProcData.t) =
if not (Procdesc.did_preanalysis proc_data.pdesc)
then
begin
Preanal.do_liveness proc_data.pdesc proc_data.tenv;
Preanal.do_dynamic_dispatch
proc_data.pdesc (Cg.create (SourceFile.invalid __FILE__)) proc_data.tenv;
end;
let initial = make_initial proc_data.pdesc in
match Analyzer.compute_post proc_data ~initial with
| Some (access_tree, _) ->
Some (make_summary proc_data access_tree)
| None ->
if Procdesc.Node.get_succs (Procdesc.get_start_node proc_data.pdesc) <> []
then failwith "Couldn't compute post"
else None in
let make_extras pdesc =
let formal_map = FormalMap.make pdesc in
{ formal_map; summary; } in
Interprocedural.compute_and_store_post ~compute_post ~make_extras callback
end