critical-bugs

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

##################################################################
##################### Non fixed bugs #############################
##################################################################

  component: VM reduction machine
  summary: buffer overflow on large records and closures (infinite loop with OCaml 5)
  introduced: 8.1
  impacted versions: 8.1-NOW
  impacted coqchk versions: none (no VM in coqchk)
  fixed in: NONE
  found by: Dolan, Roux, Melquiond
  GH issue number: ocaml/ocaml#6385, #13439
  exploit: ??
  risk: requires very large number of arguments, fix block size or nested letins

  component: VM and native reduction machines
  summary: memory corruption by evaluating on ill-typed terms (obtained from unsafe tactics)
  introduced: 8.1
  impacted versions: 8.1-NOW
  impacted coqchk versions: none (no VM or native in coqchk)
  fixed in: NONE
  found by: Gaëtan Gilbert, Andres Erbsen
  GH issue number: #16891
  exploit: requires a memory corruption to craft something that doesn't just SIGSEV
  risk: could be activated by chance but unlikely to produce anything
        other than SIGSEV outside a deliberate attack

  component: name handling / typechecker
  summary: kernel and checker accept incorrect name aliasing information
  introduced: a long time ago
  impacted versions: -NOW
  impacted coqchk versions: same
  fixed in: NONE
  found by: Pierre-Marie Pédrot
  GH issue number: #7609
  exploit: see issue (requires a plugin or hand crafted .vo file)
  risk: low

  component: primitive types and operators
  summary: coqchk checks too little about primitive declarations
  introduced: v8.10 (#6914 primitive integers)
  impacted versions: coqchk only
  impacted coqchk versions: V8.10-NOW
  fixed in: NONE
  found by: Gaëtan Gilbert
  GH issue number: #12439
  exploit: not fully worked out, requires crafted .vo file
  risk: none (requires crafted .vo file)

  component: module functors
  summary:  Print Assumptions + Parameter Inline fails to report some inconsistent flags
  introduced: #79
  impacted versions: V8.6-NOW
  impacted coqchk versions: none
  found by: Jason Gross
  GH issue number: #12155
  exploit: see issue
  risk: moderate if not using coqchk, none if using coqchk (coqchk rejects the produced file)

  component: module functors
  summary: Print Assumptions does not report Unset Universe Checking used during functor application
  introduced: v8.11 (#10291) or earlier 
  impacted versions: V8.11-NOW
  impacted coqchk versions: none
  found by: Gaëtan Gilbert
  GH issue number: #16646
  exploit: see issue
  risk: moderate if not using coqchk, none if using coqchk (coqchk rejects the produced file)

##################################################################
######################### Fixed bugs #############################
##################################################################

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/bug_4294.v
  GH issue number: #4294
  risk: ?

  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

  component: modules, universes, inductives
  summary: module subtyping disrespected squashing status of inductives
  introduced: probably 7.4 (12965209478bd99dfbe57f07d5b525e51b903f22)
  impacted released versions: until 8.15.0
  impacted coqchk versions: none
  fixed in: 8.15.1, 8.16
  found by: Pédrot
  exploit: see GitHub issue
  GH issue number: #15838
  risk: unlikely (caught by coqchk, needs Unset Elimination Schemes in the module type)

  component: Modules
  summary: Functor inlining drops universe substitution
  introduced: ?
  impacted released versions: ??-V8.8.0
  impacted coqchk versions: same? not sure if coqchk has a this bug
  fixed in: V8.8.1, V8.9.0 (#7616)
  found by: Pierre-Marie Pédrot
  GH issue number: #7615
  exploit: see issue
  risk: medium

  component: modules, primitive types
  summary: Primitives are incorrectly considered convertible to anything by module subtyping
  introduced: 8.11
  impacted released versions: V8.11.0-V8.18.0
  impacted coqchk versions: same
  fixed in: V8.19.0
  found by: Gaëtan Gilbert
  GH issue number: #18503
  exploit: see issue
  risk: high if there is a Primitive in a Module Type, otherwise low

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

  component: cumulative inductives and sections
  summary: variance inference for section universes ignored use of section universes in inductives and axioms defined before the inductive being inferred
  introduced: V8.12 (73c3b874633d6f6f8af831d4a37d0c1ae52575bc)
  impacted released versions: V8.12 to V8.15 including patch releases
  impacted coqchk versions: none
  fixed in: V8.16 PR#15950 (118ffbc010ce53ebd45baa42edd28335301ca9a5)
  found by: Gilbert and Pédrot
  exploit: see #15916
  risk: could be used inadvertently in developments with complex universe usage, only when using cumulative inductives declared in sections. coqchk still works.

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/bug_4588.v
  GH issue number: #4588
  risk: ?

  component: modules and universes
  summary: incorrect checking of subtyping with algebraic universes
  introduced: a long time ago
  impacted released versions: ??-V8.8.0
  impacted coqchk versions: same
  fixed in: V8.8.1, V8.9.0 (#7798)
  found by: Gaëtan Gilbert
  GH issue number: #7695
  exploit: see issue
  risk: needs usage of explicit algebraic universe annotations, coqchk
        may catch through defunctorialization

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/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/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: v8.10
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: 5914313 (v8.10)
  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/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/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/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 (#13431)
  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, 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

  component: "virtual machine" (compilation to bytecode ran by a C-interpreter)
  summary: arbitrary code execution on arrays of floating point numbers
  introduced: 8.13
  impacted released versions: 8.13.0, 8.13.1, 8.14.0
  impacted coqchk versions: none (no virtual machine in coqchk)
  fixed in: 8.14.1
  found by: Melquiond
  GH issue number: #15070
  risk: none, unless mixing open terms and primitive floats inside primitive
  arrays; critical otherwise

  component: "native" conversion machine (translation to OCaml which compiles to native code)
  summary: conversion of Prod / Prod values was comparing the wrong components
  introduced: V8.5
  impacted released versions: V8.5-V8.16.0 (when built with native computation enabled)
  impacted coqchk versions: none (no native computation in coqchk)
  fixed in: 8.16.1
  found by: Melquiond
  GH issue number: #16645
  risk: systematic

  component: "virtual" and "native" conversion machines
  summary: η-expansion of cofixpoints was performed in the wrong environment
  introduced: V8.9
  impacted released versions: V8.9-V8.16.0
  impacted coqchk versions: none (no VM / native computation in coqchk)
  fixed in: 8.16.1
  found by: Gaëtan Gilbert and Pierre-Marie Pédrot
  GH issue number: #16831
  risk: low, as it requires carefully crafted cofixpoints

  component: all 3 kernel conversion machines (lazy, VM, native), primitive arrays
  summary: conversion would compare the mutated version of primitive arrays instead of undoing mutation where needed
  introduced: V8.13
  impacted released versions: V8.13 to V8.16.0
  impacted coqchk versions: same
  fixed in: V8.16.1, V8.17
  found by: Maxime Buyse and Andres Erbsen
  exploit: Andres Erbsen
  GH issue number: #16829
  risk: some if using primitive arrays

  component: "virtual" reduction machine
  summary: tactic code could mutate a global cache of values for section variables
  introduced: V8.1
  impacted released versions: V8.1-V8.16.1
  impacted coqchk versions: none (no tactics in coqchk, VM only sees checked terms)
  fixed in: V8.17.0
  found by: Gaëtan Gilbert with hint from Pierre-Marie Pédrot
  GH issue number: #16957
  risk: the full exploitation seems to require "Definition := ltac:()"
        with change_no_check on a section variable in the ltac

  component: VM machine
  summary: incorrect handling of universe polymorphism
  introduced: V8.5
  impacted released versions: V8.5-V8.8.0
  impacted coqchk versions: none (no VM in coqchk)
  fixed in: V8.8.1, V8.9.0
  found by: Jason Gross
  GH issue number: #7723
  exploit: see issue
  risk: ??

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/bug_13330.v
  GH issue number: #13330
  risk: unlikely to be exploited by mistake, requires the use of unsafe tactics

Forgetting unsafe flags

  component: sections
  summary: unsafe typing flags used inside a section would not be reported by Print Assumptions
           after closing the section
  introduced: abab878b8d8b5ca85a4da688abed68518f0b17bd (#10291, 8.11)
              technically available earlier through plugins
  impacted coqchk versions: none (coqchk rejects affected files)
  found by: Anton Trunov
  GH issue number: #14317
  risk: low as it needs the use of explicit unsafe flags 

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/bug_12483.v 
  GH issue number: #12483
  risk: proof of false when using the incorrect axiom

  component: floating-point library
  summary: Incorrect implementation of SFclassify.
  introduced: 8.11
  impacted released versions: 8.11.0-8.15.1
  fixed by fixing the implementation: #16101
  found by: François Bobot
  exploit: test-suite/bugs/bug_16096.v
  GH_issue_number: #16096
  risk: proof of false when using the axioms in Floats.Axioms.

  component: primitive floating-points + "native" conversion machine (translation to OCaml which compiles to native code)
  summary: nativenorm reading back closures as arbitrary floating-point values
  introduced: 8.11
  impacted released versions: 8.11.0-8.17.1
  impacted coqchk versions: none (no native computation in coqchk)
  fixed in: 8.18.0
  found by: Jason Gross
  GH issue number: #17871
  risk: proof of false when using primitive floats and native_compute

Deserialization

  component: coqchk (coqc trusts that .vo files are well formed)
  summary: deserialization of .vo data not properly checked
  introduced: 8.16 (univ levels), 8.10 (retroknowledge)
  impacted released versions: 8.10-8.18.1
  impacted coqchk versions: same
  fixed in: 8.19
  found by: Mario Carneiro
  GH issue number: N/A (fix pull requests: #18403, #18406)
  risk: can lead to segfaults or arbitrary code execution on crafted .vo files
    (files produced by coqc are fine)

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: