Potential bug/vulnerability

[JorgeMVP]

Potential bug/vulnerability

[lsf37]

I think you might be right, there is nothing in the decode path that says that the VCPU must be currently associated with a TCB, and therefore vcpu->vcpuTCB could be NULL.

That means invokeVCPUInjectIRQ should definitely guard against this case, and write to the VCPU object register instead of doing a remote call when there is no TCB (same as in the unicore case).

I.e. it should be:

exception_t invokeVCPUInjectIRQ(vcpu_t *vcpu, unsigned long index, virq_t virq)
{
    if (likely(ARCH_NODE_STATE(armHSCurVCPU) == vcpu)) {
        set_gic_vcpu_ctrl_lr(index, virq);
#ifdef ENABLE_SMP_SUPPORT
    } else if (vcpu->vcpuTCB != NULL && vcpu->vcpuTCB->tcbAffinity != getCurrentCPUIndex()) {
        doRemoteOp3Arg(IpiRemoteCall_VCPUInjectInterrupt, (word_t)vcpu, index, virq.words[0],      vcpu->vcpuTCB->tcbAffinity);
#endif /* CONFIG_ENABLE_SMP */
    } else {
        vcpu->vgic.lr[index] = virq;
    }

    return EXCEPTION_NONE;
}

Well spotted. Goes to show that the SMP kernel really is not that mature yet esp with HYP features or MCS.

Did you run into a crash with that or did you see it in the code?

[andybui01]

Did you run into a crash with that or did you see it in the code?

Code inspection.

[lsf37]

If it can really trigger a NULL pointer access in the kernel, that would definitely be a major bug, yes. That should not be possible. Since it is the unverified SMP config of the kernel, there is no proof that this doesn't happen and we should definitely investigate.

[Ivan-Velickovic]

A reproducible test is here, Ivan-Velickovic/sel4test@49d1aab (tested with ../init-build.sh -DPLATFORM=odroidc4 -DSMP=1 -DARM_HYP=1).

I believe Jorge's claim is correct.

[JorgeMVP]

@andybui01 also helped to find this one, so we can assign it to him, he can fix it I believe :)

[lsf37]

Fix should be up here now: #1200. Will wait to confirm that the test now passes.