On the verification of system-level information flow properties for virtualized execution platforms Academic Article