Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file shadow_stack.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321(**************************************************************************)(* 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). *)(* *)(**************************************************************************)openTypesopenIrincludeCli.Make(structletname="Shadow stack protection"letshortname="shadow-stack"end)typemode=|Inline(** Use standard DBA assertions *)|Builtin(** Use new push and pop builtins *)moduleMode=Builder.Variant_choice_assoc(structtypet=modeletname="mode"letdoc="Use standard DBA assertions [Inline] or new push and pop builtins \
[Builtin]"letdefault=Inlineletassoc_map=[("inline",Inline);("builtin",Builtin)]end)typeAst.t+=Initial_stackofAst.Expr.tAst.loclistmoduleInline(P:Path.S)(S:STATE):Exec.EXTENSIONwithtypepath=P.tandtypestate=S.t=structtypepath=P.tandstate=S.tmoduleEval=Eval.Make(P)(S)letpointer_size=Kernel_options.Machine.word_size()letarray="shadow_stack"letptr=Dba.Var.create"shadow_stack_pointer"~bitsize:(Size.Bit.createpointer_size)~tag:Tempandwitness=Dba.Var.create"shadow_stack_witness"~bitsize:(Size.Bit.createpointer_size)~tag:Templetptr_r=Dba.Expr.vptrandwitness_r=Dba.Expr.vwitnessletzero=Dba.Expr.constant(Bitvector.zerospointer_size)andoffset=Dba.Expr.constant(Bitvector.of_int~size:pointer_size(pointer_size/8))letinitialization_callback=Some(fun_state->letstate=S.alloc~arraystateinS.assignptr(S.Value.constant(Bitvector.zerospointer_size))state)letdeclaration_callback=Some(fundecl(env:Script.env)pathstate->matchdeclwith|Initial_stackvalues->letoffset=S.Value.constant(Bitvector.of_int~size:pointer_size(pointer_size/8))inletptr_v,state=List.fold_left(fun(ptr_v,state)addr->letaddr=Script.eval_expr~size:env.wordsizeaddrenvinletaddr,state=Eval.safe_evaladdrstatepathin(S.Value.binaryPlusptr_voffset,S.storearray~addr:ptr_vaddrLittleEndianstate))(S.Value.constant(Bitvector.zerospointer_size),state)valuesinSome(S.assignptrptr_vstate)|_->None)letinstruction_callback=Noneletprocess_handler:typea.(moduleIr.GRAPHwithtypet=a)->a->unit=fungraph->letmoduleG=(valgraph)inletinsert_return_checkgraphvertextarget=ignore(G.insert_list_beforegraphvertex[Assert(Dba.Expr.ugtptr_rzero);Assign{var=ptr;rval=Dba.Expr.subptr_roffset};Load{var=witness;base=Somearray;dir=LittleEndian;addr=ptr_r;};Assert(Dba.Expr.equalwitness_rtarget);])infungraph->G.iter_new_vertex(funvertex->matchG.nodegraphvertexwith|Goto{tag=Call{base;_};_}|Terminator(Jump{tag=Call{base;_};_})->ignore(G.insert_list_beforegraphvertex[Store{base=Somearray;dir=LittleEndian;addr=ptr_r;rval=Dba_utils.Expr.of_vaddrbase;};Assign{var=ptr;rval=Dba.Expr.addptr_roffset};])|Goto{target;tag=Return;_}->insert_return_checkgraphvertex(Dba_utils.Expr.of_vaddrtarget)|Terminator(Jump{target;tag=Return;_})->insert_return_checkgraphvertextarget|_->())graphletprocess_callback=Someprocess_handlerletbuiltin_callback=Noneletbuiltin_printer=Noneletat_exit_callback=NoneendmoduleBuiltin(P:Path.S)(S:STATE):Exec.EXTENSIONwithtypepath=P.tandtypestate=S.t=structtypepath=P.tandstate=S.tletkey=P.register_key[]moduleEval=Eval.Make(P)(S)letinitialization_callback=Noneletinstruction_callback=Noneletdeclaration_callback=Some(fundecl(env:Script.env)pathstate->matchdeclwith|Initial_stackvalues->P.setkey(List.rev_map(funaddr->Script.eval_expr~size:env.wordsizeaddrenv)values)path;Somestate|_->None)typeIr.builtin+=PushofDba.Expr.t|PopofDba.Expr.tletprocess_handler:typea.(moduleIr.GRAPHwithtypet=a)->a->unit=fungraph->letmoduleG=(valgraph)infungraph->G.iter_new_vertex(funvertex->matchG.nodegraphvertexwith|Goto{tag=Call{base;_};_}|Terminator(Jump{tag=Call{base;_};_})->ignore(G.insert_beforegraphvertex(Builtin(Push(Dba_utils.Expr.of_vaddrbase))))|Goto{target;tag=Return;_}->ignore(G.insert_beforegraphvertex(Builtin(Pop(Dba_utils.Expr.of_vaddrtarget))))|Terminator(Jump{target;tag=Return;_})->ignore(G.insert_beforegraphvertex(Builtin(Poptarget)))|_->())graphletprocess_callback=Someprocess_handlerletpushtargetaddrpath_state=Logger.debug~level:2"%a: push(%a)"Virtual_address.ppaddrDba_printer.Ascii.pp_bl_termtarget;P.setkey(target::P.getkeypath)path;Okstateletreportaddrtargetwitnessstate=Logger.error"@[<v>%a: Stack tampering@ (goto %a, expected %a)@ %a@]"Virtual_address.ppaddrBitvector.pp_hex_or_bin(S.get_a_valuetargetstate)Bitvector.pp_hex_or_bin(S.get_a_valuewitnessstate)S.ppstateletpoptargetaddrpath_state=Logger.debug~level:2"%a: pop(%a)"Virtual_address.ppaddrDba_printer.Ascii.pp_bl_termtarget;matchP.getkeypathwith|[]->Logger.error"%a: return does not match any call"Virtual_address.ppaddr;ErrorAssertion_failed|witness::tail->(P.setkeytailpath;lettarget_v=Eval.evaltargetstateandwitness_v=Eval.evalwitnessstateinmatchS.test(S.Value.binaryEqtarget_vwitness_v)statewith|Truestate->Okstate|Falsestate->reportaddrtarget_vwitness_vstate;ErrorAssertion_failed|Both{t;f}->reportaddrtarget_vwitness_vf;Okt)letbuiltin_callback=Some(function|Pushtarget->Some(pushtarget)|Poptarget->Some(poptarget)|_->None)letbuiltin_printer=Some(funppf->function|Pushtarget->Format.fprintfppf"shadow push %a"Dba_printer.Ascii.pp_bl_termtarget;true|Poptarget->Format.fprintfppf"shadow pop %a"Dba_printer.Ascii.pp_bl_termtarget;true|_->false)letat_exit_callback=Noneendlet()=Exec.register_plugin(modulestructletname="shadow_stack"letgrammar_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_listvalues)]->(Libparser.Syntax.Decl(Initial_stack(List.revvalues)),[])|_->assertfalse);];]letinstruction_printer=Noneletdeclaration_printer=Some(funppf->function|Initial_stackvalues->Format.fprintfppf"initial call stack %a"(Format.pp_print_list~pp_sep:(funppf()->Format.pp_print_stringppf", ")(funppf(addr,_)->Script.Expr.ppppfaddr))values;true|_->false)letextension:typeab.(moduleEXPLORATION_STATISTICS)->(modulePath.Swithtypet=a)->(moduleSTATEwithtypet=b)->(moduleExec.EXTENSIONwithtypepath=aandtypestate=b)option=fun_pathstate->ifis_enabled()then(ifOptions.Logger.is_debug_enabled()thenLogger.set_log_level"debug";Logger.set_debug_level(Options.Logger.get_debug_level());matchMode.get()with|Inline->Some(moduleInline((valpath))((valstate)))|Builtin->Some(moduleBuiltin((valpath))((valstate))))elseNoneend:Exec.PLUGIN)