diff options
| author | Guillaume Melquiond | 2021-02-16 23:19:10 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-02-16 23:19:10 +0100 |
| commit | 70caa6eb02c69b30e5307db02bf5c81f1a2b84dc (patch) | |
| tree | 63fd7aa231595e7a3b1269782e71b90ad5d9c511 | |
| parent | c6bc1cea49cb5a18142437325ecb6875514c22bb (diff) | |
Fix missing arities of VM opcodes.
Since the compiler initializes the arities to zero, coq_tcode_of_code
wrongly believes that the word following a primitive operation contains
an opcode, while it is the global index of the primitive operation. So,
the function will try to translate it and thus corrupt it. But as long as
the evaluated term fully reduces (which is always the case for
CoqInterval), the corrupted word will never be read.
At this point, it all depends on the arity of the global index (seen as
an opcode). If it is zero, then coq_tcode_of_code will recover and
correctly translate the following opcodes. If it is nonzero, then the
function starts translating random words, possibly corrupting the memory
past the end of the translation buffer. Independently of this memory
corruption, coq_interprete will execute random code once it gets to the
opcode following the primitive operation, since it has not been
translated.
The reason CoqInterval is not always crashing due to this bug is just
plain luck. Indeed, the arity of the pseudo opcode only depends on the
global index of the primitive operations. So, as long as this arity is
zero, the memory corruption is fully contained. This happens in the vast
majority of cases, since coq_tcode_of_code translates any unrecognized
opcode to STOP, which has arity zero.
This bug is exploitable.
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 4bc6848ba7..2c0b580e24 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -70,7 +70,9 @@ void init_arity () { arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]= - arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1; + arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]= + arity[CHECKNEXTUPFLOATINPLACE]=arity[CHECKNEXTDOWNFLOATINPLACE]= + 1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]= |