path: root/dev/doc/critical-bugs

Preliminary compilation of critical bugs in stable releases of Coq
==================================================================
  WORK IN PROGRESS WITH SEVERAL OPEN QUESTIONS


To add: #7723 (vm_compute universe polymorphism), #7695 (modules and algebraic universes), #7615 (lost functor substitutions)

Typing constructions

  component: "match"
  summary: substitution missing in the body of a let
  introduced: ?
  impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl4
  impacted development branches: none
  impacted coqchk versions: ?
  fixed in: master/trunk/v8.5 (e583a79b5, 22 Nov 2015, Herbelin), v8.4 (525056f1, 22 Nov 2015, Herbelin), v8.3 (4bed0289, 22 Nov 2015, Herbelin)
  found by: Herbelin
  exploit: test-suite/success/Case22.v
  GH issue number: ?
  risk: ?

  component: fixpoint, guard
  summary: missing lift in checking guard
  introduced: probably from V5.10
  impacted released versions: probably V5-V7, V8.0-V8.0pl4, V8.1-V8.1pl4
  impacted development branches: v8.0 ?
  impacted coqchk versions: ?
  fixed in: master/trunk/v8.2 (ff45afa8, r11646, 2 Dec 2008, Barras), v8.1 (f8e7f273, r11648, 2 Dec 2008, Barras)
  found by: Barras
  exploit: test-suite/failure/guard.v
  GH issue number: none
  risk: unprobable by chance

  component: cofixpoint, guard
  summary: de Bruijn indice bug in checking guard of nested cofixpoints
  introduced: after V6.3.1, before V7.0
  impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4
  impacted development branches: none
  impacted coqchk versions: ?
  fixed in: master (9f81e2c36, 10 Apr 2014, Dénès), v8.4 (f50ec9e7d, 11 Apr 2014, Dénès), v8.3 (40c0fe7f4, 11 Apr 2014, Dénès), v8.2 (06d66df8c, 11 Apr 2014, Dénès), v8.1 (977afae90, 11 Apr 2014, Dénès), v8.0 (f1d632992, 29 Nov 2015, Herbelin, backport)
  found by: Dénès
  exploit: ?
  GH issue number: none ?
  risk: ?

  component: inductive types, elimination principle
  summary: de Bruijn indice bug in computing allowed elimination principle
  introduced: 23 May 2006, 9c2d70b, r8845, Herbelin (part of universe polymorphism)
  impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2, V8.4-V8.4pl4
  impacted development branches: none
  impacted coqchk versions: ?
  fixed in: master (8a01c3685, 24 Jan 2014, Dénès), v8.4 (8a01c3685, 25 Feb 2014, Dénès), v8.3 (2b3cc4f85, 25 Feb 2014, Dénès), v8.2 (459888488, 25 Feb 2014, Dénès), v8.1 (79aa20872, 25 Feb 2014, Dénès)
  found by: Dénès
  exploit: see GH#3211
  GH issue number: #3211
  risk: ?

  component: universe subtyping
  summary: bug in Prop<=Set conversion which made Set identifiable with Prop, preventing a proof-irrelevant interpretation of Prop
  introduced: V8.2 (bba897d5f, 12 May 2008, Herbelin)
  impacted released versions: V8.2-V8.2pl2
  impacted development branches: none
  impacted coqchk versions: ?
  fixed in: master/trunk (679801, r13450, 23 Sep 2010, Glondu), v8.3 (309a53f2, r13449, 22 Sep 2010, Glondu), v8.2 (41ea5f08, r14263, 6 Jul 2011, Herbelin, backport)
  found by: Georgi Guninski
  exploit: test-suite/failure/prop_set_proof_irrelevance.v
  GH issue number: none?
  risk: ?

Module system

  component: modules, universes
  summary: missing universe constraints in typing "with" clause of a module type
  introduced: ?
  impacted released versions: V8.3-V8.3pl2, V8.4-V8.4pl6; unclear for V8.2 and previous versions
  impacted development branches: none
  impacted coqchk versions: ?
  fixed in: master/trunk (d4869e059, 2 Oct 2015, Sozeau), v8.4 (40350ef3b, 9 Sep 2015, Sozeau)
  found by: Dénès
  exploit: test-suite/bugs/closed/bug_4294.v
  GH issue number: #4294
  risk: ?

