package binsec
Semantic analysis of binary executables
Install
Dune Dependency
Authors
-
AAdel Djoudi
-
BBenjamin Farinier
-
CChakib Foulani
-
DDorian Lesbre
-
FFrédéric Recoules
-
GGuillaume Girol
-
JJosselin Feist
-
LLesly-Ann Daniel
-
MMahmudul Faisal Al Ameen
-
MManh-Dung Nguyen
-
MMathéo Vergnolle
-
MMathilde Ollivier
-
MMatthieu Lemerre
-
NNicolas Bellec
-
OOlivier Nicole
-
RRichard Bonichon
-
RRobin David
-
SSébastien Bardin
-
SSoline Ducousso
-
TTa Thanh Dinh
-
YYaëlle Vinçont
-
YYanis Sellami
Maintainers
Sources
binsec-0.10.1.tbz
sha256=87d4048c9a90c8a14ee029e77d31032a15427f06416a31938cec8a68394234c4
sha512=6a023d2a5c87c56b0aac489874431d8dcccee1451a072a826190be3a7f75a961688bab95f193f494231744abc3bc9733ab5c809057d36a5e4d24c6c29c369144
doc/src/shadow_stack/shadow_stack.ml.html
Source file shadow_stack.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321
(**************************************************************************) (* This file is part of BINSEC. *) (* *) (* Copyright (C) 2016-2025 *) (* CEA (Commissariat à l'énergie atomique et aux énergies *) (* alternatives) *) (* *) (* you can redistribute it and/or modify it under the terms of the GNU *) (* Lesser General Public License as published by the Free Software *) (* Foundation, version 2.1. *) (* *) (* It is distributed in the hope that it will be useful, *) (* but WITHOUT ANY WARRANTY; without even the implied warranty of *) (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) (* GNU Lesser General Public License for more details. *) (* *) (* See the GNU Lesser General Public License version 2.1 *) (* for more details (enclosed in the file licenses/LGPLv2.1). *) (* *) (**************************************************************************) open Types open Ir include Cli.Make (struct let name = "Shadow stack protection" let shortname = "shadow-stack" end) type mode = | Inline (** Use standard DBA assertions *) | Builtin (** Use new push and pop builtins *) module Mode = Builder.Variant_choice_assoc (struct type t = mode let name = "mode" let doc = "Use standard DBA assertions [Inline] or new push and pop builtins \ [Builtin]" let default = Inline let assoc_map = [ ("inline", Inline); ("builtin", Builtin) ] end) type Ast.t += Initial_stack of Ast.Expr.t Ast.loc list module Inline (P : Path.S) (S : STATE) : Exec.EXTENSION with type path = P.t and type state = S.t = struct type path = P.t and state = S.t module Eval = Eval.Make (P) (S) let pointer_size = Kernel_options.Machine.word_size () let array = "shadow_stack" let ptr = Dba.Var.create "shadow_stack_pointer" ~bitsize:(Size.Bit.create pointer_size) ~tag:Temp and witness = Dba.Var.create "shadow_stack_witness" ~bitsize:(Size.Bit.create pointer_size) ~tag:Temp let ptr_r = Dba.Expr.v ptr and witness_r = Dba.Expr.v witness let zero = Dba.Expr.constant (Bitvector.zeros pointer_size) and offset = Dba.Expr.constant (Bitvector.of_int ~size:pointer_size (pointer_size / 8)) let initialization_callback = Some (fun _ state -> let state = S.alloc ~array state in S.assign ptr (S.Value.constant (Bitvector.zeros pointer_size)) state) let declaration_callback = Some (fun decl (env : Script.env) path state -> match decl with | Initial_stack values -> let offset = S.Value.constant (Bitvector.of_int ~size:pointer_size (pointer_size / 8)) in let ptr_v, state = List.fold_left (fun (ptr_v, state) addr -> let addr = Script.eval_expr ~size:env.wordsize addr env in let addr, state = Eval.safe_eval addr state path in ( S.Value.binary Plus ptr_v offset, S.store array ~addr:ptr_v addr LittleEndian state )) (S.Value.constant (Bitvector.zeros pointer_size), state) values in Some (S.assign ptr ptr_v state) | _ -> None) let instruction_callback = None let process_handler : type a. (module Ir.GRAPH with type t = a) -> a -> unit = fun graph -> let module G = (val graph) in let insert_return_check graph vertex target = ignore (G.insert_list_before graph vertex [ Assert (Dba.Expr.ugt ptr_r zero); Assign { var = ptr; rval = Dba.Expr.sub ptr_r offset }; Load { var = witness; base = Some array; dir = LittleEndian; addr = ptr_r; }; Assert (Dba.Expr.equal witness_r target); ]) in fun graph -> G.iter_new_vertex (fun vertex -> match G.node graph vertex with | Goto { tag = Call { base; _ }; _ } | Terminator (Jump { tag = Call { base; _ }; _ }) -> ignore (G.insert_list_before graph vertex [ Store { base = Some array; dir = LittleEndian; addr = ptr_r; rval = Dba_utils.Expr.of_vaddr base; }; Assign { var = ptr; rval = Dba.Expr.add ptr_r offset }; ]) | Goto { target; tag = Return; _ } -> insert_return_check graph vertex (Dba_utils.Expr.of_vaddr target) | Terminator (Jump { target; tag = Return; _ }) -> insert_return_check graph vertex target | _ -> ()) graph let process_callback = Some process_handler let builtin_callback = None let builtin_printer = None let at_exit_callback = None end module Builtin (P : Path.S) (S : STATE) : Exec.EXTENSION with type path = P.t and type state = S.t = struct type path = P.t and state = S.t let key = P.register_key [] module Eval = Eval.Make (P) (S) let initialization_callback = None let instruction_callback = None let declaration_callback = Some (fun decl (env : Script.env) path state -> match decl with | Initial_stack values -> P.set key (List.rev_map (fun addr -> Script.eval_expr ~size:env.wordsize addr env) values) path; Some state | _ -> None) type Ir.builtin += Push of Dba.Expr.t | Pop of Dba.Expr.t let process_handler : type a. (module Ir.GRAPH with type t = a) -> a -> unit = fun graph -> let module G = (val graph) in fun graph -> G.iter_new_vertex (fun vertex -> match G.node graph vertex with | Goto { tag = Call { base; _ }; _ } | Terminator (Jump { tag = Call { base; _ }; _ }) -> ignore (G.insert_before graph vertex (Builtin (Push (Dba_utils.Expr.of_vaddr base)))) | Goto { target; tag = Return; _ } -> ignore (G.insert_before graph vertex (Builtin (Pop (Dba_utils.Expr.of_vaddr target)))) | Terminator (Jump { target; tag = Return; _ }) -> ignore (G.insert_before graph vertex (Builtin (Pop target))) | _ -> ()) graph let process_callback = Some process_handler let push target addr path _ state = Logger.debug ~level:2 "%a: push(%a)" Virtual_address.pp addr Dba_printer.Ascii.pp_bl_term target; P.set key (target :: P.get key path) path; Ok state let report addr target witness state = Logger.error "@[<v>%a: Stack tampering@ (goto %a, expected %a)@ %a@]" Virtual_address.pp addr Bitvector.pp_hex_or_bin (S.get_a_value target state) Bitvector.pp_hex_or_bin (S.get_a_value witness state) S.pp state let pop target addr path _ state = Logger.debug ~level:2 "%a: pop(%a)" Virtual_address.pp addr Dba_printer.Ascii.pp_bl_term target; match P.get key path with | [] -> Logger.error "%a: return does not match any call" Virtual_address.pp addr; Error Assertion_failed | witness :: tail -> ( P.set key tail path; let target_v = Eval.eval target state and witness_v = Eval.eval witness state in match S.test (S.Value.binary Eq target_v witness_v) state with | True state -> Ok state | False state -> report addr target_v witness_v state; Error Assertion_failed | Both { t; f } -> report addr target_v witness_v f; Ok t) let builtin_callback = Some (function | Push target -> Some (push target) | Pop target -> Some (pop target) | _ -> None) let builtin_printer = Some (fun ppf -> function | Push target -> Format.fprintf ppf "shadow push %a" Dba_printer.Ascii.pp_bl_term target; true | Pop target -> Format.fprintf ppf "shadow pop %a" Dba_printer.Ascii.pp_bl_term target; true | _ -> false) let at_exit_callback = None end let () = Exec.register_plugin (module struct let name = "shadow_stack" let grammar_extension = [ Dyp.Add_rules [ ( ( "decl", [ Dyp.Regexp (RE_String "initial"); Dyp.Regexp (RE_String "call"); Dyp.Regexp (RE_String "stack"); Dyp.Non_ter ("comma_separated_expr_rev_list", No_priority); ], "default_priority", [] ), fun _ -> function | [ _; _; _; Libparser.Syntax.Obj (Script.Expr_list values) ] -> ( Libparser.Syntax.Decl (Initial_stack (List.rev values)), [] ) | _ -> assert false ); ]; ] let instruction_printer = None let declaration_printer = Some (fun ppf -> function | Initial_stack values -> Format.fprintf ppf "initial call stack %a" (Format.pp_print_list ~pp_sep:(fun ppf () -> Format.pp_print_string ppf ", ") (fun ppf (addr, _) -> Script.Expr.pp ppf addr)) values; true | _ -> false) let extension : type a b. (module EXPLORATION_STATISTICS) -> (module Path.S with type t = a) -> (module STATE with type t = b) -> (module Exec.EXTENSION with type path = a and type state = b) option = fun _ path state -> if is_enabled () then ( if Options.Logger.is_debug_enabled () then Logger.set_log_level "debug"; Logger.set_debug_level (Options.Logger.get_debug_level ()); match Mode.get () with | Inline -> Some (module Inline ((val path)) ((val state))) | Builtin -> Some (module Builtin ((val path)) ((val state)))) else None end : Exec.PLUGIN)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>