chore: add script to test ProVerif example files

The newly (re-)added lines come from this pull request: https://github.com/rosenpass/rosenpass/pull/230

analysis/config.mpv

@@ -88,6 +88,18 @@ set verboseCompleted=VERBOSE.
 #define SES_EV(...)
 #endif
 
+#if COOKIE_EVENTS
+#define COOKIE_EV(...) __VA_ARGS__
+#else
+#define COOKIE_EV(...)
+#endif
+
+#if KEM_EVENTS
+#define KEM_EV(...) __VA_ARGS__
+#else
+#define KEM_EV(...)
+#endif
+
 
 (* TODO: Authentication timing properties *)
 (* TODO: Proof that every adversary submitted package is equivalent to one generated by the proper algorithm using different coins. This probably requires introducing an oracle that extracts the coins used and explicitly adding the notion of coins used for Packet->Packet steps and an inductive RNG notion. *)

marzipan/TODO.md

@@ -34,15 +34,17 @@
 * ~~refactor filtering in run_proverif (see karo's comment)~~
 * ~configurable target directory~
 * ~lark parser: multiline comments, how???~
+* ~parse errors~
+  * ~error when trying with: `nix run .# -- parse ../target/proverif/01_secrecy.entry.i.pv`~
+    * ~`in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));`~
+    * ~                                          ^~
+  * ~04_dos… has a syntax error (see below)~
 
 ## Next Steps
 
 * integrate marzipan.awk into Python, somehow
   * options term special cases (c.f. manual page 133, starting with "fun" term)
     * complete with CryptoVerif options
-  * error when trying with: `nix run .# -- parse ../target/proverif/01_secrecy.entry.i.pv`
-    * `in(C, Cinit_conf(Ssskm, Spsk, Sspkt, ic));`
-    *                                           ^
 * rewrite marzipan.awk into Python/LARK
   * define a LARK grammar for marzipan.awk rules
   * write python code for processing marzipan rules, e.g. alias replacement (step: i.pv->o.pv)

marzipan/src/__init__.py

@@ -14,6 +14,23 @@ console = pkgs.rich.console.Console()
 logger = pkgs.logging.getLogger(__name__)
 
 
+def set_logging_logrecordfactory(filename):
+    old_factory = pkgs.logging.getLogRecordFactory()
+
+    def record_factory(*args, **kwargs):
+        record = old_factory(*args, **kwargs)
+        record.filename = filename
+        return record
+
+    pkgs.logging.setLogRecordFactory(record_factory)
+
+
+#def set_logging_format(max_length):
+#    pass
+#    #format_str = "{levelname:<8} {filename:<" + str(max_length + 2) + "} {message}"
+#    #pkgs.logging.basicConfig(level=pkgs.logging.DEBUG, style="{", format=format_str)
+
+
 @click.group()
 def main():
     pkgs.logging.basicConfig(level=pkgs.logging.DEBUG)
@@ -50,7 +67,7 @@ def clean_line(prev_line, line):
     return prev_line
 
 
-def run_proverif(file, extra_args=[]):
+def run_proverif(file, log_file, extra_args=[]):
     params = ["proverif", "-test", *extra_args, file]
     logger.debug(params)
 
@@ -63,13 +80,15 @@ def run_proverif(file, extra_args=[]):
     )
     try:
         prev_line = None
-        for line in process.stdout:
-            cleaned_line = clean_line(prev_line, line)
-            prev_line = line
-            if cleaned_line is not None:
-                yield cleaned_line
-        if prev_line is not None:
-            yield prev_line
+        with open(log_file, "a") as log:
+            for line in process.stdout:
+                log.write(line)
+                cleaned_line = clean_line(prev_line, line)
+                prev_line = line
+                if cleaned_line is not None:
+                    yield cleaned_line
+            if prev_line is not None:
+                yield prev_line
 
     except Exception as e:
         # When does this happen? Should the error even be ignored? Metaverif should probably just abort here, right? --karo
@@ -83,6 +102,9 @@ def run_proverif(file, extra_args=[]):
             logger.error(
                 f"Proverif exited with a non-zero error code {params}: {return_code}"
             )
+            if prev_line is not None:
+                logger.error(f"Last line of log file {log_file}:")
+                logger.error(f"> {prev_line.rstrip()}")
             exit(return_code)
 
 
@@ -193,7 +215,12 @@ def analyze(repo_path, output):
 
     entries = []
     analysis_dir = pkgs.os.path.join(repo_path, "analysis")
