Skip to content
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

Jump to bottom

adds traps for memory and division operations #840

Merged
merged 2 commits into from
Jun 8, 2018
Merged

adds traps for memory and division operations #840

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d6b29e1
adds traps for memory and division operations
ivg Jun 1, 2018
27b0465
fixes a typo in the pagefault handler function name
ivg Jun 8, 2018
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
387 changes: 244 additions & 143 deletions lib/bap_primus/bap_primus.mli
View file
Open in desktop

Large diffs are not rendered by default.

54 changes: 47 additions & 7 deletions lib/bap_primus/bap_primus_interpreter.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,15 @@ let pc_change,pc_changed =
let halting,will_halt =
Observation.provide ~inspect:sexp_of_unit "halting"

let division_by_zero,will_divide_by_zero =
Observation.provide ~inspect:sexp_of_unit "division-by-zero"

let segfault, will_segfault =
Observation.provide ~inspect:sexp_of_word "segfault"

let pagefault,page_fail =
Observation.provide ~inspect:sexp_of_word "pagefault"

let interrupt,will_interrupt =
Observation.provide ~inspect:sexp_of_int "interrupt"

Expand Down Expand Up @@ -177,18 +186,26 @@ let state = Bap_primus_machine.State.declare
curr = Top {me=prog; up=Nil};
})


type exn += Halt
type exn += Division_by_zero
type exn += Segmentation_fault of addr
type exn += Runtime_error of string

let () =
Exn.add_printer (function
| Runtime_error msg ->
Some (sprintf "Bap_primus runtime error: %s" msg)
| Halt -> Some "Halt"
| Segmentation_fault x ->
Some (asprintf "Segmentation fault at %a" Addr.pp_hex x)
| Division_by_zero -> Some "Division by zero"
| _ -> None)


let division_by_zero_handler = "__primus_division_by_zero_handler"
let pagefault_handler = "__primus_pagefault_hanlder"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Typo in the string, should be: "__primus_pagefault_handler"



module Make (Machine : Machine) = struct
open Machine.Syntax

Expand Down Expand Up @@ -226,12 +243,24 @@ module Make (Machine : Machine) = struct
Env.get v >>= fun r ->
!!on_read (v,r) >>| fun () -> r

let binop op x y =
try

let call_when_provided name =
Code.is_linked (`symbol name) >>= fun provided ->
if provided then Code.exec (`symbol name) >>| fun () -> true
else Machine.return false

let binop op x y = match op with
| Bil.DIVIDE | Bil.SDIVIDE
| Bil.MOD | Bil.SMOD
when Word.is_zero y.value ->
!!will_divide_by_zero () >>= fun () ->
call_when_provided division_by_zero_handler >>= fun called ->
if called
then undefined (Type.Imm (Word.bitwidth x.value))
else Machine.raise Division_by_zero
| _ ->
value (Bil.Apply.binop op x.value y.value) >>= fun r ->
!!on_binop ((op,x,y),r) >>| fun () -> r
with Division_by_zero -> failf "Division by zero" ()


let unop op x =
value (Bil.Apply.unop op x.value) >>= fun r ->
Expand All @@ -253,14 +282,25 @@ module Make (Machine : Machine) = struct
value c >>= fun r ->
!!on_const r >>| fun () -> r

let trapped_memory_access access =
Machine.catch access (function
| Bap_primus_memory.Pagefault a ->
!!page_fail a >>= fun () ->
call_when_provided pagefault_handler >>= fun trapped ->
if trapped then access
else
!!will_segfault a >>= fun () ->
Machine.raise (Segmentation_fault a)
| exn -> Machine.raise exn)

let load_byte a =
!!on_loading a >>= fun () ->
Memory.get a.value >>= fun r ->
trapped_memory_access (Memory.get a.value) >>= fun r ->
!!on_loaded (a,r) >>| fun () -> r

let store_byte a x =
!!on_storing a >>= fun () ->
Memory.set a.value x >>= fun () ->
trapped_memory_access (Memory.set a.value x) >>= fun () ->
!!on_stored (a,x)

let rec eval_exp x =
Expand Down
9 changes: 9 additions & 0 deletions lib/bap_primus/bap_primus_interpreter.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,9 @@ open Bap_primus_types
val pc_change : addr observation
val halting : unit observation
val interrupt : int observation
val division_by_zero : unit observation
val segfault : addr observation
val pagefault : addr observation

val loading : value observation
val loaded : (value * value) observation
Expand Down Expand Up @@ -54,6 +57,12 @@ val leave_jmp : jmp term observation


type exn += Halt
type exn += Division_by_zero
type exn += Segmentation_fault of addr

val division_by_zero_handler : string
val pagefault_handler : string


module Make (Machine : Machine) : sig
type 'a m = 'a Machine.t
Expand Down
31 changes: 27 additions & 4 deletions lib/bap_primus/bap_primus_linker.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,8 @@ let empty = {
alias = Int.Map.empty;
}

