Browse files

adds constant tracking analysis (#872)

The analysis tracks static constants in a binary, i.e., values
are hardcoded in a program.

For the purposes of the analysis a value is a static constant if
it was initialized from a constant value or computed from a static
constant value.

The constant tracker analysis can be called from Primus Lisp using
the `all-static-constants` and `points-to-static-data` functions.
See `--primus-lisp-documentation` for the documentation on this

Along with the constant tracker this PR adds some sample analysis.

For example, check-hardcoded-values reports the
`hardcoded-socket-address` incident every time a hardcoded socket
address is used in one of the BSD Socket API function.

Another analysis is implemented in the `check-null-pointers` module
that reports a `null-pointer-dereference` incident every time a static
NULL pointer is dereferenced.
  • Loading branch information...
ivg authored and gitoleg committed Sep 18, 2018
1 parent 1338a3c commit 7096bb3fdc51f38ba0627b8a77392ae191649149
@@ -0,0 +1,15 @@
Flag constant_tracker
Description: Build the constant tracking analysis
Default: false
Library constant_tracker_plugin
Build$: flag(everything) || flag(constant_tracker)
Path: plugins/constant_tracker
BuildDepends: bap-primus
FindlibName: bap-plugin-constant_tracker
CompiledObject: best
InternalModules: Constant_tracker_main
XMETADescription: Constant Tracking Analysis based on Primus
DataFiles: lisp/*.lisp ($constant_tracker_lisp_path)
XMETAExtraLines: tags="primus, lisp, analysis"
@@ -0,0 +1,8 @@
let (/) = Filename.concat
let () =
add_variable ~doc:"where to install the library"
| None -> BaseEnv.var_get "datadir" / "primus" / "site-lisp"
| Some path -> path)
@@ -1,5 +1,5 @@
Flag primus_test
Description: Build Primus Lisp Library
Description: Build Primus Lisp Program Testing Framework
Default: false
@@ -69,6 +69,7 @@ install: [
["ocamlfind" "remove" "bap-plugin-primus_region"]
["ocamlfind" "remove" "bap-plugin-primus_taint"]
["ocamlfind" "remove" "bap-plugin-primus_test"]
["ocamlfind" "remove" "bap-plugin-constant_tracker"]
["ocamlfind" "remove" "bap-plugin-primus_dictionary"]
["ocamlfind" "remove" "bap-plugin-primus_greedy"]
["ocamlfind" "remove" "bap-plugin-primus_exploring"]
@@ -155,6 +156,7 @@ remove: [
["ocamlfind" "remove" "bap-plugin-primus_region"]
["ocamlfind" "remove" "bap-plugin-primus_taint"]
["ocamlfind" "remove" "bap-plugin-primus_test"]
["ocamlfind" "remove" "bap-plugin-constant_tracker"]
["ocamlfind" "remove" "bap-plugin-primus_dictionary"]
["ocamlfind" "remove" "bap-plugin-primus_greedy"]
["ocamlfind" "remove" "bap-plugin-primus_exploring"]
@@ -0,0 +1,3 @@
PKG bap
PKG bap-primus
FLG -short-paths,-open Bap.Std,-open Bap_primus.Std
@@ -0,0 +1,106 @@
open Core_kernel
open Bap.Std
open Bap_primus.Std
include Self()
type state = {
consts : Primus.Value.Id.Set.t;
let state = Primus.Machine.State.declare
(fun _ -> {consts = Primus.Value.Id.Set.empty})
let is_const x {consts} =
Set.mem consts ( x)
let all_consts xs s =
List.for_all xs ~f:(fun x -> is_const x s)
let declare_const v {consts} = {
consts = Set.add consts ( v)
module IsConst(Machine : Primus.Machine.S) = struct
open Machine.Syntax
module Value = Primus.Value.Make(Machine)
let run inputs =
Machine.Local.get state >>| all_consts inputs >>= function
| true -> Value.b1
| false -> Value.b0
module IsConstBuffer(Machine : Primus.Machine.S) = struct
open Machine.Syntax
module Value = Primus.Value.Make(Machine)
module Memory = Primus.Memory.Make(Machine)
let points_to_static_data s ptr len =
let rec check ptr len =
if Word.is_zero len
then Value.b1
Memory.get ptr >>= fun v ->
if is_const v s
then check (Addr.succ ptr) (Word.pred len)
else Value.b0 in
check (Value.to_word ptr) (Value.to_word len)
[@@@warning "-P"]
let run [ptr; len] =
Machine.Local.get state >>= fun s ->
points_to_static_data s ptr len
module Tracker(Machine : Primus.Machine.S) = struct
open Machine.Syntax
let intro v = Machine.Local.update state ~f:(declare_const v)
let propagate inputs output =
Machine.Local.get state >>= fun s ->
if all_consts inputs s
then Machine.Local.put state (declare_const output s)
else Machine.return ()
let prop_binop ((op,x,y),z) = propagate [x;y] z
let prop_unop ((op,x),z) = propagate [x] z
let prop_cast ((c,_,x),z) = propagate [x] z
let prop_extract ((_,_,x),z) = propagate [x] z
let prop_concat ((x,y),z) = propagate [x;y] z
let declare_interface =
let module Lisp = Primus.Lisp.Make(Machine) in
let open Primus.Lisp.Type.Spec in
Machine.sequence [
Lisp.define "all-static-constant" (module IsConst)
~types:(all int @-> bool)
~docs:"(all-static-constant X Y ..) is true if X,Y,... are static constants.
A value is a static constant if it was initialized from a constant
value or computed from static constant values. ";
Lisp.define "points-to-static-data" (module IsConstBuffer)
~types:(tuple [int; int] @-> bool)
~docs: "(points-to-static-data PTR LEN) is true iff
(all-static-constant *PTR .. *(PTR+LEN-1))"
let init () = Machine.sequence Primus.Interpreter.[
const >>> intro;
binop >>> prop_binop;
unop >>> prop_unop;
cast >>> prop_cast;
extract >>> prop_extract;
concat >>> prop_concat;
let enable = Config.flag "enable"
let () = Config.when_ready (fun {Config.get} ->
if get enable then
Primus.Machine.add_component (module Tracker))
@@ -0,0 +1,12 @@
(defun check-hardcoded-socket-address (sockaddr-ptr)
(when (points-to-static-data sockaddr-ptr 16)
(incident-report 'hardcoded-socket-address (incident-location))))
(defmethod call (name fd addr)
(when (is-in name 'accept 'bind 'connect)
(check-hardcoded-socket-address addr)))
(defmethod call (name fd buf size flags addr len)
(when (is-in name 'sendto 'recvfrom)
(check-hardcoded-socket-address addr)))
@@ -0,0 +1,9 @@
(defun check-null-pointer (ptr)
(when (and (not ptr) (all-static-constants ptr))
(incident-report 'null-pointer-dereference (incident-location))))
(defmethod loading (ptr)
(check-null-pointer ptr))
(defmethod storing (ptr)
(check-null-pointer ptr))

0 comments on commit 7096bb3

Please sign in to comment.