-    entries.extend(sorted(pkgs.glob.glob(str(analysis_dir) + "/*.entry.mpv")))
+    full_paths = sorted(pkgs.glob.glob(str(analysis_dir) + "/*.entry.mpv"))
+    entries.extend(full_paths)
+
+    #modelnames = [pkgs.os.path.basename(path).replace('.entry.mpv', '') for path in full_paths]
+    #max_length = max(len(modelname) for modelname in modelnames) if modelnames else 0
+    #set_logging_format(max_length)
 
     with pkgs.concurrent.futures.ProcessPoolExecutor() as executor:
         futures = {
@@ -231,12 +258,14 @@ def clean(repo_path, output):
 
 
 def metaverif(repo_path, tmpdir, file):
-    print(f"Start metaverif on {file}")
     # Extract the name using regex
-    name_match = pkgs.re.search(r"([^/]*)(?=\.mpv)", file)
+    name_match = pkgs.re.search(r"([^/]*)(?=\.entry\.mpv)", file)
     if name_match:
         name = name_match.group(0)  # Get the matched name
 
+        set_logging_logrecordfactory(name)
+        logger.info(f"Start metaverif on {file}")
+
         # Create the file paths
         cpp_prep = pkgs.os.path.join(tmpdir, f"{name}.i.pv")
         awk_prep = pkgs.os.path.join(tmpdir, f"{name}.o.pv")
@@ -253,9 +282,8 @@ def metaverif(repo_path, tmpdir, file):
 
         ta, res, ctr, expected, descs = pretty_output_init(cpp_prep)
         with open(log_file, "a") as log:
-            generator = run_proverif(awk_prep)
+            generator = run_proverif(awk_prep, log_file)
             for line in generator:
-                log.write(line)
                 # parse-result-line:
                 match = pkgs.re.search(r"^RESULT .* \b(true|false)\b\.$", line)
                 if match:
@@ -274,7 +302,10 @@ def metaverif(repo_path, tmpdir, file):
 @main.command()
 @click.argument("file_path")
 def parse(file_path):
-    parse_main(file_path)
+    try:
+        parse_main(file_path)
+    except pkgs.lark.exceptions.UnexpectedCharacters as e:
+        logger.error(f"Error {type(e).__name__} parsing {file_path}: {e}")
 
 
 if __name__ == "__main__":

marzipan/src/parser.py

@@ -76,7 +76,8 @@ ident_regex = (
 proverif_grammar = Lark(
     grammar="""
     PROCESS: "process"
-    start: decl* PROCESS process
+    EQUIVALENCE: "equivalence"
+    start: decl* PROCESS process | decl* EQUIVALENCE process process
     YIELD: "yield"
     channel: CHANNEL
     CHANNEL: "channel"
@@ -107,11 +108,11 @@ proverif_grammar = Lark(
     OPTIONS_AXIOM: OPTIONS_QUERY_LEMMA_AXIOM
     OPTIONS_QUERY_LEMMA: OPTIONS_QUERY_LEMMA_AXIOM | "induction" | "noInduction"
     OPTIONS_LEMMA: OPTIONS_QUERY_LEMMA_AXIOM | "maxSubset"
-    OPTIONS_QUERY: OPTIONS_QUERY_LEMMA_AXIOM | "proveAll"
+    OPTIONS_QUERY: OPTIONS_QUERY_LEMMA | "proveAll"
     OPTIONS_QUERY_SECRET: "reachability" | "pv_reachability" | "real_or_random" | "pv_real_or_random" | "/cv_[a-zA-Z0-9À-ÿ'_]*/"
     OPTIONS_RESTRICTION: "removeEvents" | "keepEvents" | "keep" # transl_option_lemma_query in pitsyntax.ml
     OPTIONS_EQUATION: "convergent" | "linear" # check_equations in pitsyntax.ml
-    OPTIONS_TYPE: "fixed" | "bounded" # TODO(blipp): complete this. These are only for compatibility with CryptoVerif and are ignored
+    OPTIONS_TYPE: "fixed" | "bounded" | "large" | "nonuniform" | "password" | "size" NAT | "size" NAT "_" NAT | "pcoll" NAT | "small" | "ghost" # from Page 22 in CryptoVerif reference manual
     options{idents}: [ "[" _non_empty_seq{idents} "]" ]
     process: ZERO
            | YIELD
@@ -142,7 +143,7 @@ proverif_grammar = Lark(
                | "let" typedecl "suchthat" pterm options{OPTIONS_PROCESS} [ "in" process [ "else" process ] ]
     if_process: "if" pterm "then" process [ "else" process ]
     in_process: "in" "(" pterm "," pattern ")" options{OPTIONS_PROCESS} [ ";" process ]
-    get_process: IDENT "(" _maybe_empty_seq{pattern} ")" [ "suchthat" pterm ] options{OPTIONS_PROCESS} [ "in" process [ "else" process ] ]
+    get_process: "get" IDENT "(" _maybe_empty_seq{pattern} ")" [ "suchthat" pterm ] options{OPTIONS_PROCESS} [ "in" process [ "else" process ] ]
     out_process: "out" "(" pterm "," pterm ")" [ ";" process ]
     insert_process: "insert" IDENT "(" _maybe_empty_seq{pterm} ")" [ ";" process ]
     event_process: "event" IDENT [ "(" _maybe_empty_seq{pterm} ")" ] [ ";" process ]
@@ -232,7 +233,7 @@ proverif_grammar = Lark(
                 | IDENT "<-R" typeid [";" pterm]
     insert_pterm: "insert" IDENT "(" _maybe_empty_seq{pterm} ")" ";" pterm
     event_pterm: "event" IDENT [ "(" _maybe_empty_seq{pterm} ")" ] ";" pterm
-    get_pterm: IDENT "(" _maybe_empty_seq{pattern} ")" [ "suchthat" pterm ] options{OPTIONS_PROCESS} [ "in" pterm [ "else" pterm ] ]
+    get_pterm: "get" IDENT "(" _maybe_empty_seq{pattern} ")" [ "suchthat" pterm ] options{OPTIONS_PROCESS} [ "in" pterm [ "else" pterm ] ]
     pattern: IDENT [":" typeid]
            | "_" [ ":" typeid ]
            | NAT
@@ -291,7 +292,7 @@ proverif_grammar = Lark(
     fun_reduc_decl: "fun" IDENT "(" _maybe_empty_seq{typeid} ")" ":" typeid "reduc" mayfailreduc options{OPTIONS_FUN_CONST} "."
     equation_decl: "equation" eqlist options{OPTIONS_EQUATION} "."
     pred_decl: "pred" IDENT [ "(" [ _maybe_empty_seq{typeid} ] ")" ] options{OPTIONS_PRED} "."
-    table_decl: IDENT "(" _maybe_empty_seq{typeid} ")" "."
+    table_decl: "table" IDENT "(" _maybe_empty_seq{typeid} ")" "."
     let_decl: "let" IDENT [ "(" [ typedecl ] ")" ] "=" process "."
 
     BOOL : "true" | "false"
@@ -351,7 +352,7 @@ proverif_grammar = Lark(
     simplify_process_values: BOOL | "interactive"
     precise_actions_values: BOOL | "trueWithoutArgsInNames"
     redundant_hyp_elim_values: BOOL | "beginOnly"
-    reconstruct_trace_values: BOOL | "n"
+    reconstruct_trace_values: BOOL | NAT | "yes" | "no" # TODO(blipp): check whether yes/no is always allowed for BOOL
     attacker_values: "active" | "passive"
     key_compromise_values: "none" | "approx" | "strict"
     predicates_implementable: "check" | "nocheck"
@@ -397,7 +398,7 @@ proverif_grammar = Lark(
     restriction_decl: "restriction" [ typedecl ";"] lemma options{OPTIONS_RESTRICTION} "."
     lemma_decl:       "lemma"       [ typedecl ";"] lemma options{OPTIONS_LEMMA} "."
 
-    noninterf_decl: [ typedecl ";"] _maybe_empty_seq{nidecl} "."
+    noninterf_decl: "noninterf" [ typedecl ";"] _maybe_empty_seq{nidecl} "."
     weaksecret_decl: "weaksecret" IDENT "."
     not_decl: "not" [ typedecl ";"] gterm "."
 

marzipan/test_parser.sh

@@ -0,0 +1,23 @@
+#!/usr/bin/env bash
+shopt -s nullglob globstar
+
+proverif_repo=$1
+
+# Prerequisites:
+# * built ProVerif
+# * ran ./test (and aborted it) such that the preparation scripts have been run
+
+# Test pitype files
+for f in $proverif_repo/examples/pitype/**/*.pv; do
+  [[ $f == *.m4.pv ]] && continue
+  echo "$f"
+  nix run .# -- parse "$f"
+done
+
+
+# Test cryptoverif files
+for f in $proverif_repo/examples/cryptoverif/**/*.pcv; do
+  [[ $f == *.m4.pcv ]] && continue
+  echo "$f"
+  nix run .# -- parse "$f"
+done