VerSeCloud: The Path to a Trustworthy, Secure Cloud

What does a secure, trustworthy and also future-proof cloud look like? The aim of the research project VerSeCloud is to provide a solution. Using a microkernel, formal methods of proof, and strictly implemented separation between customer applications, the consortium partners – Kernkonzept GmbH, genua GmbH, the University of Potsdam and the Technical University of Munich – are developing the foundations for a highly secure cloud infrastructure.

by Nicolas Frinker, software engineer at genua

Virtualization as the basis for cloud solutions has become a key element in today's IT infrastructure. The associated abstraction of existing physical resources into a virtual environment allows these resources to be used in a flexible, scalable and cost-effective way.

However, sensitive data and applications require a high level of data security and trustworthiness, which cannot be provided by currently available virtualization solutions: Owing to their underlying operating systems, current solutions are complex and extensive and, as a result, it is extremely difficult to check that they provide reliable security. Approval or certification is therefore only feasible at great effort and expense.

In the VerSeCloud research project, we together with our project partners (Kernkonzept GmbH from Dresden, the University of Potsdam and the Technical University of Munich) are working on a future-proof, reliable and secure virtualization solution also intended for security-critical cloud applications.

Cloud Applications: Streamlined And Verifiable

Based on the L4Re microkernel, we are developing a performant (thanks to Intel Vt-x) and flexible hypervisor which can run Linux and OpenBSD without modification. Using nested virtualization, it is also possible to run other operating systems such as MS Windows. As a result of the microkernel basis, the code base remains streamlined and verifiable. The L4Re microkernel, which runs with system rights, is only responsible for the most fundamental tasks such as separation of the applications. All other tasks are outsourced and performed only with restricted access rights. With this architecture, the security-relevant components remain streamlined and verifiable and are therefore also suitable for more in-depth reviews, e.g., in an approval process.

In addition to the solid and secure technical basis, formal methods to mathematically verify security features of the microkernel and drivers are also used in the VerSeCloud research project. An abstract model of the L4Re microkernel is used to define an expected condition and an extremely large number of automatically generated tests is then used to compare the expected condition with the actual condition in the implementation. For the drivers, network drivers in particular are examined in greater detail, and common features are determined and transferred to the proof assistant Coq. There, their correctness can be proved and code synthesized, which can then substitute parts of the driver with evidentially correct code. This approach using formal methods increases security significantly.

Four Questions to Nicolas Frinker

Are comprehensive IT security and data protection in a cloud environment where data is accessed using many different devices including mobile devices, actually possible?

Nicolas Frinker: IT security and data protection in a cloud environment depend on two factors: the provider and the used technology and software. The used technology must ensure that customers in the cloud environment are separated from each other securely and reliably. In turn, the trustworthy provider must ensure that this technology is used consistently. If both requirements are met, customer applications and data are well protected.

What would be potential application scenarios?

Nicolas Frinker: Today's large-scale cloud providers are mostly located in the USA and do not necessarily command the trust of many German companies. These companies therefore lack a trustworthy provider and, in addition, the used software draws attention repeatedly due to security problems.

To fill the gap left by the missing, trustworthy cloud providers, many companies resort to self-hosted clouds, so-called private clouds. Here, the datacenter is installed in the company's own basement and is used exclusively by the company, so that software-based separation of multiple customers is no longer necessary. This solution is therefore secure, but at the same time the essential benefits of a public cloud, such as scalability and cost-efficiency, are lost.

Here, VerSeCloud can provide the basis for a promising future: A cloud environment based on the software researched in VerSeCloud with its formally proven security features offers the necessary secure and technical basis on which multiple customers can share the same cloud environment without having to worry about their separation from other customers. If this software is then also operated by a trustworthy cloud provider, cost-effective and scalable security and data protection are possible!

How is the project divided up within the team?

Nicolas Frinker: Basically, Kernkonzept and genua are jointly researching improvement of the new hypervisor, while Kernkonzept together with the University of Potsdam is endeavoring to evidence security features by means of formal verification. My main task is to make OpenBSD, as a further guest system in addition to Linux, runnable on the new hypervisor.

What progress has so far been made?

Nicolas Frinker: The new hypervisor is now properly matured and can run Linux and OpenBSD as guest systems. There has been plenty of progress on the formal methods front too: For example, a complete, simple driver for L4Re has been synthesized from the proof assistant Coq.