Obj.magic for Coq?! · Coq users · Zulip Chat Archive

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)
*)

Pierre-Marie Pédrot (Nov 23 2022 at 13:53):

Pierre-Marie Pédrot (Nov 23 2022 at 13:59):

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. *)

Gaëtan Gilbert (Nov 23 2022 at 14:00):

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

Pierre-Marie Pédrot (Nov 23 2022 at 14:01):

Pierre-Marie Pédrot (Nov 23 2022 at 14:02):

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

Paolo Giarrusso (Nov 23 2022 at 19:00):

Paolo Giarrusso (Nov 23 2022 at 19:02):

Gaëtan Gilbert (Nov 23 2022 at 19:25):

Gaëtan Gilbert (Nov 23 2022 at 19:27):

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

Paolo Giarrusso (Nov 23 2022 at 19:31):

aka Eval vm_compute in term assumes but does not enforce that term is well-typed?

Gaëtan Gilbert (Nov 23 2022 at 19:34):

Andres Erbsen (Nov 23 2022 at 21:37):

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.

Demi Obenour (Nov 24 2022 at 06:46):

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:.

Guillaume Melquiond (Nov 24 2022 at 06:50):

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.

Guillaume Melquiond (Nov 24 2022 at 06:52):

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.

Demi Obenour (Nov 24 2022 at 06:56):

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.

Demi Obenour (Nov 24 2022 at 06:58):

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

Gaëtan Gilbert (Nov 24 2022 at 08:52):

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

Stream: Coq users

Topic: Obj.magic for Coq?!

Gaëtan Gilbert (Nov 23 2022 at 13:43):