diff --git a/Changelog b/Changelog index d95a4f95aa16899872a7884c3f1e4a8fe818cc8f..7ebb7055d6056b2810db4aaf30904dd1120aa987 100644 --- a/Changelog +++ b/Changelog @@ -17,6 +17,7 @@ Open Source Release <next-release> ################################## +-* Obfuscator [2019/02/26] Obfuscate logic types and logic constructors. - Eva [2019/01/10] Improved precision on nested loops (by postponing the widening on inner loops according to -eva-widening-period). - Kernel [2019/01/03] Add attributes for loop statements to allow diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli index c550806aaab96422e193ca33ed092fe8e4fca01e..f0eb6d86d0a0ea8d55cd9ac567a80295ffca5f28 100644 --- a/src/kernel_services/ast_data/cil_types.mli +++ b/src/kernel_services/ast_data/cil_types.mli @@ -1487,7 +1487,7 @@ and logic_body = (** Description of a logic type. @plugin development guide *) and logic_type_info = { - lt_name: string; + mutable lt_name: string; lt_params : string list; (** type parameters*) mutable lt_def: logic_type_def option; (** definition of the type. None for abstract types. *) @@ -1528,7 +1528,7 @@ and logic_var = { (** Description of a constructor of a logic sum-type. @plugin development guide *) and logic_ctor_info = - { ctor_name: string; (** name of the constructor. *) + { mutable ctor_name: string; (** name of the constructor. *) ctor_type: logic_type_info; (** type to which the constructor belongs. *) ctor_params: logic_type list (** types of the parameters of the constructor. *) diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml index 213f983d1f4b5e0129ce8d670c81ebc49fdfcd13..1226530bf2284b2a9bbe0c896c49a1a46898673c 100644 --- a/src/plugins/obfuscator/obfuscate.ml +++ b/src/plugins/obfuscator/obfuscate.ml @@ -38,7 +38,8 @@ class visitor = object method! vglob_aux = function | GType (ty,_) -> - ty.tname <- Dictionary.fresh Obfuscator_kind.Type ty.tname; + if not (Cil.typeHasAttribute "fc_stdlib" 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.is_unused_builtin v -> @@ -83,10 +84,15 @@ class visitor = object if Varinfo.Hashtbl.mem varinfos_visited vi then Cil.SkipChildren else begin - if Cil.isFunctionType vi.vtype then begin - if vi.vname <> "main" then - vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname - end else begin + if Cil.isFunctionType vi.vtype then + try + if vi.vname <> "main" + && not (Cil.is_builtin vi) + && not (Cil.is_special_builtin vi.vname) + && not (Cil.hasAttribute "fc_stdlib" vi.vattr) then + vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname + with Not_found -> assert false + 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 @@ -157,11 +163,15 @@ class visitor = object Cil.DoChildren method! vlogic_type_info_decl lti = - warn "logic type" lti.lt_name; + 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 = - warn "logic constructor" lci.ctor_name; + 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 diff --git a/src/plugins/obfuscator/obfuscator_kind.ml b/src/plugins/obfuscator/obfuscator_kind.ml index f4f1fb22e5b396056789b6d543d1b17e1283e04a..47633a9a28a574c381913a693849d2664462df63 100644 --- a/src/plugins/obfuscator/obfuscator_kind.ml +++ b/src/plugins/obfuscator/obfuscator_kind.ml @@ -33,7 +33,9 @@ type k = | Logic_var | Predicate | Type - + | Logic_type + | Logic_constructor + let name_of_kind = function | Behavior -> "behavior" | Enum -> "enum" @@ -47,6 +49,8 @@ let name_of_kind = function | Logic_var -> "logic variable" | Predicate -> "predicate" | Type -> "type" + | Logic_type -> "logic type" + | Logic_constructor -> "logic constructor" let prefix = function | Behavior -> "B" @@ -61,6 +65,8 @@ let prefix = function | Logic_var -> "LV" | Predicate -> "P" | Type -> "T" + | Logic_type -> "LT" + | Logic_constructor -> "LC" include Datatype.Make_with_collections (struct diff --git a/src/plugins/obfuscator/obfuscator_kind.mli b/src/plugins/obfuscator/obfuscator_kind.mli index 0aa33ec52230294a569a723f00e481c5e67c11e5..25685566b8843a4848c14a17bfd4fb2e0e6bc89c 100644 --- a/src/plugins/obfuscator/obfuscator_kind.mli +++ b/src/plugins/obfuscator/obfuscator_kind.mli @@ -33,6 +33,8 @@ type k = | Logic_var | Predicate | Type + | Logic_type + | Logic_constructor include Datatype.S_with_collections with type t = k val prefix: t -> string diff --git a/tests/misc/obfuscate.i b/tests/misc/obfuscate.c similarity index 73% rename from tests/misc/obfuscate.i rename to tests/misc/obfuscate.c index 044b97cb3c955441f9d142dc8c256c8576a97a80..ade70e66898e508959bff64c86b295b21a82c266 100644 --- a/tests/misc/obfuscate.i +++ b/tests/misc/obfuscate.c @@ -46,3 +46,16 @@ int logic(int f1) int main(int* p) { if ("ti\rti" == "ti\rti") f(p); } + +/* Obfuscate logic types and logic constructors. */ +/*@ type t = T | F; */ + +#include "stdint.h" + +/* Do not obfuscate builtins and stdlib types and functions. */ +int builtin_and_stdlib () { + int32_t x = 42; + Frama_C_show_each(x); + /*@ assert \true; */ + return 1; +} diff --git a/tests/misc/oracle/obfuscate.res.oracle b/tests/misc/oracle/obfuscate.res.oracle index 6ba918f0252ea446c324c85ca1b090a33cff40f6..efd7abd9fba1b99bafec1204d5033bd1049a3f2e 100644 --- a/tests/misc/oracle/obfuscate.res.oracle +++ b/tests/misc/oracle/obfuscate.res.oracle @@ -1,4 +1,7 @@ -[kernel] Parsing tests/misc/obfuscate.i (no preprocessing) +[kernel] Parsing tests/misc/obfuscate.c (with preprocessing) +[obfuscator] Warning: unobfuscated attribute name `fc_stdlib' +[obfuscator] Warning: unobfuscated attribute parameter name `stdint.h' +[obfuscator] Warning: unobfuscated attribute name `missingproto' /* *********************************** */ /* start of dictionary for obfuscation */ /* *********************************** */ @@ -12,11 +15,17 @@ #define F1 my_func #define F2 f #define F3 logic +#define F4 builtin_and_stdlib // global variables #define G1 my_var // labels #define L1 end #define L2 end +// logic constructors +#define LC1 T +#define LC2 F +// logic types +#define LT1 t // logic variables #define LV1 I #define LV2 x @@ -29,6 +38,8 @@ #define V2 __retres #define V3 V1 #define V4 __retres +#define V5 x +#define V6 __retres // formal variables #define f1 p #define f2 f1 @@ -47,6 +58,7 @@ /* ********************************************************* */ /* Generated by Frama-C */ +#include "stdint.h" enum T1 { E1 = 0, E2 = 1, @@ -54,7 +66,8 @@ enum T1 { }; int G1 = 0; /*@ global invariant LV1: G1 ≥ 0; - */ + +*/ /*@ requires G1 > 0; ensures G1 > \old(G1); ensures ∀ ℤ LV2; LV2 ≡ LV2; @@ -102,4 +115,19 @@ int main(int *f3) return V4; } +/*@ type LT1 = LC1 | LC2; + +*/ +extern int ( /* missing proto */ Frama_C_show_each)(); + +int F4(void) +{ + int V6; + int32_t V5 = 42; + Frama_C_show_each(V5); + /*@ assert \true; */ ; + V6 = 1; + return V6; +} +