diff --git a/compiler/CCT/fail/doit/x86_64/rol.jazz b/compiler/CCT/fail/doit/x86_64/rol.jazz new file mode 100644 index 000000000..f7abdc754 --- /dev/null +++ b/compiler/CCT/fail/doit/x86_64/rol.jazz @@ -0,0 +1,6 @@ +// This is CT in the ordinary sense, but not DOIT as ROL is not DOIT. +export fn rol(#secret reg u32 x) -> #secret reg u32 { + x < #secret reg u32, #secret reg u32 { + a = a; + b = b; + a, b = #swap(a, b); + return a, b; +} diff --git a/compiler/Makefile b/compiler/Makefile index 064a1cb94..3ffb8f3cd 100644 --- a/compiler/Makefile +++ b/compiler/Makefile @@ -7,7 +7,7 @@ CHECK := $(CHECKPY) scripts/runtest --jobs="$(JSJOBS)" CHECK += config/tests.config CHECKCATS ?= \ safety \ - CCT \ + CCT CCT-DOIT \ x86-64-ATT \ x86-64-Intel \ x86-64-print \ diff --git a/compiler/config/tests.config b/compiler/config/tests.config index d051eca2b..44423ff12 100644 --- a/compiler/config/tests.config +++ b/compiler/config/tests.config @@ -14,6 +14,12 @@ kodirs = !safety/fail bin = ./scripts/check-cct okdirs = !CCT/success kodirs = !CCT/fail +exclude = !CCT/**/doit + +[test-CCT-DOIT] +bin = ./scripts/check-cct +args = --doit +kodirs = !CCT/fail/doit [test-SCT] bin = ./scripts/check-cct diff --git a/compiler/entry/jazzct.ml b/compiler/entry/jazzct.ml index c75bb016a..7ee879406 100644 --- a/compiler/entry/jazzct.ml +++ b/compiler/entry/jazzct.ml @@ -5,7 +5,7 @@ open Utils let parse_and_check arch call_conv = let module A = (val get_arch_module arch call_conv) in - let check infer ct_list speculative pass file = + let check ~doit infer ct_list speculative pass file = let _env, pprog, _ast = try Compile.parse_file A.arch_info file with | Annot.AnnotationError (loc, code) -> @@ -44,7 +44,7 @@ let parse_and_check arch call_conv = in if speculative then - match Sct_checker_forward.ty_prog A.is_ct_sopn prog ct_list with + match Sct_checker_forward.ty_prog (A.is_ct_sopn ~doit) prog ct_list with | exception Annot.AnnotationError (loc, code) -> hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code | sigs -> @@ -53,7 +53,7 @@ let parse_and_check arch call_conv = sigs else let sigs, errs = - Ct_checker_forward.ty_prog A.is_ct_sopn ~infer prog ct_list + Ct_checker_forward.ty_prog (A.is_ct_sopn ~doit) ~infer prog ct_list in Format.printf "/* Security types:\n@[%a@]*/@." (pp_list "@ " (Ct_checker_forward.pp_signature prog)) @@ -63,8 +63,13 @@ let parse_and_check arch call_conv = in Stdlib.Option.iter on_err errs in - fun infer ct_list speculative compile file -> - match check infer ct_list speculative compile file with + fun infer ct_list speculative compile file doit -> + let compile = + if doit && compile < Compiler.PropagateInline then + Compiler.PropagateInline + else compile + in + match check ~doit infer ct_list speculative compile file with | () -> () | exception HiError e -> Format.eprintf "%a@." pp_hierror e; @@ -104,6 +109,10 @@ let file = let doc = "The Jasmin source file to verify" in Arg.(required & pos 0 (some non_dir_file) None & info [] ~docv:"JAZZ" ~doc) +let doit = + let doc = "Allow only DOIT instructions on secrets" in + Arg.(value & flag & info [ "doit" ] ~doc) + let () = let doc = "Check Constant-Time security of Jasmin programs" in let man = @@ -118,5 +127,5 @@ let () = Cmd.v info Term.( const parse_and_check $ arch $ call_conv $ infer $ slice $ speculative - $ compile $ file) + $ compile $ file $ doit) |> Cmd.eval |> exit