Virtualisation helps secure mobiles

Now think about mobile devices such as smartphones and mobile internet devices, which are also increasingly used for critical transactions and may conceivably replace PCs as the access device of choice for most web services. These devices are, in many respects, starting to resemble PCs (albeit with a much more convenient form factor). Does this mean that they will be as prone to security exploits, and that we are heading towards full-scale disaster as far as the security of our web services is concerned?

They might well be, if we fail to do something about it. The good news is that the technology that can protect us exists.

Enter mobile virtualisation

The first part is old technology in a new guise -- virtualisation. Originating in the mainframe world of the 1960s, it has recently caused a revolution in the data centre. By partitioning a physical server into several virtual machines, each appearing to software like a real machine clearly separated from all others, the hypervisor (or virtual machine monitor) allows to consolidate multiple (logical) servers onto a single computer. This helps to reduce hardware cost and power bills, without compromising their isolation.

This data-centre scenario does not have much in common with a mobile device, so why is virtualisation of use there?

The key to the answer is a fundamental property of virtualisation: isolation. Because virtualisation partitions a single computing platform into multiple isolated logical machines which appear like physical ones, it implicitly provides firewalls which can be deployed for security purposes. These firewalls are provided by the hypervisor, which, to the software running in each virtual machine (the so-called guest software) appears to be part of the hardware.

Imagine a PC which is used to access online services as we do today, except that whenever the time comes to enter a PIN or password, that PIN is not entered using your PC's keyboard, but a physically-separate device. As long as the remote server can ascertain that the PIN entry comes directly from the separate device (for example, through a secure network link), and that the device is itself tamper-proof, the transaction can be secured even if the PC is infected with every virus under the sun. (Ok, I'm simplifying things a bit here - there still needs to be some secure visual feedback on what you're actually authorising - but I think you get the picture...)

Sounds fine, if a bit cumbersome, but not suitable for a mobile device. The last thing you want is to carry a separate pin-entry device with you, right?

This is exactly where virtualisation comes in: we can simulate this detached PIN-entry device by putting it into a separate virtual machine. The normal phone software runs in its own virtual machine (or more likely several). The hypervisor ensures that the security-critical PIN-entry functionality is completely protected from any (potentially compromised) software running in other virtual machines. Again, you'll notice that I'm simplifying: the hypervisor also needs to ensure that the access to the actual (hard or soft) keyboard, and any visual feedback, are secure, but I hope you get the basic idea.

So, what about the hypervisor itself? Why won't it become compromised.

Hypervisor security

Good question, particularly if you think of enterprise-style hypervisors. These are big systems, including the (security-critical) management components that consist of hundreds of thousands, or even millions, lines of code. Experience tells us that even well-engineered software averages several bugs per thousand lines of code (kLoC), so these hypervisors can be expected to contain thousands of bugs. Some fraction of those will be relevant to security, creating vulnerabilities that can be exploited by hackers.

So, the key to security is size: small is beautiful. This is one reason (of several) why a well-designed hypervisor for mobile use is very small. By adapting it to the specific requirements of mobile systems (and the similar requirements of other consumer-electronics devices), and a careful design and implementation which focuses on providing the minimum set of primitives, a total code size of around 10 kLoC is achievable, as in the market-leading OKL4 hypervisor from Open Kernel Labs. Due to its minimalist design, and design principles inherited from operating-system microkernels, such a small hypervisor is called a microvisor.

Even with traditional software-engineering methods, the number of bugs in such a small code base can be reduced to a few handfuls. And, with luck, none of them will constitute security vulnerabilities. This is helped by stability: once you have a well-designed hypervisor that supports a small set of primitives well-matched to its application domain, there is little need to change it. And certainly there is no need to change it once it has been deployed on the device, as the user-visible device functionality does not depend on it.

By now you're probably thinking I'm trying to get myself out a corner. Clearly, the argument that the hypervisor cannot be compromised is more than a bit hand-wavy so far.

Enter formal verification

In fact, this is no longer the case. This is the bottom line of a landmark result recently achieved at NICTA, Australia's national Centre of Excellence for ICT Research. The NICTA researchers announced the successful formal verification of their seL4 microkernel, a kernel that shares its ancestry with OKL4 (so the two systems have a lot in common).

What is formal verification? It means establishing the properties of systems with mathematical methods (and rigour). But even that needs further explanation, as different people use the term in different ways.

Static-analysis tools are frequently used to detect bugs in programs. The more sophisticated ones use formal methods to determine the presence (or absence) of certain properties in the code. The formal methods behind such approaches fall into a category called model-checking. While model-checking approaches can be extremely useful for eliminating bugs in programs, including very large ones, their scope is inherently limited to checking relatively simple and well-defined properties. As such they can identify bugs from a narrow class.

The kind of formal verification the NICTA researchers are using is called a refinement proof. It shows, in a very strict sense, a correspondence between a high-level and a low-level representation of a system. More precisely, it proves (with mathematical rigour) that all the possible behaviours of the low-level representation are completely captured (that is, permitted) by the high-level representation. For high-level representation think of the functional description (that is, the application programming interface) of the kernel, formulated in a mathematical language. For the low-level representation think of the actual kernel implementation.

Refinement proofs have been performed on some (very small) operating-system kernels before. There are two facts that are new and exciting about the verification of seL4.

The first is that the low-level representation of the kernel is the actual source code of seL4, written in the C language. Past successful verification projects stopped at an (albeit low-level) model of the kernel. This still requires an informal (therefore non-rigorous and inexact) step of arguing the correspondence between the model and the actual code.

The second fact is that seL4 is a general-purpose platform, which enables developers to build arbitrary systems on top. For example, seL4 can serve as a hypervisor, and is able to run Linux in a virtual machine, and does so at essentially the same performance as the industry-leading OKL4 hypervisor. So, seL4 is not a toy or an academic exercise, but suitable for use in the real world.

Together these attributes make seL4 the world's first general-purpose operating-system kernel, or hypervisor, that has been formally verified down to the actual source code.

Implications

We now have a rock-solid foundation on which to build secure systems. A formally verified hypervisor can be truly considered an extension of the hardware - it is as reliable and secure as the underlying hardware. It can therefore isolate virtual machines as securely as if they were running on separate hardware, exactly what is needed for security.

We now have the building blocks to make mobile devices secure, and avoid repeating the mistakes of the past. Mobile devices will evolve to take on more of the functionality we know from PCs, but we can make it happen without the distasteful side effects.

About the author:

A pioneer in the field of operating systems with over two decades of experience, Dr Gernot Heiser co-founded Open Kernel Labs and serves as the chief technology officer. As the company’s key technologist, Heiser sets the direction of the company's research and development efforts to maintain OK Labs leadership position in mobile virtualisation and embedded systems software development.

Before co-founding OK Labs, Heiser created and led the Embedded Real-Time Operating Systems (ERTOS) research group at NICTA, Australia’s Information and Communications Technology Centre of Excellence. With his help, NICTA has become recognised as a world leader in embedded operating systems technology.

As a full-time faculty member at the University of New South Wales (UNSW), Heiser designed a suite of world-class OS courses, led the development of several research operating systems and founded the group that provided the basis for NICTA's OS group and eventually, OK Labs. He was recently awarded the prestigious John Lions Chair of Operating Systems at UNSW, where he continues to teach advanced-level courses and supervise Ph.D students.

Related forum discussions

	To start a discussion topic about this article, please log in or register.