The in-file heuristic ignores the --oraclename command-line option

[yavivanov]

The global file heuristic introduced in PR #303 (and included in PR #304) ignores the --oraclename command-line option.
If a theory specifies the global file heuristic as o or O, Tamarin ignores the oracle specified in --oraclename. Instead, it tries to use the default oraclename ("./oracle").

Steps to invoke this behavior:

1. In a given file, define the global file heuristic as either heuristic:o or heuristic:O.
2. Run Tamarin for the given file with the command-line options --prove --oraclename=oracle_for_the_theory.oracle (some oracle with a filename different than oracle). Do not specify another heuristic in the command line, as this would overwrite the in-file heuristic.
3. Tamarin outputs an error "./oracle: readCreateProcess: posix_spawnp: does not exist (No such file or directory)".
   "./oracle" is the default oraclename used by Tamarin when no oraclename was specified.
   Yet, Tamarin tried to use it, although --oraclename was specified in the command line.

Note:
Heuristics in lemma attributes exhibit the same behavior (issue #372). As per PR #406, this is considered correct behaviour for them.

Edit: rewrote/added the note

[kevinmorio]

This is the expected behavior. Using the --oraclename flag without the --heuristic flag has no effect, because it doesn't specify a complete goal ranking. In the case where you have a heuristic: (o|O) in the model, --oraclename could override the default heuristic file. But what would be the expected behavior if there is no heuristic: (o|O) in the model? Then whether the --oraclename flag is used or ignored would depend on whether the model includes heuristic: (o|O).

In my opinion such a behavior would not be very intuitive and I don't see the need for it. In your case, you can specify the oracle file directly in the model like heuristic: o "./oracle_for_the_theory.oracle". I think it is clearer if each goal ranking is independent of the others.

To avoid misconceptions in the future, I'm in favor of integrating the --oraclename option directly into the --heuristic option such that there is no possibility of specifying incomplete goal rankings and having a unified syntax for them. That is you could then use --heuristic=o "./some-oracle".

Specifying heuristic: (o|O) in the model is the same as heuristic: (o|O) "./oracle". That is, an oracle goal ranking defaults to the oracle file ./oracle. That is the reason for the file-not-found error.

[rkunnema]

There is a security consideration that we should at least discuss: an untrusted spthy file could unexpectedly call a script that damages the system. This also came up in the discussion for #220.

My proposal would be to guarantee that file bla.spthy only ever calls script bla.oracle, unless is invoked on the command line and changes this default with --oraclename. If a number of scripts want to use the same oracle, they can still use symbolic links to achieve this behavior.

[kevinmorio]

Unintentional or even malicious code execution through oracles is definitively a thing we should avoid.

However, allowing bla.spthy to only call bla.spthy would severely limit the usefulness of the feature and be diametrical to the original intentions I had with it: Using different oracles for different lemmas. For example:

theory Bla

heuristic: o "./bla-default

lemma A[heuristic=o "./bla-A"]
  ...

lemma A[heuristic=o "./bla-A"]
  ...

end

Instead, I propose asking the user if they trust all the oracles that are specified in the theory like

Do you trust "./bla-default"? [y/N]
Do you trust "./bla-A"? [y/N]
Do you trust "./bla-B"? [y/N]

To suppress these questions and trust all oraacles, we can add a flag --trust-oracles or even --trust-oracles "./bla-default" "./bla-A" "./bla-B".

[rkunnema]

Hi!

On 2. Sep 2022, at 10:52, Kevin Morio ***@***.***> wrote: Unintentional or even malicious code execution through oracles is definitively a thing we should avoid. However, allowing bla.spthy to only call bla.spthy would severely limit the usefulness of the feature and be diametrical to the original intentions I had with it: Using different oracles for different lemmas.

I think that's supported, at least I saw it in some oracles, e.g., `examples/csf19-wrapping/gcm.spthy.oracle`. ARGV[1] gives the current lemma name, which the default oracle can use. (Note: this does not seem to be documented in https://tamarin-prover.github.io/manual/book/011_advanced-features.html)

Instead, I propose asking the user if they trust all the oracles that are specified in the theory like Do you trust "./bla-default"? [y/N] Do you trust "./bla-A"? [y/N] Do you trust "./bla-B"? [y/N] To suppress these questions and trust all oraacles, we can add a flag --trust-oracles or even --trust-oracles "./bla-default" "./bla-A" "./bla-B".

That seems like a lot of work for the user and some engineering, too (how to do interactive prompts in GUI mode? Can we always to this if we are not in the IOMonad?). Cheers, Robert