RFC: Add option to prevent arbitrary code execution in `TermElabM`

Proposal

The current interface for elaboration and tactic execution permits running arbitrary code inside proofs via the run_tac construction and the unsafe elaborator. For this reason, even just type checking the correctness of some Lean code requires some trust of the author of the code. This opens the door to possible reward hacking by machine learning models and malicious attacks for a Lean proof and verification service.

I propose that an addition flag prohibitUnsafe : Bool := false be added to Elab.Term.Context to prevent this behaviour. In conjunction of this flag, we add a function

def throwErrorIfUnsafe : TermElabM Unit := do
  if (← readThe Context).prohibitUnsafe then
    throwError "Cannot elaborate unsafe"

This function would then be called in any elaborator which can execute arbitrary, unfiltered code such as evalTerm or run_tac. When prohibitUnsafe := true, any unfiltered formal statement or proof would not be able to run arbitrary code.

Moreover, we add a core option elab.prohibitUnsafe (passed to TermElabM via mkTermContext) so the prohibition flag could be enabled in a scope by writing

set_option elab.prohibitUnsafe true

If a tactic has legitimate usage of evalTerm (e.g. one that only evaluates natural number terms), it can temporarily override this flag. This transfers the trust from the author of the proof (which could be a machine learning model or a human operator) to the author of the tactics. The flag is not turned on by default, and existing code will continue to run. However any tactic using evalTerm or the unsafe elaborator would not be able to run under prohibitUnsafe := true unless there is an explicit override. We can then vet existing tactics to see their behaviours warrant a override.

This feature benefits machine learning researchers whose models generate large amounts of unvetted code. It is relatively easy to maintain since the flag is turned off by default. The flag would be turned on when processing untrusted inputs.

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

https://leanprover.zulipchat.com/#narrow/channel/341532-lean4-dev/topic/Unsafe.20prohibition.20flag.20in.20.60Elab.2ETerm.2EContext.60/with/526697664

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Read Elab.Term.Context and mkTermContext first, then trace the evalTerm, run_tac, and unsafe elaborator entry points mentioned in the proposal. Done means the requested prohibition can be enabled through elab.prohibitUnsafe, blocks the relevant execution paths when enabled, and preserves existing behavior by default.