package frama-c

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

Source file obfuscate.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
(**************************************************************************)
(*                                                                        *)
(*  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

let warn kind name =
  Options.warning ~once:true "unobfuscated %s name `%s'" kind name

let has_literal_string = ref false

class visitor = object

  inherit Visitor.frama_c_inplace

  val varinfos_visited = Varinfo.Hashtbl.create 17
  val logic_vars_visited = Logic_var.Hashtbl.create 7
  val id_pred_visited = Identified_predicate.Hashtbl.create 7

  method! vtype = function
    | TFun(t, args, variadic, attrs) ->
      let args' =
        match args with
        | None -> None
        | Some l ->
          Some
            (List.map
               (fun (s,t,a) ->
                  (Dictionary.fresh Obfuscator_kind.Formal_in_type s, t, a)) l)
      in
      Cil.ChangeDoChildrenPost(TFun(t,args',variadic,attrs), Fun.id)
    | _ -> Cil.DoChildren

  method! vglob_aux = function
    | GType (ty,_) ->
      if not (Cil.is_in_libc (Cil.typeAttrs ty.ttype)) then
        ty.tname <- Dictionary.fresh Obfuscator_kind.Type ty.tname;
      Cil.DoChildren
    | GVarDecl (v, _) | GVar (v, _, _)
    | GFun ({svar = v}, _) | GFunDecl (_, v, _)
      when Cil_builtins.is_unused_builtin v ->
      Cil.SkipChildren
    | _ ->
      Cil.DoChildren

  method! vcompinfo ci =
    ci.cname <- Dictionary.fresh Obfuscator_kind.Type ci.cname;
    Cil.DoChildren

  method! venuminfo ei =
    ei.ename <- Dictionary.fresh Obfuscator_kind.Type ei.ename;
    Cil.DoChildren

  method! vfieldinfo fi =
    fi.fname <- Dictionary.fresh Obfuscator_kind.Field fi.fname;
    Cil.DoChildren

  method! venumitem ei =
    ei.einame <- Dictionary.fresh Obfuscator_kind.Enum ei.einame;
    Cil.DoChildren

  method! vexpr e = match e.enode with
    | Const(CStr str) ->
      has_literal_string := true;
      (* ignore the result: will be handle by hacking the pretty printer *)
      (try
         ignore (Dictionary.id_of_literal_string str)
       with Not_found ->
         ignore (Dictionary.fresh Obfuscator_kind.Literal_string str));
      Cil.SkipChildren
    | _ ->
      Cil.DoChildren

  method! vvdec vi =
    (* Varinfo can be visited (and obfuscated) more than once:
       functions for their declaration and definition, variables
       as parts of the type of the function, and in the body of
       the function declaration, etc. Thus we make sure that the
       obfuscator does not visit them twice *)
    if Varinfo.Hashtbl.mem varinfos_visited vi then
      Cil.SkipChildren
    else begin
      if Cil.isFunctionType vi.vtype then begin
        if vi.vname <> "main"
        && not (Cil_builtins.is_builtin vi)
        && not (Cil.is_in_libc vi.vattr) then
          vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname
      end
      else begin
        let add =
          if vi.vglob then Dictionary.fresh Obfuscator_kind.Global_var
          else if vi.vformal then Dictionary.fresh Obfuscator_kind.Formal_var
          else Dictionary.fresh Obfuscator_kind.Local_var
        in
        vi.vname <- add vi.vname;
      end;
      Varinfo.Hashtbl.add varinfos_visited vi ();
      Cil.DoChildren
    end

  method! vlogic_var_decl lvi =
    match lvi.lv_kind with
    | LVGlobal | LVFormal | LVQuant | LVLocal ->
      if Logic_var.Hashtbl.mem logic_vars_visited lvi then
        Cil.SkipChildren
      else begin
        lvi.lv_name <- Dictionary.fresh Obfuscator_kind.Logic_var lvi.lv_name;
        Logic_var.Hashtbl.add logic_vars_visited lvi ();
        Cil.DoChildren
      end
    | LVC ->
      Cil.SkipChildren

  method! vstmt_aux stmt =
    let labels =
      List.map
        (function
          | Label(s, loc, true) ->
            (* only obfuscate user's labels, not Cil's ones *)
            let s' = Dictionary.fresh Obfuscator_kind.Label s in
            Label(s', loc, true)
          | Label(_, _, false) | Case _ | Default _ as label -> label)
        stmt.labels
    in
    stmt.labels <- labels;
    Cil.DoChildren

  method! videntified_predicate p =
    if Identified_predicate.Hashtbl.mem id_pred_visited p then
      Cil.SkipChildren
    else begin
      Identified_predicate.Hashtbl.add id_pred_visited p ();
      let { tp_kind; tp_statement = pred } = p.ip_content in
      let names = pred.pred_name in
      let names' =
        List.map (Dictionary.fresh Obfuscator_kind.Predicate) names
      in
      let pred' = { pred with pred_name = names' } in
      let ip_content = Logic_const.toplevel_predicate ~kind:tp_kind pred' in
      let p' = { p with ip_content } in
      Cil.ChangeDoChildrenPost (p', Fun.id)
    end

  method! vterm t =
    List.iter (fun s -> warn "term" s) t.term_name;
    Cil.DoChildren

  method! vannotation = function
    | Daxiomatic(str, globs, attrs, loc) ->
      let str' = Dictionary.fresh Obfuscator_kind.Axiomatic str in
      Cil.ChangeDoChildrenPost(Daxiomatic(str',globs,attrs,loc),Fun.id)
    | Dlemma(str, labs, typs, pred, attrs, loc) ->
      let str' = Dictionary.fresh Obfuscator_kind.Lemma str in
      Cil.ChangeDoChildrenPost(
        Dlemma(str',labs,typs, pred, attrs, loc),Fun.id)
    | _ ->
      Cil.DoChildren

  method! vmodel_info mi =
    warn "model" mi.mi_name;
    Cil.DoChildren

  method! vlogic_type_info_decl lti =
    if not (Logic_env.is_builtin_logic_type lti.lt_name)
    then lti.lt_name <- Dictionary.fresh Obfuscator_kind.Logic_type lti.lt_name ;
    Cil.DoChildren

  method! vlogic_ctor_info_decl lci =
    if not (Logic_env.is_builtin_logic_ctor lci.ctor_name)
    then
      lci.ctor_name <-
        Dictionary.fresh Obfuscator_kind.Logic_constructor lci.ctor_name ;
    Cil.DoChildren

  method! vattr = function
    | Attr(str, _) | AttrAnnot str ->
      warn "attribute" str;
      Cil.DoChildren

  method! vattrparam p =
    (match p with
     | AStr str | ACons(str, _) | ADot(_, str) -> warn "attribute parameter" str
     | _ -> ());
    Cil.DoChildren

  initializer has_literal_string := false

end

let obfuscate_behaviors () =
  (* inheriting method vbehavior or vspec does not work since only a copy of the
     piece of spec is provided. *)
  Globals.Functions.iter
    (fun kf ->
       let h = Datatype.String.Hashtbl.create 7 in
       Annotations.iter_behaviors_by_emitter
         (fun emitter b ->
            if Emitter.equal emitter Emitter.end_user
            && not (Cil.is_default_behavior b)
            then begin
              Annotations.remove_behavior ~force:true emitter kf b;
              let new_ = Dictionary.fresh Obfuscator_kind.Behavior b.b_name in
              Datatype.String.Hashtbl.add h b.b_name new_;
              b.b_name <- new_;
              Annotations.add_behaviors emitter kf [ b ];
            end)
         kf;
       let handle_bnames iter remove add =
         iter
           (fun emitter l ->
              remove emitter kf l;
              add emitter kf (List.map (Datatype.String.Hashtbl.find h) l))
           kf
       in
       handle_bnames
         Annotations.iter_complete
         (fun e kf l -> Annotations.remove_complete e kf l)
         (fun e kf l -> Annotations.add_complete e kf l);
       handle_bnames
         Annotations.iter_disjoint
         (fun e kf l -> Annotations.remove_disjoint e kf l)
         (fun e kf l -> Annotations.add_disjoint e kf l))

module UpdatePrinter (X: Printer.PrinterClass) = struct
  (* obfuscated printer *)
  class printer = object
    inherit X.printer as super
    method! constant fmt = function
      | CStr str -> Format.fprintf fmt "%s" (Dictionary.id_of_literal_string str)
      | c -> super#constant fmt c

    method! file fmt ast =
      if !has_literal_string then begin
        let string_fmt =
          if Options.Literal_string.is_default () then fmt
          else begin
            let file = Options.Literal_string.get () in
            try
              let cout = open_out file in
              Format.formatter_of_out_channel cout
            with Sys_error _ as exn ->
              Options.error "@[cannot generate the literal string dictionary \
                             into file `%s':@ %s@]"
                file
                (Printexc.to_string exn);
              fmt
          end
        in
        Format.fprintf string_fmt "\
/* *********************************************************** */@\n\
/* start of dictionary required to compile the obfuscated code */@\n\
/* *********************************************************** */@\n";
        Dictionary.pretty_kind string_fmt Obfuscator_kind.Literal_string;
        Format.fprintf string_fmt "\
/* ********************************************************* */@\n\
/* end of dictionary required to compile the obfuscated code */@\n\
/* ********************************************************* */@\n@\n";
        if fmt != string_fmt then begin
          Format.pp_print_flush string_fmt ();
          Format.fprintf fmt "\
/* include the dictionary of literal strings */@\n\
@[#include \"%s\"@]@\n@\n"
            (Options.Literal_string.get ())
        end
      end;
      super#file fmt ast

  end
end

let obfuscate () =
  Dictionary.mark_as_computed ();
  obfuscate_behaviors ();
  Visitor.visitFramacFile
    (new visitor :> Visitor.frama_c_visitor)
    (Ast.get ());
  Printer.update_printer (module UpdatePrinter: Printer.PrinterExtension)

(*
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