Stream: Coq users

Topic: Obj.magic for Coq?!


view this post on Zulip Gaëtan Gilbert (Nov 23 2022 at 13:43):

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

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2022 at 13:53):

How many SEGFAULTs can we get with this?

view this post on Zulip 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. *)

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

view this post on Zulip Gaëtan Gilbert (Nov 23 2022 at 14:00):

segfault is pretty easy

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

view this post on Zulip Pierre-Marie Pédrot (Nov 23 2022 at 14:01):

that's not very serious...

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 23 2022 at 19:00):

no proof of False yet?

view this post on Zulip Paolo Giarrusso (Nov 23 2022 at 19:02):

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 ?

view this post on Zulip Gaëtan Gilbert (Nov 23 2022 at 19:25):

it's not a bug imo
if it is it's not fixable

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 23 2022 at 19:31):

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

view this post on Zulip Gaëtan Gilbert (Nov 23 2022 at 19:34):

yes

view this post on Zulip 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.

view this post on Zulip Demi Obenour (Nov 24 2022 at 06:46):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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")

view this post on Zulip Gaëtan Gilbert (Nov 24 2022 at 08:52):

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

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 15:36):

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


Last updated: Jan 28 2023 at 05:02 UTC