Exploits in Lean

Stream: new members

[Stepan Nesterov]

A few examples of Lean exploits, allowing one to write compiling code which proves False, have been publicized recently, such as this one:
James E Hanson said:

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic
import Mathlib.NumberTheory.FLT.Basic
import Lean

open Lean

unsafe def badNatUnsafe : ℕ := unsafeCast (-4294967296 : ℤ)

@[implemented_by badNatUnsafe] opaque badNatVal : ℕ

run_elab
  addDecl <| .defnDecl {
    name        := .str .anonymous "badNat"
    levelParams := []
    type        := .const ``Nat []
    value       := .lit <| .natVal badNatVal
    hints       := .opaque
    safety      := .safe
  }

theorem FLT : FermatLastTheorem := by
  have truly_marvelous_0 : ¬badNat ≤ 9223372036854775807 := by decide
  have truly_marvelous_1 : ¬9223372036854775807 < badNat := by decide
  simp_all only [not_le]

#print axioms FLT
-- 'FLT' depends on axioms: [propext]

Given that these exist, how would I convince outside people that such and such theorem has been formally proved using Lean? Clearly, 'I have code on my computer which complies' is not good enough. Is 'I have a code on my computer which compiles and never uses the keyword unsafe' obviously good enough? If so, why is Lean by default set up in such a way that writing an unsafe declaration does not immediately produce at least a warning that this file is potentially compomised and is there a way to change it? Is it the case, that, e.g. mathlib's CI would immediately disallow such a declaration?

[James E Hanson]

Stepan Nesterov said:

Is 'I have a code on my computer which compiles and never uses the keyword unsafe' obviously good enough?

No, it's not.

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic
import Mathlib.NumberTheory.FLT.Basic
import Lean

open Lean

axiom Int_eq_Nat : ℤ = ℕ

def badNatDefinitelySafe : ℕ := cast Int_eq_Nat (-4294967296 : ℤ)

def badNat : ℕ := by_elab return .lit <| .natVal badNatDefinitelySafe

theorem FLT : FermatLastTheorem := by
  have truly_marvelous_0 : ¬badNat > 9223372036854775807 := by decide
  have truly_marvelous_1 : ¬badNat ≤ 9223372036854775807  := by decide
  simp_all only [gt_iff_lt, not_lt]

#print axioms FLT
-- 'FLT' depends on axioms: [propext, Classical.choice, Quot.sound]

[Henrik Böving]

Given that these exist, how would I convince outside people that such and such theorem has been formally proved using Lean?

As the thread you are quoting this from says, the official tool provided for this purpose by the FRO, comparator has not been affected by issues like this so far. As I have explained in that thread, it is also systemically immune against this specific kind of attack.

If so, why is Lean by default set up in such a way that writing an unsafe declaration does not immediately produce at least a warning that this file is potentially compomised and is there a way to change it?

The unsafe keyword here is a red herring, there are several ways to circumvent the use of unsafe to pull this off.

Is it the case, that, e.g. mathlib's CI would immediately disallow such a declaration?

We run mathlib against lean4checker and nanoda on a daily basis, if you were to commit this exploit into mathlib right now (and thus somehow make it past code review with this obviously very suspicious change) it would be noticed within 24 hours. We have plans to add even more defense in depth to this mechanism in the future. That being said we have so far not seen an exploit that would not at least cause suspicion during a mathlib code review. I'd argue the attack scenario of "someone commits wrong code into mathlib" based on these exploits is quite low. A much more likely scenario to me would be e.g. that someone commits a wrong definition as we have e.g. seen with the Navier Stokes conjecture in the formal conjectures repository (in this case wrong by accident but of course purposely introducing a wrong definition is conceivable).

[Yaël Dillies]

Henrik Böving said:

the Navier Stokes conjecture in the formal conjectures repository

Do you mean lean-dojo? FC#1457 is still under review

[Henrik Böving]

Yes lean-dojo sorry, I mix these two up sometiems

[Stepan Nesterov]

Can you give a layman explanation as to what the core reason behind this contradiction in Lean is? It seems like you can somehow replace the actual proof of equality of two numbers with executing code which then exhibits overflow?

[Henrik Böving]

I have already explained this in the original thread: #lean4 > SafeVerify-passing kernel soundness exploit @ 💬

[James E Hanson]

And to be clear the example I posted here really is just a mildly obfuscated version of my original example.

[Stepan Nesterov]

Henrik Böving said:

I have already explained this in the original thread: #lean4 > SafeVerify-passing kernel soundness exploit @ 💬

But where’s the bug actually at? Is it in the Lean kernel, the compiler which translated the tactics to Lean kernel language, the decide tactic, or all of them?

[Henrik Böving]

I find it extremly hard to pinpoint "the bug"in Lean here. The Lean kernel fundamentally assumes that all objects are built only from their constructors and this code just doesn't do that. One might reason that the bug is that the Lean frontend that people use on an everyday basis allows people to produce such declarations and pass them to the kernel but this is intended. The Lean frontend that you use on a daily basis assumes that you are a friendly user and if you aren't we know dozens of tricks like this to make it swallow a theorem. It makes this assumption because not having to defend against a malicious user all the time actually provides tremendous speedup benefits. If you are dealing with a malicious user and want to verify their claim you should use Comparator which successfully upholds the kernel invariant by design and indeed Comparator does not accept this declaration. So one might even argue there is no bug in Lean and/or Comparator here and it's all working as designed. There is of course a bug in SafeVerify here because it does not undertake the effort of comparator to uphold the kernel's fundamental invariant of its objects being built from constructors.

[Stepan Nesterov]

Here is maybe a more precise question (or maybe I'm terribly confused):
unsafeCast is defined by

unsafe def unsafeCast {α : Sort u} {β : Sort v} (a : α) : β :=
  PLift.down (ULift.down.{max u v} (cast lcProof (ULift.up.{max u v} (PLift.up a))))

where lcProof is an unsafe axiom. The proof of FLT uses this definition, therefore #print_axioms, if implemented correctly, should list lcProof as an axiom. Why does it not do that?

[Henrik Böving]

This is a general issue in people's understanding of how Lean works I think. What is happening is that we give a C program a piece of memory that does not fulfill the assumptions of this program and thus makes it do a weird thing. The unsafeCast is not part of the memory that we pass to the kernel, it is just used to aid the creation of this invalid piece of memory to begin with. It could've been built in dozens of other ways by e.g. loading an invalid olean file that was previously written to the disk using some program etc.

[Henrik Böving]

Which is to say you have to distinguish between the meta part and the non-meta part of this program, the unsafeCast only occurs in the meta program to produce a declaration that is already invalidated that can then be used in the non-meta part of the program.

[Stepan Nesterov]

How difficult would it be to specify a subset of Lean which is guaranteed to produce only correct declarations and covers all the things which we use in practice? In other words, does the average Lean user need to be concerned with accidentally creating such a declaration, which then might be a nightmare to debug?

[Henrik Böving]

How difficult would it be to specify a subset of Lean which is guaranteed to produce only correct declarations and covers all the things which we use in practice?

You would have to arguably forbid basically any meta programming, there is lots of ways to create this type of stuff witout unsafe as I have mentioned above.

does the average Lean user need to be concerned with accidentally creating such a declaration

it is almost impossible to do this unintentionally if you are not using unsafe casts, this has never happened in practice before. In general almost all of the bugs of the class that are being discussed here are not interesting if you are just doing Lean yourself. They are of interest to people because they might want to verify e.g. proofs generated by an AI.