Integrity Error Not Captured

[dz333]

Bug description: An untrusted input can modify data in a trusted array when the array index is untrusted.

Code example: In the code, tag1[N] is a trusted array, but the input "tag_in" and the address "index" are untrusted. Assignment "tag1[index] := tag_in" indicates that an untrusted input can affect the trusted data stored in the array, which is incorrect.

Possible solution?: "tag1[index]" should be treated as untrusted when it is a right value in an assignment because the data source is controlled by the adversary; while "tag1[index]" should be trusted when it is a left value in an assignment.

class ErrorExample extends Module {
  val io = IO(new Bundle {
    val way       = Input(UInt(1.W),    Label(Level("L"), Level("L")))
    val index     = Input(UInt(8.W),    Label(Level("L"), Level("L")))
    val tag_in    = Input(UInt(19.W),   Label(Level("L"), Level("L")))
    val write_en  = Input(UInt(1.W),    Label(Level("L"), Level("L")))
    val tag_out   = Output(UInt(19.W),  Label(Level("L"), Level("L")))
  })

  val tag0 = Reg(t=Vec(256, UInt(19.W)), lbl=Label(Level("L"), Level("L")))
  val tag1 = Reg(t=Vec(256, UInt(19.W)), lbl=Label(Level("H"), Level("H")))

  when (io.write_en === 1.U) {
    when (io.way === 0.U)       { tag0(io.index) := io.tag_in }
    .otherwise                  { tag1(io.index) := io.tag_in }
  }
}

[dz333]

Affects v0.1 only