Double Dereferences under Tainted Branch Detector

ddtbd-debug.recipe

(extend ddtbd)
;; debugging stuff
(option primus-propagate-taint-to-attributes)
(option print-bir-attr tainted-reg)
(option print-bir-attr tainted-ptr)
(option print-bir-attr tainted-regs)
(option print-bir-attr tainted-ptrs)
(option dump bir:out.bir)

(option primus-print-obs enter-term read)
(option primus-print-output trace)

ddtbd.ml

open Core_kernel
open Bap.Std
open Bap_primus.Std
open Bap_taint.Std
open Bap_future.Std
open Format
include Self()

let max_length = Config.(param int "length" ~default:4)

(* a kind of program point *)
type point =
  | Cond                        (* a tainted condition *)
  | L1                          (* the first load  *)
  | L2                          (* the second access *)

type path = {
  length : int;                 (* length of the tainted path *)
  points : (point * addr) list; (* points of interest, for the report *)
  step   : point;               (* on which state we are *)
}

let initial_state = {
  length = 0;
  points = [];
  step = Cond;
}

let state = Primus.Machine.State.declare
    ~uuid:"10d552e4-9c4d-40ce-8bfe-50faed839dcf"
    ~name:"ddtbd"
    (fun _ -> initial_state)

let get par =
  Future.peek_exn (Config.determined par)

let string_of_point = function
  | Cond -> "branch"
  | L1 -> "first load"
  | L2 -> "second load"

module Tracker(Machine : Primus.Machine.S) = struct
  open Machine.Syntax
  module Tracker = Taint.Tracker.Make(Machine)
  module Eval = Primus.Interpreter.Make(Machine)


  let init_track v =
    Tracker.lookup v Taint.Rel.direct >>= fun td ->
    if Set.is_empty td
    then Machine.return ()
    else Eval.pc >>= fun pc ->
      info "path is tainted by the condition at %a" Addr.pp pc;
      Machine.Local.update state ~f:(fun s -> {
            s with length = get max_length;
                   points = (Cond,pc) :: s.points;
          })

  let on_jmp (_,dst) = init_track dst
  let on_cnd cnd = init_track cnd


  let push k p s = {s with step = k; points = (k,p)::s.points}

  let next_step is_load s p = match s.step with
    | Cond -> if is_load then push L1 p s else s
    | L1 | L2 -> push L2 p s


  (* ideally, we should make an observation... but let's print it just *)
  let report s =
    info "DDTBD Violation. Backtrace:@\n";
    List.iter s.points ~f:(fun (p,pc) ->
        info "%a: %s@\n" Addr.pp pc (string_of_point p));
    Machine.return ()

  let access ~is_load addr =
    Machine.Local.get state >>= function
    | {length=0} -> Machine.return () (* no tracking yet *)
    | s ->                            (* we're close to a tainted branch *)
      Tracker.lookup addr Taint.Rel.indirect >>= fun taints ->
      if Set.is_empty taints
      then Machine.return ()         (* but a load is not tained *)
      else Eval.pc >>= fun pc ->        (* we got a load, let's get the PC *)
        info "%s on a tainted path at %a"
          (if is_load then "load" else "store")
          Addr.pp pc ;
        let s = next_step is_load s pc in
        Machine.Local.put state s >>= fun () ->
        match s.step with
        | L2 -> report s             (* we reached the last state *)
        | _ -> Machine.return ()


  let decay _ =
    Machine.Local.update state ~f:(fun s ->
        let length = max 0 (s.length - 1) in
        if length = 0 && s.length <> 0 then info "path has decayed";
        if length = 0 then initial_state
        else {s with length})

  let init () = Machine.sequence Primus.Interpreter.[
      eval_cond >>> on_cnd;
      jumping >>> on_jmp;
      loading >>> access ~is_load:true;
      storing >>> access ~is_load:false;
      leave_term >>> decay;
    ]
end

let () = Config.when_ready (fun _ ->
    Primus.Machine.add_component (module Tracker))

ddtbd.recipe

(parameter taint-source malloc_result "a source of the taint")
(parameter decay 100 "the number of terms while the trail is hot")
(parameter depth 10000 "a depth of analysis")
(parameter entry-points all-subroutines "where to search")
(option taint-reg ${taint-source})
(option run)
(option primus-promiscuous-mode)
(option primus-greedy-scheduler)
(option primus-limit-max-length 10000)
(option primus-propagate-taint-from-attributes)
(option report-progress)

download the provided recipes and run with

bap ./exe --recipe ddtbd

or

bap ./exe --recipe ddtbd-debug

the latter will also propagate taint to the IR terms and dump them. And create a trace file.

Hi,

BAP has updated. Now the version is 1.6.0-dev. Syntax is changed.

And could I compile this ddtbd to plugin?