let unresolved_handler = `symbol "__primus_linker_unresolved_call"

let unresolved_handler = "__primus_linker_unresolved_call"

include struct
open Sexp
Expand All @@ -59,6 +60,10 @@ include struct
List (Atom dst :: sexp_of_args args)
end

let unbound_name,needs_unbound =
Bap_primus_observation.provide ~inspect:sexp_of_name
"linker-unbound"

module Trace = struct
module Observation = Bap_primus_observation
let exec,will_exec = Observation.provide
Expand Down Expand Up @@ -123,7 +128,6 @@ module Make(Machine : Machine) = struct
Machine.Local.get state >>| code_of_name name >>| Option.is_some

let do_fail name =
Machine.Observation.make will_fail name >>= fun () ->
Machine.Local.get state >>= fun s ->
match resolve_name s name with
| Some s -> linker_error (`symbol s)
Expand All @@ -135,8 +139,9 @@ module Make(Machine : Machine) = struct
Code.exec

let fail name =
Machine.Observation.make will_fail name >>= fun () ->
Machine.Local.get state >>= fun s ->
match code_of_name unresolved_handler s with
match code_of_name (`symbol unresolved_handler) s with
| None -> do_fail name
| Some code -> run name code

Expand All @@ -159,8 +164,26 @@ module Make(Machine : Machine) = struct
} in
{codes; terms; names; addrs; alias})


let unlink name =
Machine.Local.get state >>= fun s ->
match id_of_name name s with
| None -> Machine.return ()
| Some id ->
let cleanup = Map.filter ~f:(fun id' -> id <> id') in
Machine.Local.put state {
codes = Map.remove s.codes id;
alias = Map.remove s.alias id;
terms = cleanup s.terms;
names = cleanup s.names;
addrs = cleanup s.addrs;
}

let lookup name =
Machine.Local.get state >>| code_of_name name

let exec name =
Machine.Local.get state >>| code_of_name name >>= function
lookup name >>= function
| None -> fail name
| Some code -> run name code

Expand Down
8 changes: 8 additions & 0 deletions lib/bap_primus/bap_primus_linker.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,10 @@ type exn += Unbound_name of name

val exec : name observation
val will_exec : name statement
val unresolved : name observation

val unresolved_handler : string

module Trace : sig
val call : (string * value list) observation
val call_entered : (string * value list) statement
Expand All @@ -25,6 +29,7 @@ end

type code = (module Code)


module Name : Regular.S with type t = name

module Make(Machine : Machine) : sig
Expand All @@ -36,6 +41,9 @@ module Make(Machine : Machine) : sig
?tid:tid ->
code -> unit m

val lookup : name -> code option m
val unlink : name -> unit m

val exec : name -> unit m

val is_linked : name -> bool m
Expand Down
14 changes: 7 additions & 7 deletions lib/bap_primus/bap_primus_memory.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,11 @@ module Random = Bap_primus_random
module Generator = Bap_primus_generator
open Bap_primus_sexp

type exn += Segmentation_fault of addr
type exn += Pagefault of addr

let () = Exn.add_printer (function
| Segmentation_fault here ->
Some (asprintf "Segmentation fault at %a"
| Pagefault here ->
Some (asprintf "Page fault at %a"
Addr.pp_hex here)
| _ -> None)

Expand Down Expand Up @@ -101,10 +101,10 @@ module Make(Machine : Machine) = struct
Machine.Local.get state >>= fun s ->
Machine.Local.put state (f s)

let segfault addr = Machine.raise (Segmentation_fault addr)
let pagefault addr = Machine.raise (Pagefault addr)

let read addr {values;layers} = match find_layer addr layers with
| None -> segfault addr
| None -> pagefault addr
| Some layer -> match Map.find values addr with
| Some v -> Machine.return v
| None -> match layer.mem with
Expand All @@ -117,8 +117,8 @@ module Make(Machine : Machine) = struct

let write addr value {values;layers} =
match find_layer addr layers with
| None -> segfault addr
| Some {perms={readonly=true}} -> segfault addr
| None -> pagefault addr
| Some {perms={readonly=true}} -> pagefault addr
| Some _ -> Machine.return {
layers;
values = Map.add values ~key:addr ~data:value;
Expand Down
2 changes: 1 addition & 1 deletion lib/bap_primus/bap_primus_memory.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ open Bap_primus_types

module Generator = Bap_primus_generator

type exn += Segmentation_fault of addr
type exn += Pagefault of addr

module Make(Machine : Machine) : sig

Expand Down
59 changes: 45 additions & 14 deletions plugins/primus_promiscuous/primus_promiscuous_main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,18 @@ let assumptions blk =
| Bil.Int _ -> assns, (neg assns) :: assms
| _ -> failwith "Not in TCF") |> snd


module TrapPageFault(Machine : Primus.Machine.S) = struct
module Code = Primus.Linker.Make(Machine)
let exec =
Code.unlink (`symbol Primus.Interpreter.pagefault_handler)
end

