Often in collaborative research environments that are facilitated through virtual infrastructures, there are requirements for sharing virtual appliances and verifying their trustworthiness. Many researchers assume that virtual appliances — shared between known virtual organisations — are naturally safe to use. However, even if we assume that neither of the sharing parties are malicious, these virtual appliances could still be mis-configured (in terms of both security and experiment requirements) or have out-of-date software installed.
Based on formal methods, we propose a flexible method for specifying such security and software requirements, and verifying the virtual appliance events (captured through logs) against these requirements. The event logs are transformed into a process model that is checked against a pre-defined whitelist — a repository of formal specifications. Verification results indicate whether or not there is any breach of the requirements and if there is a breach, the exact steps leading to it are made explicit.