package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file components.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
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    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 Cil_types
open Cil_datatype

open Pdg_types

(* ************************************************************************* *)
(** {2 Searching security annotations} *)
(* ************************************************************************* *)
(*
(** The state of statement for which a security verification should occur. *)
module Security_Annotations =
  Cil_computation.StmtSetRef
    (struct
       let name = "Components.Annotations"
       let dependencies = [ Ast.self ]
     end)

let rec is_security_predicate p = match p.content with
  | Pand(p1, p2) -> is_security_predicate p1 || is_security_predicate p2
  | (* [state(lval) op term] *)
      Prel(_,
           { term_node = Tapp(f1, _ , ([ _ ])) },
           { term_node = TLval(TVar _,_) })
        when f1.l_var_info.lv_name = Model.state_name ->
      true
  | (* [state(lval) op term] *)
      Prel(_,
           { term_node = Tapp(f1, _, [ _ ]) },
           { term_node = _ })
        when f1.l_var_info.lv_name = Model.state_name ->
      assert false
  | _ ->
      false

let has_security_requirement kf =
  List.exists (is_security_predicate $ Logic_const.pred_of_id_pred)
    (Kernel_function.get_spec kf).spec_requires

(* Do not called twice. *)
let search_security_requirements () =
  if Security_Annotations.is_empty () then begin
    Security_slicing_parameters.feedback
      ~level:3 "searching security annotations";
    (* TODO: chercher dans les GlobalAnnotations *)
    let is_security_annotation a =
         (match a.annot_content with
           | AAssert (_behav,p,_) -> is_security_predicate p
           | AStmtSpec { spec_requires = l } ->
               List.exists
                 (is_security_predicate $ Logic_const.pred_of_id_pred) l
           | APragma _
           | AInvariant _ (* | ALoopBehavior _ *)
               (* [JS 2008/02/26] may contain a security predicate *)
           | AVariant _ | AAssigns _
               -> false)
    in
    Annotations.iter
      (fun s annotations ->
         if
           Value.is_reachable_stmt s
           && List.exists
             (function Before a | After a -> is_security_annotation a)
             !annotations
         then
           Security_Annotations.add s);
    Globals.Functions.iter
      (fun kf ->
         if has_security_requirement kf  then
           List.iter
             (fun (_, callsites) ->
                List.iter Security_Annotations.add callsites)
             (!Value.callers kf));
  end
*)
(* ************************************************************************* *)
(** {2 Computing security components} *)
(* ************************************************************************* *)

open PdgIndex

let get_node_stmt node = Key.stmt (Pdg.Api.node_key node)

module NodeKf = Datatype.Pair(PdgTypes.Node)(Kernel_function)

(* type bwd_kind = Direct | Indirect
   type fwd_kind = Impact | Security
   type kind =
   | Backward of bwd_kind
   | Forward of fwd_kind

   (** Debugging purpose only *)
   let pretty_kind fmt = function
   | Backward Direct -> Format.fprintf fmt "backward direct"
   | Backward Indirect -> Format.fprintf fmt "backward indirect"
   | Forward Security -> Format.fprintf fmt "forward"
   | Forward Impact -> Format.fprintf fmt "impact"
*)