Module system

  component: modules, universes
  summary: universe constraints for module subtyping not stored in vo files
  introduced: presumably 8.2 (b3d3b56)
  impacted released versions: 8.2, 8.3, 8.4
  impacted development branches: v8.5
  impacted coqchk versions: none
  fixed in: v8.2 (c1d9889), v8.3 (8056d02), v8.4 (a07deb4), trunk (0cd0a3e) Mar 5, 2014, Tassi
  found by: Tassi by running coqchk on the mathematical components library
  exploit: requires multiple files, no test provided
  GH issue number: #3243
  risk: could be exploited by mistake

Universes

  component: template polymorphism
  summary: issue with two parameters in the same universe level
  introduced: 23 May 2006, 9c2d70b, r8845, Herbelin
  impacted released versions: V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2
  impacted development branches: none
  impacted coqchk versions: ?
  fixed in: trunk/master/v8.4 (8082d1faf, 5 Oct 2011, Herbelin), V8.3pl3 (bb582bca2, 5 Oct 2011, Herbelin), v8.2 branch (3333e8d3, 5 Oct 2011, Herbelin), v8.1 branch (a8fc2027, 5 Oct 2011, Herbelin), 
  found by: Barras
  exploit: test-suite/failure/inductive.v
  GH issue number: none
  risk: unlikely to be activated by chance

  component: universe polymorphism
  summary: universe polymorphism can capture global universes
  impacted released versions: V8.5 to V8.8
  impacted coqchk versions: V8.5 to V8.9
  fixed in: ec4aa4971f (58e1d0f200 for the checker)
  found by: Gaëtan Gilbert
  exploit: test-suite/misc/poly-capture-global-univs
  GH issue number: #8341
  risk: unlikely to be activated by chance (requires a plugin)

  component: template polymorphism
  summary: template polymorphism not collecting side constrains on the
  universe level of a parameter; this is a general form of the
  previous issue about template polymorphism exploiting other ways to
  generate untracked constraints
  introduced: morally at the introduction of template polymorphism, 23
  May 2006, 9c2d70b, r8845, Herbelin
  impacted released versions: at least V8.4-V8.4pl6, V8.5-V8.5pl3,
  V8.6-V8.6pl2, V8.7.0-V8.7.1, V8.8.0-V8.8.1, V8.9.0-V8.9.1, in theory
  also V8.1-V8.1pl4, V8.2-V8.2pl2, V8.3-V8.3pl2 but not exploit found
  there yet (an exploit using a plugin to force sharing of universe
  level is in principle possible though)
  impacted development branches: all from 8.4 to 8.9 at the time of writing and suspectingly also all from 8.1 to 8.4 if a way to create untracked constraints can be found
  impacted coqchk versions: a priori all (tested with V8.4 and V8.9 which accept the exploit)
  fixed in: soon in master and V8.10.0 (PR #9918, Aug 2019, Dénès and Sozeau)
  found by: Gilbert using explicit sharing of universes, exploit found for 8.5-8.9 by Pédrot, other variants generating sharing using sections, or using ltac tricks by Sozeau, exploit in 8.4 by Herbelin and Jason Gross by adding new tricks to Sozeau's variants
  exploit: test-suite/failure/Template.v
  GH issue number: #9294
  risk: moderate risk to be activated by chance

  component: template polymorphism
  summary: using the same universe in the parameters and the
  constructor arguments of a template polymorphic inductive (using
  named universes in modern Coq, or unification tricks in older Coq)
  produces implicit equality constraints not caught by the previous
  template polymorphism fix.
  introduced: same as the previous template polymorphism bug, morally
  from V8.1, first verified impacted version V8.5 (the universe
  unification is sufficiently different in V8.4 to prevent our trick
  from working)
  fixed in: expected in 8.10.2, 8.11+beta, master (#11128, Nov 2019, Gilbert)
  found by: Gilbert
  exploit: test-suite/bugs/closed/bug_11039.v
  GH issue number: #11039
  risk: moderate risk (found by investigating #10504)

  component: universe polymorphism, asynchronous proofs
  summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
  introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
  impacted released versions: V8.5-V8.10
  impacted development branches: none
  impacted coqchk versions: immune
  fixed in: PR#10664
  found by: Pédrot
  exploit: no test
  GH issue number: none
  risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)

  component: algebraic universes
  summary: Set+2 was incorrectly simplified to Set+1
  introduced: V8.10 (with the SProp commit 75508769762372043387c67a9abe94e8f940e80a)
  impacted released versions: V8.10.0 V8.10.1 V8.10.2
  impacted coqchk versions: same
  fixed in: PR#11422
  found by: Gilbert
  exploit: see PR (custom application of Hurkens to get around the refreshing at elaboration)
  GH issue number: see PR
  risk: unlikely to be triggered through the vernacular (the system "refreshes" algebraic
    universes such that +2 increments do not appear), mild risk from plugins which manipulate
    algebraic universes.

Primitive projections

  component: primitive projections, guard condition
  summary: check of guardedness of extra arguments of primitive projections missing
  introduced: 6 May 2014, a4043608f, Sozeau
  impacted released versions: V8.5-V8.5pl2, 
  impacted development branches: none
  impacted coqchk versions: ?
  fixed in: trunk/master/v8.5 (ba00867d5, 25 Jul 2016, Sozeau)
  found by: Sozeau, by analyzing bug report #4876
  exploit: to be done (?)
  GH issue number: #4876
  risk: consequence of bug found by chance, unlikely to be exploited by chance (MS?)

  component: primitive projections, guard condition
  summary: records based on primitive projections became possibly recursive without the guard condition being updated
  introduced: 10 Sep 2014, 6624459e4, Sozeau (?)
  impacted released versions: V8.5
  impacted development branches: none
  impacted coqchk versions: ?
  fixed in: trunk/master/v8.5 (120053a50, 4 Mar 2016, Dénès)
  found by: Dénès exploiting bug #4588
  exploit: test-suite/bugs/closed/bug_4588.v
  GH issue number: #4588
  risk: ?

Conversion machines

  component: "lazy machine" (lazy krivine abstract machine)
  summary: the invariant justifying some optimization was wrong for some combination of sharing side effects
  introduced: prior to V7.0
  impacted released versions: V8.0-V8.0pl4, V8.1-V8.1pl3
  impacted development branches: none
  impacted coqchk versions: (eefe63d52, Barras, 20 May 2008), was in beta-development for 8.2 at this time
  fixed in: master/trunk/8.2 (f13aaec57/a8b034513, 15 May 2008, Barras), v8.1 (e7611477a, 15 May 2008, Barras), v8.0 (6ed40a8bc, 29 Nov 2016, Herbelin, backport)
  found by: Gonthier
  exploit: by Gonthier
  GH issue number: none
  risk: unrealistic to be exploited by chance

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: collision between constructors when more than 256 constructors in a type
  introduced: V8.1
  impacted released versions: V8.1-V8.5pl3, V8.2-V8.2pl2, V8.3-V8.3pl3, V8.4-V8.4pl5
  impacted development branches: none
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: master/trunk/v8.5 (00894adf6/596a4a525, 26-39 Mar 2015, Grégoire), v8.4 (cd2101a39, 1 Apr 2015, Grégoire), v8.3 (a0c7fc05b, 1 Apr 2015, Grégoire), v8.2 (2c6189f61, 1 Apr 2015, Grégoire), v8.1 (bb877e5b5, 29 Nov 2015, Herbelin, backport)
  found by: Dénès, Pédrot
  exploit: test-suite/bugs/closed/bug_4157.v
  GH issue number: #4157
  risk: 

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: wrong universe constraints
  introduced: possibly exploitable from V8.1; exploitable at least from V8.5
  impacted released versions: V8.1-V8.4pl5 unknown, V8.5-V8.5pl3, V8.6-V8.6.1, V8.7.0-V8.7.1
  impacted development branches: unknown for v8.1-v8.4, none from v8.5
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: master (c9f3a6cbe, 12 Feb 2018, PR#6713, Dénès), v8.7 (c058a4182, 15 Feb 2018, Zimmermann, backport), v8.6 (a2cc54c64, 21 Feb 2018, Herbelin, backport), v8.5 (d4d550d0f, 21 Feb 2018, Herbelin, backport)
  found by: Dénès
  exploit: test-suite/bugs/closed/bug_6677.v
  GH issue number: #6677
  risk: 

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: missing pops in executing 31bit arithmetic
  introduced: V8.5
  impacted released versions: V8.1-V8.4pl5
  impacted development branches: v8.1 (probably)
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: master/trunk/v8.5 (a5e04d9dd, 6 Sep 2015, Dénès), v8.4 (d5aa3bf6, 9 Sep 2015, Dénès), v8.3 (5da5d751, 9 Sep 2015, Dénès), v8.2 (369e82d2, 9 Sep 2015, Dénès), 
  found by: Catalin Hritcu
  exploit: lost?
  GH issue number: ?
  risk: 

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: primitive integer emulation layer on 32 bits not robust to garbage collection
  introduced: master (before v8.10 in GH pull request #6914)
  impacted released versions: none
  impacted development branches:
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in:
  found by: Roux, Melquiond
  exploit:
  GH issue number: #9925
  risk:

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: broken long multiplication primitive integer emulation layer on 32 bits
  introduced: e43b176
  impacted released versions: 8.10.0, 8.10.1, 8.10.2
  impacted development branches: 8.11
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: 4e176a7
  found by: Soegtrop, Melquiond
  exploit: test-suite/bugs/closed/bug_11321.v
  GH issue number: #11321
  risk: critical, as any BigN computation on 32-bit architectures is wrong

  component: "native" conversion machine (translation to OCaml which compiles to native code)
  summary: translation of identifier from Coq to OCaml was not bijective, leading to identify True and False
  introduced: V8.5
  impacted released versions: V8.5-V8.5pl1
  impacted development branches: none
  impacted coqchk versions: none (no native computation in coqchk)
  fixed in: master/trunk/v8.6 (244d7a9aa, 19 May 2016, letouzey), v8.5 (088b3161c, 19 May 2016, letouzey), 
  found by: Letouzey, Dénès
  exploit: see commit message for 244d7a9aa
  GH issue number: ?
  risk: 

  component: primitive projections, native_compute
  summary: stuck primitive projections computed incorrectly by native_compute
  introduced: 1 Jun 2018, e1e7888a, ppedrot
  impacted released versions: 8.9.0
  impacted coqchk versions: none
  found by: maximedenes exploiting bug #9684
  exploit: test-suite/bugs/closed/bug_9684.v
  GH issue number: #9684

  component: lazy machine
  summary: incorrect De Bruijn handling when inferring the relevance mark for a lambda
  introduced: 2019-03-15, 23f84f37c674a07e925925b7e0d50d7ee8414093 and 71b9ad8526155020c8451dd326a52e391a9a8585, SkySkimmer
  impacted released versions: 8.10.0
  impacted coqchk versions: 8.10.0
  found by: ppedrot investigating unexpected conversion failures with SProp
  exploit: test-suite/bugs/closed/bug_10904.v
  GH issue number: #10904
  risk: none without using -allow-sprop (off by default in 8.10.0),
        otherwise could be exploited by mistake

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: buffer overflow on large accumulators
  introduced: 8.1
  impacted released versions: 8.1-8.12.1
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: 8.13.0
  found by: Dolan, Roux, Melquiond
  GH issue number: ocaml/ocaml#6385, #11170
  risk: medium, as it can happen for large irreducible applications

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: buffer overflow on large records and closures
  introduced: 8.1
  impacted released versions: 8.1-now
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in:
  found by: Dolan, Roux, Melquiond
  GH issue number: ocaml/ocaml#6385, #11170
  risk: unlikely to be activated by chance, might happen for autogenerated code

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: buffer overflow, arbitrary code execution on floating-point operations
  introduced: 8.13
  impacted released versions: 8.13.0
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: 8.13.1
  found by: Melquiond
  GH issue number: #13867
  risk: none, unless using floating-point operations; high otherwise;
        noticeable if activated by chance, since it usually breaks
        control-flow integrity

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: arbitrary code execution on irreducible PArray.set
  introduced: 8.13
  impacted released versions: 8.13.0, 8.13.1
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: 8.13.2
  found by: Melquiond
  GH issue number: #13998
  risk: none, unless using primitive array operations; systematic otherwise

Side-effects

  component: side-effects
  summary: polymorphic side-effects inside monomorphic definitions incorrectly handled as not inlined
  introduced: ?
  impacted released versions: at least from 8.6 to 8.12.0
  impacted coqchk versions: none (no side-effects in the checker)
  found by: ppedrot
  exploit: test-suite/bugs/closed/bug_13330.v
  GH issue number: #13330
  risk: unlikely to be exploited by mistake, requires the use of unsafe tactics

Conflicts with axioms in library

  component: library of real numbers
  summary: axiom of description and decidability of equality on real numbers in library Reals was inconsistent with impredicative Set
  introduced: 67c75fa01, 20 Jun 2002
  impacted released versions: 7.3.1, 7.4
  impacted coqchk versions: 
  fixed by deciding to drop impredicativity of Set: bac707973, 28 Oct 2004
  found by: Herbelin & Werner
  exploit: need to find the example again
  GH issue number: no
  risk: unlikely to be exploited by chance

  component: library of extensional sets, guard condition
  summary: guard condition was unknown to be inconsistent with propositional extensionality in library Sets
  introduced: not a bug per se but an incompatibility discovered late
  impacted released versions: technically speaking from V6.1 with the introduction of the Sets library which was then inconsistent from the very beginning without we knew it
  impacted coqchk versions: ?
  fixed by constraining the guard condition: (9b272a8, ccd7546c 28 Oct 2014, Barras, Dénès)
  found by: Schepler, Dénès, Azevedo de Amorim
  exploit: ?
  GH issue number: none
  risk: unlikely to be exploited by chance (?)

  component: library for axiom of choice and excluded-middle
  summary: incompatibility axiom of choice and excluded-middle with elimination of large singletons to Set
  introduced: not a bug but a change of intended "model"
  impacted released versions: strictly before 8.1
  impacted coqchk versions: ?
  fixed by constraining singleton elimination: b19397ed8, r9633, 9 Feb 2007, Herbelin
  found by: Benjamin Werner
  exploit:
  GH issue number: none
  risk:

  component: primitive floating-points
  summary: Incorrect specification of PrimFloat.leb
  introduced: 8.11
  impacted released versions: 8.11.0, 8.11.1, 8.11.2
  fixed by fixing the spec: #12484
  found by: Pierre Roux
  exploit: test-suite/bugs/closed/bug_12483.v 
  GH issue number: #12483
  risk: proof of false when using the incorrect axiom

There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1).

There were otherwise maybe unexploitable kernel bugs, e.g. 2df88d83 (Require overloading), 0adf0838 ("Univs: uncovered bug in strengthening of opaque polymorphic definitions."), 5122a398 (#3746 about functors), #4346 (casts in VM), a14bef4 (guard condition in 8.1), 6ed40a8 ("Georges' bug" with ill-typed lazy machine), and various other bugs in 8.0 or 8.1 w/o knowing if they are critical.

Another non exploitable bug?

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: bug in 31bit arithmetic
  introduced: V8.1
  impacted released versions: none
  impacted development branches: 
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: master/trunk/v8.5 (0f8d1b92c, 6 Sep 2015, Dénès)
  found by: Dénès, from a bug report by Tahina Ramananandro
  exploit: ?
  GH issue number: ?
  risk: