aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/critical-bugs12
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 79c2155823..4452baf513 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -332,6 +332,18 @@ Conversion machines
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
+
Side-effects
component: side-effects