Make standalone the security (CT) checker

.gitlab-ci.yml

@@ -81,6 +81,7 @@ ocaml:
     - compiler/_build/
     - compiler/jasminc
     - compiler/jazz2tex
+    - compiler/jazzcheck
 
 eclib:
   stage: prove
@@ -143,7 +144,7 @@ opam-compiler:
     nix-shell --arg inCI true $EXTRA_NIX_ARGUMENTS --run
     'eval $(opam env) &&
      make -C compiler -j$NIX_BUILD_CORES &&
-     (cd compiler && mkdir -p bin && cp _build/default/entry/jasminc.exe bin/jasminc && cp _build/default/entry/jazz2tex.exe bin/jazz2tex && mkdir -p lib/jasmin/easycrypt && cp ../eclib/*.ec lib/jasmin/easycrypt/)'
+     (cd compiler && mkdir -p bin && cp _build/default/entry/jasminc.exe bin/jasminc && cp _build/default/entry/jazz2tex.exe bin/jazz2tex && cp _build/default/entry/jazzcheck.exe bin/jazzcheck && mkdir -p lib/jasmin/easycrypt && cp ../eclib/*.ec lib/jasmin/easycrypt/)'
   artifacts:
     paths:
     - compiler/bin/

CHANGELOG.md

@@ -78,6 +78,11 @@
 - Extraction as EasyCrypt code targets version 2024.01
   ([PR #690](https://github.com/jasmin-lang/jasmin/pull/690)).
 
+- The Constant-Time security checker is now available as a separate `jazzcheck`
+  tool; the `-checkCT`, `-checkCTon`, and `-infer` command line options are
+  deprecated
+  ([PR #766](https://github.com/jasmin-lang/jasmin/pull/766)).
+
 ## Bug fixes
 
 - Type-checking rejects invalid variants of primitive operators

compiler/.gitignore

@@ -8,3 +8,4 @@ report.log
 /jasmin.mlpack
 /jasminc
 /jazz2tex
+/jazzcheck

compiler/Makefile

@@ -41,10 +41,11 @@ all: build
 build: native
 
 define do-build
-	$(RM) jasminc jazz2tex
-	dune build @check entry/jasminc.$(1) entry/jazz2tex.$(1)
+	$(RM) jasminc jazz2tex jazzcheck
+	dune build @check entry/jasminc.$(1) entry/jazz2tex.$(1) entry/jazzcheck.$(1)
 	ln -sf "_build/default/entry/jasminc.$(1)" jasminc
 	ln -sf "_build/default/entry/jazz2tex.$(1)" jazz2tex
+	ln -sf "_build/default/entry/jazzcheck.$(1)" jazzcheck
 endef
 
 byte:
@@ -67,16 +68,18 @@ check-ci:
 
 clean:
 	dune clean
-	$(RM) jasminc jazz2tex
+	$(RM) jasminc jazz2tex jazzcheck
 
 install:
 	$(INSTALL) -m 0755 -d $(DESTDIR)$(BINDIR)
 	$(INSTALL) -m 0755 -T jasminc $(DESTDIR)$(BINDIR)/jasminc
 	$(INSTALL) -m 0755 -T jazz2tex $(DESTDIR)$(BINDIR)/jazz2tex
+	$(INSTALL) -m 0755 -T jazzcheck $(DESTDIR)$(BINDIR)/jazzcheck
 
 uninstall:
 	$(RM) $(DESTDIR)$(BINDIR)/jasminc
 	$(RM) $(DESTDIR)$(BINDIR)/jazz2tex
+	$(RM) $(DESTDIR)$(BINDIR)/jazzcheck
 
 # --------------------------------------------------------------------
 dist: $(DISTDIR).tgz

compiler/default.nix

@@ -9,7 +9,7 @@ stdenv.mkDerivation {
 
   installPhase = ''
     mkdir -p $out/bin
-    for p in jasminc jazz2tex
+    for p in jasminc jazz2tex jazzcheck
     do
       cp _build/default/entry/$p.exe $out/bin/$p
     done

compiler/dune

@@ -1,4 +1,12 @@
 (subdir entry
+
+(library
+  (name commonCLI)
+  (wrapped false)
+  (libraries cmdliner jasmin.jasmin)
+  (flags (:standard -rectypes))
+  (modules commonCLI))
+
 (executable
  (public_name jasminc)
  (name jasminc)
@@ -13,5 +21,13 @@
  (modules jazz2tex)
  (flags (:standard -rectypes))
  (modes byte exe)
- (libraries cmdliner jasmin))
+ (libraries commonCLI))
+
+(executable
+ (public_name jazzcheck)
+ (name jazzcheck)
+ (modules jazzcheck)
+ (flags (:standard -rectypes))
+ (modes byte exe)
+ (libraries commonCLI))
 )

compiler/entry/commonCLI.ml

@@ -0,0 +1,34 @@
+open Jasmin
+open Cmdliner
+
+type arch = Amd64 | CortexM
+
+let get_arch_module arch call_conv : (module Arch_full.Arch) =
+  (module Arch_full.Arch_from_Core_arch
+            ((val match arch with
+                  | Amd64 ->
+                      (module (val CoreArchFactory.core_arch_x86 ~use_lea:false
+                                     ~use_set0:false call_conv)
+                      : Arch_full.Core_arch)
+                  | CortexM ->
+                      (module CoreArchFactory.Core_arch_ARM
+                      : Arch_full.Core_arch))))
+
+let arch =
+  let alts = [ ("x86-64", Amd64); ("arm-m4", CortexM) ] in
+  let doc =
+    Format.asprintf "The target architecture (%s)" (Arg.doc_alts_enum alts)
+  in
+  let arch = Arg.enum alts in
+  Arg.(value & opt arch Amd64 & info [ "arch" ] ~doc)
+
+let call_conv =
+  let alts =
+    [ ("linux", Glob_options.Linux); ("windows", Glob_options.Windows) ]
+  in
+  let doc = Format.asprintf "Undocumented (%s)" (Arg.doc_alts_enum alts) in
+  let call_conv = Arg.enum alts in
+  Arg.(
+    value
+    & opt call_conv Glob_options.Linux
+    & info [ "call-conv"; "cc" ] ~docv:"OS" ~doc)

compiler/entry/commonCLI.mli

@@ -0,0 +1,8 @@
+open Jasmin
+open Cmdliner
+
+type arch
+
+val get_arch_module : arch -> Glob_options.call_conv -> (module Arch_full.Arch)
+val arch : arch Term.t
+val call_conv : Glob_options.call_conv Term.t

compiler/entry/jazz2tex.ml

@@ -1,30 +1,20 @@
-module J = Jasmin
-
-type arch = Amd64 | CortexM
+open Jasmin
+open Cmdliner
+open CommonCLI
 
 let parse_and_print arch call_conv =
-  let module A =
-    J.Arch_full.Arch_from_Core_arch
-      ((val match arch with
-            | Amd64 ->
-                (module (val J.CoreArchFactory.core_arch_x86 ~use_lea:false
-                               ~use_set0:false call_conv)
-                : J.Arch_full.Core_arch)
-            | CortexM ->
-                (module J.CoreArchFactory.Core_arch_ARM : J.Arch_full.Core_arch))) in
+  let module A = (val get_arch_module arch call_conv) in
   fun output file ->
-    let _, _, ast = J.Compile.parse_file A.arch_info file in
+    let _, _, ast = Compile.parse_file A.arch_info file in
     let out, close =
       match output with
       | None -> (stdout, ignore)
       | Some latexfile -> (open_out latexfile, close_out)
     in
     let fmt = Format.formatter_of_out_channel out in
-    Format.fprintf fmt "%a@." J.Latex_printer.pp_prog ast;
+    Format.fprintf fmt "%a@." Latex_printer.pp_prog ast;
     close out
 
-open Cmdliner
-
 let file =
   let doc = "The Jasmin source file to pretty-print" in
   Arg.(required & pos 0 (some non_dir_file) None & info [] ~docv:"JAZZ" ~doc)
@@ -35,25 +25,6 @@ let output =
   in
   Arg.(value & opt (some string) None & info [ "o"; "output" ] ~docv:"TEX" ~doc)
 
-let arch =
-  let alts = [ ("x86-64", Amd64); ("arm-m4", CortexM) ] in
-  let doc =
-    Format.asprintf "The target architecture (%s)" (Arg.doc_alts_enum alts)
-  in
-  let arch = Arg.enum alts in
-  Arg.(value & opt arch Amd64 & info [ "arch" ] ~doc)
-
-let call_conv =
-  let alts =
-    [ ("linux", J.Glob_options.Linux); ("windows", J.Glob_options.Windows) ]
-  in
-  let doc = Format.asprintf "Undocumented (%s)" (Arg.doc_alts_enum alts) in
-  let call_conv = Arg.enum alts in
-  Arg.(
-    value
-    & opt call_conv J.Glob_options.Linux
-    & info [ "call-conv"; "cc" ] ~docv:"OS" ~doc)
-
 let () =
   let doc = "Pretty-print Jasmin source programs into LATEX" in
   let man =
@@ -65,7 +36,7 @@ let () =
     ]
   in
   let info =
-    Cmd.info "jazz2tex" ~version:J.Glob_options.version_string ~doc ~man
+    Cmd.info "jazz2tex" ~version:Glob_options.version_string ~doc ~man
   in
   Cmd.v info Term.(const parse_and_print $ arch $ call_conv $ output $ file)
   |> Cmd.eval |> exit

compiler/entry/jazzcheck.ml

@@ -0,0 +1,75 @@
+open Jasmin
+open Cmdliner
+open CommonCLI
+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 file =
+    let _env, pprog, _ast =
+      try Compile.parse_file A.arch_info file with
+      | Annot.AnnotationError (loc, code) ->
+          hierror ~loc:(Lone loc) ~kind:"annotation error" "%t" code
+      | Pretyping.TyError (loc, code) ->
+          hierror ~loc:(Lone loc) ~kind:"typing error" "%a" Pretyping.pp_tyerror
+            code
+      | Syntax.ParseError (loc, msg) ->
+          hierror ~loc:(Lone loc) ~kind:"parse error" "%s"
+            (Option.default "" msg)
+    in
+    let prog =
+      try Compile.preprocess A.reg_size A.asmOp pprog
+      with Typing.TyError (loc, code) ->
+        hierror ~loc:(Lmore loc) ~kind:"typing error" "%s" code
+    in
+
+    let sigs, errs =
+      Ct_checker_forward.ty_prog A.is_ct_sopn ~infer prog ct_list
+    in
+    Format.printf "/* Security types:\n@[<v>%a@]*/@."
+      (pp_list "@ " (Ct_checker_forward.pp_signature prog))
+      sigs;
+    let on_err (loc, msg) =
+      hierror ~loc:(Lone loc) ~kind:"constant type checker" "%t" msg
+    in
+    Stdlib.Option.iter on_err errs
+  in
+  fun infer ct_list file ->
+    match check infer ct_list file with
+    | () -> ()
+    | exception HiError e ->
+        Format.eprintf "%a@." pp_hierror e;
+        exit 1
+
+let infer =
+  let doc = "Infer security contracts" in
+  Arg.(value & flag & info [ "infer" ] ~doc)
+
+let slice =
+  let doc =
+    "Only check the given function (and its dependencies). This argument may \
+     be repeated to check many functions. If not given, all functions will be \
+     checked."
+  in
+  Arg.(value & opt_all string [] & info [ "slice"; "only"; "on" ] ~doc)
+
+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 () =
+  let doc = "Check Constant-Time security of Jasmin programs" in
+  let man =
+    [
+      `S Manpage.s_environment;
+      Manpage.s_environment_intro;
+      `I ("OCAMLRUNPARAM", "This is an OCaml program");
+      `I ("JASMINPATH", "To resolve $(i,require) directives");
+    ]
+  in
+  let info =
+    Cmd.info "jazzcheck" ~version:Glob_options.version_string ~doc ~man
+  in
+  Cmd.v info
+    Term.(const parse_and_check $ arch $ call_conv $ infer $ slice $ file)
+  |> Cmd.eval |> exit

compiler/jasmin.opam

@@ -15,6 +15,7 @@ install: [
   mkdir -p "%{prefix}%/bin"
   cp "_build/default/entry/jasminc.exe" "%{prefix}%/bin/jasminc"
   cp "_build/default/entry/jazz2tex.exe" "%{prefix}%/bin/jazz2tex"
+  cp "_build/default/entry/jazzcheck.exe" "%{prefix}%/bin/jazzcheck"
   mkdir -p "%{prefix}%/lib/jasmin/easycrypt"
   sh -c "cp ../eclib/*.ec \"%{prefix}%/lib/jasmin/easycrypt/\""
 ]

compiler/scripts/check-cct

@@ -2,4 +2,4 @@
 
 set -ex
 
-exec $(dirname $0)/../jasminc -checkCT "$@"
+exec $(dirname $0)/../jazzcheck "$@"

compiler/src/CLI_errors.ml

@@ -57,4 +57,9 @@ let check_options () =
   if !latexfile <> ""
   then warning Deprecated Location.i_dummy
          "the [-latex] option has been deprecated since March 2023; use [jazz2tex] instead";
+
+  if Option.is_some !ct_list || !infer
+  then warning Deprecated Location.i_dummy
+         "the command-line options for constant-time have been deprecated since April 2024; use [jazzcheck] instead";
+
   List.iter chk_out_file [ outfile; latexfile; ecfile ]

compiler/src/glob_options.ml

@@ -211,9 +211,9 @@ let options = [
     "-oec"     ,  Arg.Set_string ecfile , "[filename]: use filename as output destination for easycrypt extraction";
     "-oecarray" , Arg.String set_ec_array_path, "[dir]: output easycrypt array theories to the given path";
     "-CT" , Arg.Unit set_constTime      , ": generates model for constant time verification";
-    "-checkCT", Arg.Unit set_ct         , ": checks that the full program is constant time (using a type system)";
-    "-checkCTon", Arg.String set_ct_on  , "[f]: checks that the function [f] is constant time (using a type system)";
-    "-infer"    , Arg.Set infer         , "infers security level annotations of the constant time type system";          
+    "-checkCT", Arg.Unit set_ct         , ": checks that the full program is constant time (using a type system) (deprecated)";
+    "-checkCTon", Arg.String set_ct_on  , "[f]: checks that the function [f] is constant time (using a type system) (deprecated)";
+    "-infer"    , Arg.Set infer         , "infers security level annotations of the constant time type system (deprecated)";
     "-checkSCT", Arg.Unit set_sct       , ": checks that the full program is speculative constant time (using a type system)";
     "-checkSCTon", Arg.String set_sct_on, "[f]: checks that the function [f] is speculative constant time (using a type system)";
     "-checkSCTafter", Arg.Symbol(compiler_step_symbol, set_sct_comp_pass), "start sct checker after given pass";