558442 - Verifier allows branch target not aligned to instruction boundary

Status: VERIFIED FIXED

(Tamarin Graveyard :: Virtual Machine, defect, P2)

Description

[William Maddox]

See discussion starting at comment #15 for bug 555097.

https://bugzilla.mozilla.org/show_bug.cgi?id=555097#c15

Comment 1

[Edwin Smith]

This was injected by the verifier semantics upgrade.  First attempt at a fix failed, working on a second attempt.

Comment 2

[Dan Smith]

Declassified.

Comment 3

[Edwin Smith]

Attachment: test case with corrupted catch target address

this is a try/catch that throws, and the catch handler points to the middle of "pushbyte -105", where -105 is the value of OP_bitnot.  The skipped portion of the catch block is dead code, so the verifier never visits it, so there is no detection of jumping to the middle of an instruction, because the beginning of the instruction is not reachable.

(copied test case from bug 555097)

Comment 4

[Edwin Smith]

Attachment: corrupted test case with an exception handler jumping to the middle of a reachable instruction

The bad_handler/handler_test_corrupted.abc test case should fail to verify because code jumps to the middle of a reachable instruction.  test cases copied from bug 555097.

Comment 5

[Edwin Smith]

Attachment: detect overlapping blocks, indicative of a branch to the middle of an instruction

If there is a branch to the middle of a reachable instruction, then it follows that the verifier will encounter overlapping blocks.  The block that contains the targeted instruction will not end in the middle of the instruction, yet a different block will start there.

This patch simply detects overlapping blocks during the second phase when we visit each block in linear order.  Failure occurs at the moment the overlap is discovered.

With this patch, the first test case does not fail to verify (branch to middle of unreachable instruction), and the second one does (branch to the middle of a reachable instruction).

Comment 6

[Edwin Smith]

Comment on attachment 438480 [details] [diff] [review]
detect overlapping blocks, indicative of a branch to the middle of an instruction

Asking for two careful reviews since this is targeted for 10.1 and its important to get it right.

Comment 7

[Tom Harwood]