module DoNothing(Machine : Primus.Machine.S) = struct
let exec = Machine.return ()
end


module Main(Machine : Primus.Machine.S) = struct
open Machine.Syntax
module Eval = Primus.Interpreter.Make(Machine)
Expand Down Expand Up @@ -157,20 +169,30 @@ module Main(Machine : Primus.Machine.S) = struct
| _ -> Machine.return ()


let map addr =
Mem.allocate ~generator:Primus.Generator.Random.Seeded.byte addr 1
let default_page_size = 4096
let default_generator = Primus.Generator.Random.Seeded.byte

let map_page already_mapped addr =
let rec map len =
let last = Addr.nsucc addr (len - 1) in
already_mapped last >>= function
| true -> map (len / 2)
| false ->
Mem.allocate ~generator:default_generator addr len in
map default_page_size

let trap () =
Linker.link ~name:Primus.Interpreter.pagefault_handler
(module TrapPageFault)

let make_loadable value =
let addr = Primus.Value.to_word value in
Mem.is_mapped addr >>= function
| false -> map addr
| true -> Machine.return ()
let pagefault x =
Mem.is_mapped x >>= function
| false -> map_page Mem.is_mapped x >>= trap
| true ->
Mem.is_writable x >>= function
| false -> map_page Mem.is_writable x >>= trap
| true -> Machine.return ()

let make_writable value =
let addr = Primus.Value.to_word value in
Mem.is_writable addr >>= function
| false -> map addr
| true -> Machine.return ()

let mark_visited blk =
Machine.Global.update state ~f:(fun t -> {
Expand All @@ -190,10 +212,19 @@ module Main(Machine : Primus.Machine.S) = struct
Machine.Seq.iter ~f:(fun var ->
Env.add var (Primus.Generator.static 0))

let ignore_division_by_zero =
Linker.link ~name:Primus.Interpreter.division_by_zero_handler
(module DoNothing)

let ignore_unresolved_names =
Linker.link ~name:Primus.Linker.unresolved_handler
(module DoNothing)

let init () = Machine.sequence [
setup_vars;
Primus.Interpreter.loading >>> make_loadable;
Primus.Interpreter.storing >>> make_writable;
ignore_division_by_zero;
ignore_unresolved_names;
Primus.Interpreter.pagefault >>> pagefault;
Primus.Interpreter.leave_pos >>> step;
Primus.Interpreter.leave_blk >>> mark_visited;
]
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I understand what's going on. Let me summarize and correct me if I got this wrong:

A page fault condition occurs when trying to access a page of memory that hasn't been mapped yet. This is handled by allocating a new page if the requested range is writable. This is what the trap function does. If these addresses are not writable, we don't call trap. We check whether the pagefault was trapped and if it wasn't, we raise a Segmentation_fault exception.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm testing these changes on our application.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Everything works great. 💯

Copy link
Member Author

@ivg ivg Jun 8, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A page fault condition occurs when trying to access a page of memory that hasn't been mapped yet. This is handled by allocating a new page if the requested range is writable. This is what the trap function does. If these addresses are not writable, we don't call trap. We check whether the pagefault was trapped and if it wasn't, we raise a Segmentation_fault exception.

Roughly correct, a pagefault occurs when the memory subsystem can't satisfy the request, either because of insufficient permissions or because of the missing page. Since this is a promiscuous mode, we're going to fix both cases and prevent the segmentation fault from occurring.

In the pagefault handler

  let pagefault x =
    Mem.is_mapped x >>= function
    | false -> map_page Mem.is_mapped x >>= trap
    | true ->
      Mem.is_writable x >>= function
      | false -> map_page Mem.is_writable x >>= trap
      | true -> Machine.return ()

we first check whether the page is mapped, if it is not, we map up to 4K of memory, trying not to override an existing mapping, i.e., if the new page is overlapping with an existent one, then we half the size of the new page and try again until, at the worst case, we end up with the 1 byte page mapping (this scenario could occur when 1 byte is requested just before the already mapped page, quite a common case, so a better algorithm could be devised). After the mapping we trap the pagefault by registering a handler. The handler is invoked by the memory subsystem. Since there is nothing else to do, it just unlinks itself, so that it doesn't trap the consequent pagefaults. If the page is mapped, but we still hit the pagefault, then we try to remap this region with writable permissions. (Note, the map_page function is promiscuous, it maps everything with writable permissions). Finally, if a page is present, and is writable, but pagefault is still signaled by the memory subsystem for unknown for us reason that we don't know how to handle, then we bail out without installing the trap, letting other components to deal with it.

Expand Down