[seL4] Running vm_multi on TK1 and TX2