(In reply to comment #6)
> (From update of attachment 438480 [details] [diff] [review])

From the looks of this patch, the first block isn't in blockStates.  Is that correct?  If so, a comment to that effect would be helpful, a 0..n counting loop generally implies "do all of 'em."

Comment 8

[Edwin Smith]

Correct, will add comment before pushing.

Comment 9

[Tom Harwood]

Comment on attachment 438480 [details] [diff] [review]
detect overlapping blocks, indicative of a branch to the middle of an instruction

The patch looks sound.  I wonder if it's really the right way to go, though; why not accept the program if it's sound in all other respects?

Comment 10

[Edwin Smith]

Attachment: (v2) detect overlapping blocks, indicative of a branch to the middle of an instruction

The previous patch exposed a subtle bug dealing with the ENTRY block (which starts at code_pos 0). 

consider this code:

function foo() {
Loop:
  label
  findpropstrict print
  getlocal 1
  callpropvoid 1

  getlocal 1
  increment_i
  dup
  setlocal 1
  pushbyte 3
  iflt Loop

  returnvoid
}

In the case when ENTRY starts with a label and is jumped to from below, two problems happened:

1. The type checker verifies the block along the entry path, and doesn't detect that that bytecode 0 is reachable as a fallthrough block, since pc == start_pos.  later, it sees the edge, and initializes a FrameState block for the first time, with the state along the jump edge.  (no merge occurs since the entry block was implicit).  the worklist algorithm never re-visits along the entry path.

2. phase 2 begins by explicitly visiting the ENTRY block, then visiting all known blocks.  This causes the ENTRY block to be visited twice.  The first time, with the ENTRY state (local 1 is undefined), and the second time, with the loop edge state, with local 1 containing a known int.

The code is safe; we have accidentally, but correctly, peeled off the first loop iteration.

NOW:  with the first verifier patch, the code fails verification because visiting the ENTRY block twice is detected as encountering overlapping blocks.

my first attempt at a fix only modified phase 2:  don't explicitly verify the ENTRY block if we know it's in frameStates.  This avoids the accidental loop peeling, but generates unsound JIT code with the invalid assumption that local 1 always contains an int.

the correct fix is to fix the typechecker (phase 1) and phase 2, to both deal properly with the case when the ENTRY block is reachable as a loop target.

Comment 11

[Edwin Smith]

Attachment: Do-while loop test case

Comment 12

[Tom Harwood]

(In reply to comment #10)
> Created an attachment (id=438488) [details]
> the correct fix is to fix the typechecker (phase 1) and phase 2, to both deal
> properly with the case when the ENTRY block is reachable as a loop target.

How about if the entry block is a catch target?

Comment 13

[Tom Harwood]

(In reply to comment #12)
> (In reply to comment #10)
> How about if the entry block is a catch target?

After a little reflection, I think failing such a program might be a feature, not a bug.

Comment 14

[Edwin Smith]

A catch target can't be at offset(In reply to comment #9)
> (From update of attachment 438480 [details] [diff] [review])
> The patch looks sound.  I wonder if it's really the right way to go, though;
> why not accept the program if it's sound in all other respects?

I think its wrong for the verifier to accept a program that *requires* a compiler to replicate code to get proper semantics.   Correctly compiling overlapping blocks requires each instruction (or instruction-part) that appears in more than one block to be translated in the context of that block.  Strikes me as highly wonky, even if it could be spec'd out to work deterministically.

(In reply to comment #12)
> (In reply to comment #10)
> > Created an attachment (id=438488) [details] [details]
> > the correct fix is to fix the typechecker (phase 1) and phase 2, to both deal
> > properly with the case when the ENTRY block is reachable as a loop target.
> 
> How about if the entry block is a catch target?

That would be a good test case.  we have this rule in parseExceptionHandlers:

                if (handler->from < 0 ||
                    handler->to < handler->from ||
                    handler->target < handler->to ||
                    handler->target >= code_length)
                {
                    // illegal range in handler record
                    verifyFailed(kIllegalExceptionHandlerError);
                }

My reading of it, is that this exception range would be legal:

  [0, 0) => 0

This should give you a catch block that can never be called.  We should never check an implicit edge to that target, since the try contains no instructions.

Comment 15

[Tom Harwood]

(In reply to comment #14)
> I think its wrong for the verifier to accept a program that *requires* a
> compiler to replicate code to get proper semantics.

That position has merit, but the obvious use for such a program is obfuscation.  It would only be effective against a simple-minded decompiler, though.

Comment 16

[Edwin Smith]

For 10.1, i want to reject programs with overlapping blocks, but we could consider allowing it in a future version if there is value in it.  But I doubt obfuscation will be a driver: given that abcdump will probably sprout logic similar to the verifier for printing code (skipping unreachable code), and that the "canonical" bytecode parser (the verifier) is open source, it isn't a stretch to imagine easily defeating such obfuscation.

Comment 17

[Tom Harwood]

(In reply to comment #10)
> Created an attachment (id=438488) [details]

The checkTarget(code_pos-1,code_pos) seems a bit fragile.  If checkTarget() ever assumed that current pointed to addressable storage then lulz will ensue.  Since current is only used in arithmetic style comparisons, it could be type uintptr_t.

Comment 18

[Tom Harwood]

(In reply to comment #16)
> For 10.1,  reject ... could [allow] it in a future version if there is value 

+1, easier to allow than to disallow after it's been released.

Comment 19

[Tom Harwood]

Comment on attachment 438488 [details] [diff] [review]
(v2) detect overlapping blocks, indicative of a branch to the middle of an instruction

r+ with the caveat that we need to harden checkTarget()'s usage of current.  A comment for this release with a future bug to clean up the latent issue works for me.

Comment 20

[Edwin Smith]

I worry just a bit about any other areas of the VM that could scan unverified
ABC in linear order, without emulating branch edges or skipping unreachable
code.  The debugger comes to mind, as does utils/abcdump, even though its not
part of the VM.  It is undesireable if the verifier and other tools have
different ideas about the meaning of the same ABC code, due to abstract
interpretation.

Comment 21

[William Maddox]

The second pass indeed does visit the blocks in ABC order, but it may be worth noting in a comment that this is a consequence of maintaining blockstates as a sorted map.

Regarding disassembly: Our disassembler and debugger are in no worse position than those in native code environments.  Tools understand that assemblers and compilers generate code in a certain way, and can be confused by code that executes correctly but is not structured in the expected way.

Comment 22

[Edwin Smith]

comment added, pushed to tr-argo and tr
http://hg.mozilla.org/tamarin-redux/rev/9eb57e1a8d23

Comment 23

[Chris Peyer]

3 Attached testcases pushed to tr and argo:
http://hg.mozilla.org/tamarin-redux/rev/dbfb28ed3562

Comment 24

[Edwin Smith]

The expected result for regress/bug_558442a.abc_

is to print -1, and exit code 0.

This test does not jump to the middle of any reachable instructions, and the reachable paths all contain valid bytecode that satisfy the verifier constraits.  If anything, abcdump needs to be fixed so it prints the bytecode properly as seen by the VM.

Marking the test case as 'skip' until we can run it properly.  We just need a way to tell the test framework what the expected output should be.