Verifying Trustworthiness of Virtual Appliances in Collaborative Environments

Abstract

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.