(* Never plugged in. To be tested.
   module Memo : sig
   val init: kind -> kernel_function -> unit
   val push_function: stmt -> kernel_function -> unit
   val pop_function: unit -> unit
   val memo:
    Pdg.t_node ->
    (unit -> (Pdg.t_node * kernel_function) list) ->
    (Pdg.t_node * kernel_function) list
   end = struct

   module Callstack = struct

    type t =
        { mutable stack: (stmt * kernel_function) list;
          mutable current_kf: kernel_function }

    let init kf callstack = callstack.stack <- []; callstack.current_kf <- kf

    let push stmt kf stack =
      stack.stack <- (stmt, stack.current_kf) :: stack.stack;
      stack.current_kf <- kf

    let pop stack =
      let kf = match stack.stack with [] -> assert false | (_, k) :: _ -> k in
      stack.current_kf <- kf

    let equal s1 s2 =
      Kernel_function.equal s1.current_kf s2.current_kf
      && try
        List.iter2
          (fun (s1, kf1) (s2, kf2) ->
             if not (s1.sid = s2.sid && Kernel_function.equal kf1 kf2) then
               raise Exit)
          s1.stack s2.stack;
        true
      with Exit ->
        false

    let hash = Hashtbl.hash

   end

   (* *********************************************************************** *)
   (* state: kind -> callstack -> (node * kf) -> (node * kf) list *)

   module Nodekfs = Hashtbl.Make(NodeKf) (* (node * kf) -> (node * kf) list *)

   module Callstacks = struct
    include Hashtbl.Make(Callstack) (* callstack -> nodekfs *)
    let memo tbl c =
      try find tbl c
      with Not_found -> let t = Nodekfs.create 7 in replace tbl c t; t
   end

   module Memo = struct
    include Hashtbl
    let memo tbl k callstack =
      try
        let callstacks = find tbl k in
        Callstacks.memo callstacks callstack
      with Not_found ->
        let callstacks = Callstacks.create 7 in
        let t = Nodekfs.create 7 in
        Callstacks.replace callstacks callstack t;
        replace tbl k callstacks;
        t
   end

   type local_tbl = (Pdg.t_node * kernel_function) list Nodekfs.t

   type state =
      { mutable kind: kind;
        mutable callstack: Callstack.t;
        mutable local_tbl: local_tbl;
        memo_tbl: (kind, local_tbl Callstacks.t) Memo.t; }
   (* *********************************************************************** *)

   let state =
    let spec = Cil.empty_funspec () in
    { kind = Backward Direct;
      callstack =
        { Callstack.stack = [];
          current_kf =
            { fundec =
                (* do not use Cil.emptyFunction here since it changes the
                   numbering of variables *)
                Declaration
                  (spec,
                   Cil_datatype.Varinfo.dummy,
                   None,
                   Cil_datatype.Location.unknown);
              return_stmt = None;
              spec = Cil.empty_funspec () } };
      local_tbl = Nodekfs.create 0;
      memo_tbl = Hashtbl.create 5 }

   let update () =
    state.local_tbl <- Memo.memo state.memo_tbl state.kind state.callstack

   let init k kf =
    state.kind <- k;
    Callstack.init kf state.callstack;
    update ()

   let push_function stmt kf =
    Callstack.push stmt kf state.callstack;
    update ()

   let pop_function () =
    Callstack.pop state.callstack;
    update ()

   let memo node f =
    let key = node, state.callstack.Callstack.current_kf in
    try
      Nodekfs.find state.local_tbl key
    with Not_found ->
      let value = f () in
      Nodekfs.replace state.local_tbl key value;
      value

   end
*)

(* used to enforce an invariant on [add] *)
module Todolist : sig
  type todo = private
    { node: PdgTypes.Node.t;
      kf: kernel_function;
      pdg: Pdg.Api.t;
      callstack_length: int;
      from_deep: bool }
  type t = todo list
  val mk_init: kernel_function -> Pdg.Api.t -> PdgTypes.Node.t list -> todo list
  val add:
    PdgTypes.Node.t -> kernel_function -> Pdg.Api.t -> int -> bool -> t -> t
end = struct

  type todo =
    { node: PdgTypes.Node.t;
      kf: kernel_function;
      pdg: Pdg.Api.t;
      callstack_length: int;
      from_deep: bool }

  type t = todo list

  let add n kf pdg len fd list =
    match Pdg.Api.node_key n with
    | Key.SigKey (Signature.In Signature.InCtrl) ->
      (* do not consider node [InCtrl]  *)
      list
    | Key.VarDecl vi when not (Kernel.LibEntry.get () && vi.vglob) ->
      (* do not consider variable declaration,
         except if libEntry is set and they are globals
         (i.e. we could have no further info about them) *)
      list
    | _ ->
      Security_slicing_parameters.debug ~level:2 "adding node %a (in %s)"
        (Pdg.Api.pretty_node false) n
        (Kernel_function.get_name kf);
      { node = n; kf = kf; pdg = pdg;
        callstack_length = len; from_deep = fd }
      :: list

  let mk_init kf pdg =
    List.fold_left (fun acc n -> add n kf pdg 0 false acc) []

