1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
|
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/bugs/closed/4294.v
GH issue number: #4294
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/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/inductive4.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)
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/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/failure/vm-bug4157.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/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: "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: lost?
GH issue number: ?
risk:
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:
|
