warning: hack

```
Inductive noption A := nNone | nSome (_:A) | Somethingelse.
Definition bla : noption (noption unit) :=
Eval vm_compute in
id ltac:(exact_no_check (Some (Some tt))).
Print bla.
(* bla = nSome (noption unit) (nSome unit tt)
: noption (noption unit)
*)
```

How many SEGFAULTs can we get with this?

```
Definition bla : forall b : bool, if b then True else False :=
Eval vm_compute in
id ltac:(exact_no_check (fun x : bool => I)).
(* The type int must be registered before this construction can be typechecked. *)
```

hopefully it's a necessary but not sufficient random requirement...

segfault is pretty easy

```
Eval vm_compute in
match ltac:(exact_no_check false) with
| Some _ => 0
| None => 1
end.
```

that's not very serious...

10 internet points to whoever uses PArrays to randomly mutate some parts of the memory or something.

no proof of `False`

yet?

I can't find an issue for this in https://github.com/coq/coq/issues?q=is%3Aissue+is%3Aopen+sort%3Aupdated-desc+label%3A%22kind%3A+inconsistency%22, should this be fixed for 8.16.1 ?

it's not a bug imo

if it is it's not fixable

for a proof of False you would need to get a security researcher to turn the segfault into arbitrary code execution

aka `Eval vm_compute in term`

assumes but does not enforce that `term`

is well-typed?

yes

```
Require Import PrimInt63 PArray. Open Scope uint63_scope.
From Ltac2 Require Import Ltac2 Constr.
Ltac2 Eval
let length := constr:(@length int) in
let copy := constr:(@copy int) in
let set := constr:(@set int) in
let x := constr:((Some ([| 0 | 7 |] ) )) in
let y := Unsafe.make (Unsafe.App set (Array.of_list [x; '1; '99])) in
let z := Unsafe.make (Unsafe.App copy (Array.of_list [y])) in
Std.eval_vm None z.
```

The `set`

is executed and then `copy`

anomalies; with `length`

it just returns a bogus length (`2`

). Same with native.

Gaëtan Gilbert said:

for a proof of False you would need to get a security researcher to turn the segfault into arbitrary code execution

That’s probably the hard way. The easier way would be to produce an incorrect result, so that `compute`

and `vm_compute`

disagree. Then proving `False`

is trivial.

That said, at this point one has arbitrary read/write in a scripting context, so it is not going to be hard to bypass ASLR, etc and get code execution. Hopefully MetaCoq will make all of this go away; I am pretty sure that “no memory corruption” will be part of the spec :laughing:.

No, using `compute`

and `vm_compute`

will not help, since the term is ill-typed anyway, whichever way you check it, so it cannot be used in a proof. Thus, you actually need to corrupt the memory to achieve a proof of False.

I can see three ways of corrupting the memory: primitive arrays, cofixpoints, and peepholed floats. The latter two seem a bit too complicated to use, but primitive arrays look trivial enough to abuse.

Simplest approach is probably to find memory Coq assumes is immutable and mutate it, so that e.g. one winds up proving `x = 0`

and `x = 1`

for the same `x`

.

That assumes one is trying to be subtle; if one wants to be evil there is always `system("unix command")`

Demi Obenour said:

Simplest approach is probably to find memory Coq assumes is immutable and mutate it, so that e.g. one winds up proving

`x = 0`

and`x = 1`

for the same`x`

.

if you're mutating memory you just modify the type of some already proved constant to `False`

thanks @Andres Erbsen for filing the issue https://github.com/coq/coq/issues/16891

Last updated: Jan 28 2023 at 05:02 UTC