end

module Component = struct

  (* not optimal implementation: no memoization (bts#006) *)

  module M = Map.Make(NodeKf)

  type fwd_kind = Impact | Security

  type kind =
    | Direct
    | Indirect_Backward
    | Forward of fwd_kind

  type value =
    { pdg: Pdg.Api.t;
      mutable callstack_length: int;
      mutable direct: bool;
      mutable indirect_backward: bool;
      mutable forward: bool }

  type t = value M.t

  let is_direct v = v.direct
  let is_indirect_backward v = v.indirect_backward && not v.direct
  let is_forward v = not (v.direct || v.indirect_backward)

  (** Returns [found, new_already] with:
      - [found] is [true] iff [elt] was previously added for [kind]
      - [new_already] is [already] updated with [elt] and its (new) associated
        value. *)
  let check_and_add first elt kind pdg len (already: t) =
    try
      (*        Format.printf "[security] check node %a (in %s, kind %a)@."
                (!Pdg.pretty_node true) (fst elt)
                (Kernel_function.get_name (snd elt))
                pretty_kind kind;*)
      let v = M.find elt already in
      let found, dir, up, down = match kind with
        | Direct -> true, true, false, false
        | Indirect_Backward -> v.indirect_backward, v.direct, true, false
        | Forward _ -> v.forward, v.direct, v.indirect_backward, true
      in
      v.callstack_length <- min v.callstack_length len;
      v.direct <- dir;
      v.indirect_backward <- up;
      v.forward <- down;
      found, already
    with Not_found ->
      let dir, up, down = match kind with
        | Direct -> true, false, false
        | Indirect_Backward -> false, true, false
        | Forward _ -> false, false, true
      in
      let v =
        { pdg = pdg; callstack_length = len;
          direct = dir; indirect_backward = up; forward = down }
      in
      false,
      if first && kind = Forward Impact then
        (* do not add the initial selected stmt for an impact analysis.
           fixed FS#411 *)
        already
      else
        M.add elt v already

  let one_step_related_nodes kind pdg node =
    (* do not consider address dependencies now (except for impact analysis):
       just consider them during the last slicing pass
       (for semantic preservation of pointers) *)
    let direct node = Pdg.Api.direct_data_dpds pdg node in
    match kind with
    | Direct -> direct node
    | Indirect_Backward -> direct node @ Pdg.Api.direct_ctrl_dpds pdg node
    | Forward Security ->
      Pdg.Api.direct_data_uses pdg node @ Pdg.Api.direct_ctrl_uses pdg node
    | Forward Impact ->
      Pdg.Api.direct_data_uses pdg node @ Pdg.Api.direct_ctrl_uses pdg node
      @ Pdg.Api.direct_addr_uses pdg node

  let search_input kind kf lazy_l =
    try
      match kind with
      | Forward _ -> Lazy.force lazy_l
      | Direct | Indirect_Backward ->
        if Eva.Analysis.use_spec_instead_of_definition kf
        then Lazy.force lazy_l
        else []
    with Not_found ->
      []

  let add_from_deep caller todo n =
    Todolist.add n caller (Pdg.Api.get caller) 0 true todo

  let forward_caller kf node todolist =
    let pdg = Pdg.Api.get kf in
    List.fold_left
      (fun todolist (caller, callsites) ->
         (* foreach caller *)
         List.fold_left
           (fun todolist callsite ->
              let nodes =
                Pdg.Api.find_call_out_nodes_to_select
                  pdg (PdgTypes.NodeSet.singleton node) (Pdg.Api.get caller) callsite
              in
              List.fold_left
                (add_from_deep caller)
                todolist
                nodes)
           todolist
           callsites)
      todolist
      (Eva.Results.callsites kf)

  let related_nodes_of_nodes kind result nodes =
    let initial_nodes =
      List.map (fun n -> n.Todolist.node, n.Todolist.kf) nodes
    in
    let rec aux first result = function
      | [] -> result
      | { Todolist.node = node; kf = kf; pdg = pdg;
          callstack_length = callstack_length; from_deep = from_deep }
        :: todolist
        ->
        let elt = node, kf in
        let found, result =
          check_and_add first elt kind pdg callstack_length result
        in
        let todolist =
          if found then begin
            todolist
          end else begin
            Security_slicing_parameters.debug
              ~level:2 "considering node %a (in %s)"
              (Pdg.Api.pretty_node false) node
              (Kernel_function.get_name kf);
            (* intraprocedural related_nodes *)
            let related_nodes = one_step_related_nodes kind pdg node in
            Security_slicing_parameters.debug ~level:3
              "intraprocedural part done";
            let todolist =
              List.fold_left
                (fun todo n ->
                   Todolist.add n kf pdg callstack_length false todo)
                todolist
                related_nodes
            in
            (* interprocedural part *)
            let backward_from_deep compute_nodes =
              (* [TODO optimisation:]
                 en fait, regarder from_deep:
                 si vrai, faire pour chaque caller
                 sinon, faire uniquement pour le caller d'où on vient *)
              match kind, callstack_length with
              | (Direct | Indirect_Backward), 0 ->
                (* input of a deep security annotation: foreach call
                   to [kf], compute its related nodes *)
                let do_caller todolist (caller, callsites) =
                  (* Format.printf "[security of %s] search callers in %s
                     for zone %a@."  (Kernel_function.get_name kf)
                     (Kernel_function.get_name caller)
                     Locations.Zone.pretty zone;*)
                  let pdg_caller = Pdg.Api.get caller in
                  let do_call todolist callsite =
                    match kind with
                    | Direct | Indirect_Backward ->
                      let nodes = compute_nodes pdg_caller callsite in
                      List.fold_left
                        (add_from_deep caller) todolist nodes
                    | Forward _ ->
                      todolist (* not considered here, see at end *)
                  in
                  List.fold_left do_call todolist callsites
                in
                List.fold_left do_caller todolist (Eva.Results.callsites kf)
              | _ ->
                todolist
            in
            let todolist =
              match Pdg.Api.node_key node with
              | Key.SigKey (Signature.In Signature.InCtrl) ->
                assert false
              | Key.SigKey (Signature.In (Signature.InImpl zone)) ->
                let compute_nodes pdg_caller callsite =
                  let nodes, _undef_zone =
                    Pdg.Api.find_location_nodes_at_stmt
                      pdg_caller callsite ~before:true zone
                      (* TODO : use undef_zone (see FS#201)? *)
                  in
                  let nodes = List.map (fun (n, _z_part) -> n) nodes in
                  (* TODO : use _z_part ? *)
                  nodes
                in
                backward_from_deep compute_nodes
              | Key.SigKey key ->
                let compute_nodes pdg_caller callsite =
                  [ match key with
                    | Signature.In (Signature.InNum n) ->
                      Pdg.Api.find_call_input_node pdg_caller callsite n
                    | Signature.Out Signature.OutRet  ->
                      Pdg.Api.find_call_output_node pdg_caller callsite
                    | Signature.In
                        (Signature.InCtrl | Signature.InImpl _)
                    | Signature.Out _ ->
                      assert false ]
                in
                backward_from_deep compute_nodes
              | Key.SigCallKey(id, key) ->
                (* the node is a call: search the related nodes inside the
                   called function (see FS#155) *)
                if from_deep then
                  (* already come from a deeper annotation:
                     do not go again inside it *)
                  todolist
                else
                  let stmt = Key.call_from_id id in
                  let called_kfs = Eva.Results.callee stmt in
                  let todolist =
                    List.fold_left
                      (fun todolist called_kf ->
                         (* foreach called kf *)
                         (*Format.printf
                           "[security] search inside %s (from %s)@."
                           (Kernel_function.get_name called_kf)
                           (Kernel_function.get_name kf);*)
                         let called_pdg = Pdg.Api.get called_kf in
                         let nodes =
                           try
                             match kind, key with
                             | (Direct | Indirect_Backward),
                               Signature.Out out_key  ->
                               let nodes, _undef_zone =
                                 Pdg.Api.find_output_nodes called_pdg out_key
                                 (* TODO: use undef_zone (see FS#201) *)
                               in
                               let nodes =
                                 List.map (fun (n, _z_part) -> n) nodes in
                               (* TODO : use _z_part ? *)
                               nodes
                             | _, Signature.In (Signature.InNum n) ->
                               search_input kind called_kf
                                 (lazy [Pdg.Api.find_input_node called_pdg n])
                             | _, Signature.In Signature.InCtrl ->
                               search_input kind called_kf
                                 (lazy
                                   [Pdg.Api.find_entry_point_node called_pdg])
                             | _, Signature.In (Signature.InImpl _) ->
                               assert false
                             | Forward _, Signature.Out _ ->
                               []
                           with
                           | Pdg.Api.Top ->
                             Security_slicing_parameters.warning
                               "no precise pdg for function %s. \n\
                                Ignoring this function in the analysis (potentially incorrect results)."
                               (Kernel_function.get_name called_kf);
                             []
                           | Pdg.Api.Bottom | Not_found -> assert false
                         in
                         List.fold_left
                           (fun todo n ->
                              (*Format.printf "node %a inside %s@."
                                (Pdg.Api.pretty_node false) n
                                (Kernel_function.get_name called_kf);*)
                              Todolist.add
                                n called_kf called_pdg
                                (callstack_length + 1) false todo)
                           todolist
                           nodes)
                      todolist
                      called_kfs
                  in
                  (match kind with
                   | Direct | Indirect_Backward ->
                     todolist
                   | Forward _ ->
                     List.fold_left
                       (fun todolist called_kf ->
                          let compute_from_stmt fold =
                            fold
                              (fun (n, kfn) _ acc ->
                                 if Kernel_function.equal kfn kf then n :: acc
                                 else acc)
                          in
                          let from_stmt =
                            compute_from_stmt M.fold result [] in
                          let from_stmt =
                            (* initial nodes may be not in results *)
                            compute_from_stmt
                              (fun f e acc ->
                                 List.fold_left
                                   (fun acc e -> f e [] acc) acc e)
                              initial_nodes
                              from_stmt
                          in
                          let from_stmt = List.fold_left
                              (fun s n -> PdgTypes.NodeSet.add n s)
                              PdgTypes.NodeSet.empty from_stmt in
                          let called_pdg = Pdg.Api.get called_kf in
                          let nodes =
                            try
                              Pdg.Api.find_in_nodes_to_select_for_this_call
                                pdg from_stmt stmt called_pdg
                            with
                            | Pdg.Api.Top ->
                              (* warning already emitted in the previous fold *)
                              []
                            | Pdg.Api.Bottom | Not_found -> assert false
                          in
                          List.fold_left
                            (fun todo n ->
                               Todolist.add
                                 n called_kf called_pdg
                                 (callstack_length + 1) false todo)
                            todolist
                            nodes)
                       todolist
                       called_kfs)
              | Key.CallStmt _ | Key.VarDecl _ ->
                assert false
              | Key.Stmt _ | Key.Label _ ->
                todolist
            in
            (* [TODO optimisation:] voir commentaire plus haut *)
            match kind with
            | (Direct | Indirect_Backward) -> todolist
            | Forward _ -> forward_caller kf node todolist
          end
        in
        (* recursive call *)
        aux false result todolist
    in
    aux true result nodes

  let initial_nodes kf stmt =
    Security_slicing_parameters.debug
      ~level:3 "computing initial nodes for %d" stmt.sid;
    let pdg = Pdg.Api.get kf in
    let nodes =
      if Eva.Results.is_reachable stmt then
        try Pdg.Api.find_simple_stmt_nodes pdg stmt
        with Not_found -> assert false
      else begin
        Security_slicing_parameters.debug
          ~level:3 "stmt %d is dead. skipping." stmt.sid;
        []
      end
    in
    Todolist.mk_init kf pdg nodes

  let direct kf stmt =
    try
      let nodes = initial_nodes kf stmt in
      Security_slicing_parameters.debug
        "computing direct component %d" stmt.sid;
      let res = related_nodes_of_nodes Direct M.empty nodes in
      (* add the initial node, fix FS#180 *)
      let mk p =
        { pdg = p; callstack_length = 0;
          direct = true; indirect_backward = false; forward = false }
      in
      let res =
        List.fold_left
          (fun acc { Todolist.node=n; kf=f; pdg=p } -> M.add (n,f) (mk p) acc)
          res
          nodes
      in
      res
    with Pdg.Api.Top | Pdg.Api.Bottom ->
      Security_slicing_parameters.warning "PDG is not manageable. skipping.";
      M.empty

  let backward kf stmt =
    try
      let nodes = initial_nodes kf stmt in
      let res = direct kf stmt in
      Security_slicing_parameters.debug
        "computing backward indirect component for %d" stmt.sid;
      related_nodes_of_nodes Indirect_Backward res nodes
    with Pdg.Api.Top | Pdg.Api.Bottom ->
      Security_slicing_parameters.warning "PDG is not manageable. skipping.";
      M.empty

  let whole kf stmt =
    let res = backward kf stmt in
    let from =
      M.fold
        (fun (n,kf) v acc ->
           Todolist.add n kf v.pdg v.callstack_length false(*?*) acc)
        res
        []
    in
    Security_slicing_parameters.debug
      "computing forward component for stmt %d" stmt.sid;
    related_nodes_of_nodes (Forward Security) res from

  (* is exactly an impact analysis iff [fwd_kind = Impact] *)
  let forward fwd_kind kf stmt =
    let nodes = initial_nodes kf stmt in
    Security_slicing_parameters.debug
      "computing forward component for stmt %d" stmt.sid;
    let res = related_nodes_of_nodes (Forward fwd_kind) M.empty nodes in
    let set =
      M.fold
        (fun (n,_) _ acc ->
           Option.fold
             ~none:acc
             ~some:(fun s -> Stmt.Set.add s acc)
             (get_node_stmt n))
        res
        Stmt.Set.empty
    in
    Stmt.Set.elements set

  let get_component kind stmt =
    let kf = Kernel_function.find_englobing_kf stmt in
    let action, check = match kind with
      | Direct -> direct, is_direct
      | Indirect_Backward -> backward, is_indirect_backward
      | Forward _ -> whole, is_forward
    in
    let set =
      M.fold
        (fun (n,_) v acc ->
           if check v then
             Option.fold
               ~none:acc
               ~some:(fun s -> Stmt.Set.add s acc)
               (get_node_stmt n)
           else
             acc)
        (action kf stmt)
        Stmt.Set.empty
    in
    Stmt.Set.elements set

  (*  let iter use_ctrl_dpds f kf stmt =
      let action = if use_ctrl_dpds then whole else direct in
      M.iter (fun elt _ -> f elt) (action kf stmt)
  *)
end

(* ************************************************************************ *)
(* Dynamic registration *)
(* ************************************************************************ *)

let register name arg =
  Dynamic.register
    ~plugin:"Security_slicing"
    name
    (Datatype.func Stmt.ty (Datatype.list Stmt.ty))
    (Component.get_component arg)

let get_direct_component = register "get_direct_component" Component.Direct

let get_indirect_backward_component =
  register "get_indirect_backward_component" Component.Indirect_Backward

let get_forward_component = register "get_forward_component"
    (Component.Forward Component.Security)

let impact_analysis =
  Dynamic.register
    ~plugin:"Security_slicing"
    "impact_analysis"
    (Datatype.func2 Kernel_function.ty Stmt.ty (Datatype.list Stmt.ty))
    (Component.forward Component.Impact)

(* ************************************************************************ *)
(*
(* type t = stmt *)

(** Security component table: a security component is represented by the
    statement at which a security verification should occur.  It is associated
    with the list of its statements. *)
module Components : sig
  (*val add: t -> stmt -> unit
  val find: t -> stmt list
  val self: State.t
  val fold_fold:
    ('b -> t -> 'a -> 'b) -> ('a -> Cil_types.stmt -> 'a) -> 'b -> 'a -> 'b
   *)
end = struct

  module S =
    State_builder.Hashtbl
      (Stmt.Hashtbl)
      (Datatype.Ref(Datatype.List(Stmt)))
      (struct
         let name = "Components"
         let size = 7
         let dependencies = [ Ast.self; Eva.Analysis.self ]
       end)

  let () =
    Cmdline.run_after_extended_stage
      (fun () ->
        State_dependency_graph.add_codependencies ~onto:S.self [ !Db.Pdg.self ])
(*
  let add c =
    let l = S.memo (fun _ -> ref []) c in
    fun s -> l := s :: !l

  let find s = !(S.find s)

  let self = S.self

  let fold_fold f g init_f init_g =
    S.fold (fun c l acc -> f acc c (List.fold_left g init_g !l)) init_f
*)
end

module Nodes =
  State_builder.SetRef
    (struct include NodeKf.Datatype let compare = NodeKf.compare end)
    (struct
       let name = "Components.Nodes"
       let dependencies = [ Security_Annotations.self ]
     end)

let use_ctrl_dependencies = ref false

(** Set tables [Components] and [Stmts]. *)
let compute, self =
  State_builder.apply_once
    "Components.compute"
    [ Security_Annotations.self ]
    (fun () ->
       search_security_requirements ();
       let add_component stmt =
         Security_slicing_parameters.debug
           "computing security component %d" stmt.sid;
         let add_one = Components.add stmt in
         let kf = Kernel_function.find_englobing_kf stmt in
         Component.iter
           !use_ctrl_dependencies
           (fun (n, _ as elt) ->
              Nodes.add elt;
              Option.iter add_one (get_node_stmt n))
           kf
           stmt
       in
       Security_Annotations.iter add_component)

let () =
  Cmdline.run_after_extended_stage
    (fun () ->
       Project.State_builder.add_dependency self !Pdg.self;
       Project.State_builder.add_dependency Nodes.self self;
       Project.State_builder.add_dependency Components.self self)

let get_component =
  Dynamic.register
  "Security.get_component"
  (Datatype.func Kernel_type.stmt (Datatype.list Kernel_type.stmt))
  (fun s -> compute (); Components.find s)

(* ************************************************************************ *)
(** {2 Security slicing} *)
(* ************************************************************************ *)

let slice ctrl =
  use_ctrl_dependencies := ctrl;
  Security_slicing_parameters.feedback ~level:2 "beginning slicing";
  compute ();
  let name = "security slicing" in
  let slicing = !Slicing.Project.mk_project name in
  let select (n, kf) sel =
    Security_slicing_parameters.debug ~level:2 "selecting %a (of %s)"
      (Pdg.Api.pretty_node false) n
      (Kernel_function.get_name kf);
    !Slicing.Select.select_pdg_nodes
      sel
      (!Slicing.Mark.make ~data:true ~addr:true ~ctrl)
      [ n ]
      kf
  in
  let sel = Nodes.fold select Slicing.Select.empty_selects in
  Security_slicing_parameters.debug "adding selection";
  !Slicing.Request.add_persistent_selection slicing sel;
  Security_slicing_parameters.debug "applying slicing request";
  !Slicing.Request.apply_all_internal slicing;
  !Slicing.Slice.remove_uncalled slicing;
  let p = !Slicing.Project.extract name slicing in
(*  Project.copy ~only:(Options.get_selection_after_slicing ()) p;*)
  Security_slicing_parameters.feedback ~level:2 "slicing done";
  p

let slice =
  Dynamic.register
    "Security_slicing.slice"
    (Datatype.func Datatype.bool Project.ty)
    slice
*)
(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct