|
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 current (NOT FIXED)
fixed in: 2385b5c1ef
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
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: "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
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:
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:
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
