Hola.
Está muy bien tu pregunta/comentario.
En el paper consideramos que el espacio (las direcciones virtuales) accesibles por los OSs es global. En tal sentido, el predicado va_accesible refiere a si va es accesible por "algún" OS. La idea en la precondición del read (con dicho predicado) es decir que un OS no puede leer direcciones de memoria que están reservadas para el hypervisor.
Saludos, Carlos