-
The most widely deployed mobile virtualization solution
Data Sheets
White Papers and Publications
Defense-Grade Security for the Rest of Us
By Carl Nerup
This White Paper lays out a vision for a High Assurance Framework (HAF) for building trusted computing and communications systems, using Commercial Off-The-Shelf (COTS) hardware and software components, including Free and Open Source Software (FOSS).
It reviews the origins of requirements for High Assurance for mobile devices, describes the required components, and outlines the architecture to implement and deploy to devices using readily-available commercial software technology.
Build Secure Smartphones for the Enterprise
By Rob McCammon
SecureIT Mobile Enterprise, a software and services solution, enables “out of the box” support for personal applications, services, and data to be complemented by a managed, secure environment for business-critical enterprise applications, services, and data. SecureIT Mobile Enterprise allows the full capability of a personal mobile device and the full capability of an Enterprise mobile device to coexist on the same hardware, replacing two devices with one without compromising functionality or freedom.
Supporting both open personal and trusted enterprise domains on a single physical device, SecureIT Mobile Enterprise reconciles the needs of the individual and the enterprise.
Learn How to Build a More Secure Smartphone
By Rob McCammon
SecureIT Mobile Government is the way to build and deploy secure communications for agency CIO's, corporate IT, government contractors, integrators, OEMs, and mobile network operators — using OKL4 mobile virtualization with COTS hardware and software.
Build Mass-Market Smartphones with Mobile Virtualization
By Rob McCammon
Open Kernel Labs, together with leading mobile OEMs and operators, is first to market with a mass-market smartphone solution proven to deliver a rich user experience at substantially reduced cost
SecureIT Mobile Government White Paper (Chinese Version)
技术白皮书
SecureIT Mobile
利用移动虚拟化和其他商业成品技术，构建一款更加安全的智能手机
针对安全应用和安全通信
Energy Management
By Gernot Heiser
In this white paper we focus on the systems software, and how it can use mechanisms supplied by the hardware in order to manage a device’s energy consumption.
Build a Smartphone for the Mass-Market (Korean Version)
Mass-Market Smartphone이란 현잧 스마트폮이 읷부 비즈니스맨이나 얼리어답터 사이에서 사용되고 있다면, 현잧의 피쳐폮과 같이 부담 없는 비용으로 구입할 수 있고 스마트폮에서 제공하는 다양한 서비스와 어플리케이션을 이용할 수 있게 하여 읷반 대중에게 확산되어 사용될 수 있는 스마트폮 솔루션을 의미한다.
오늘날 스마트폮은 글로벌 모바읷 에코시스템(the global mobile ecosystem)을 이끌어 가고 있다. Gartner에 따르면, 젂체 모바읷 폮 춗하는 2009년 젂체 12억대 중 스마트폮은 1억 7240만대로 2008년 대비 23.8% 상승했고, 게다가 2014년까지 스마트폮의 춗하량은 매년 24% 증가할 것으로 예측하고 있다.
스마트폮은 망사업자들, 모바읷 폮 제조업자들, 모바읷 칩셋 공급자들 그리고 모바읷 유저들을 타겟으로 하는 서비스의 중요한 자산이다. 또한 젂체적으로 개발자들과 사업자들에게도 큰 매력을 느끼게 하는 스마트폮 OS의 풍부한 오픈 어플리케이션 플랫폼들은 새로운 범주의 어플리케이션과 서비스들을 가능하여 새로운 시장 창춗과 고부가가치의 실현을 가능하게 한다.
The NirvanaPhone Concept Specification and Reference Architeture
By Open Kernel Labs and Citrix
The objective of the Nirvana Phone is to enable a user to more fully leverage their Smartphone as their primary computing device, and enable the connection to common larger form factor peripherals such as full screen monitors, mice, and keyboards.
Motorola Evoke Teardown
By William Weinberg
This white paper examines the economic impact of virtualization as a core component of mobile handset design. In particular, it offers readers a “teardown” of key device components (hardware and software) and analyzes how mobile virtualization reduces costs on the Bill of Materials. It also identifies incremental benefits from embedding virtualization in mobile devices, including performance and power management, as paths to both cost reduction and differentiation in a dynamic marketplace.
seL4: Formal Verification of an OS Kernel
By Gerwin Klein, Kevin Elphinstone, Gernot Heiser, et al.
Complete formal verification is the only known way to guarantee that a system is free of programming errors. We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation.
Automatic Device Driver Synthesis with Termite
By NICTA, The University of New South Wales, and Open Kernel Labs
Faulty device drivers cause significant damage through down time and data loss.
We present a concrete driver synthesis approach and tool called Termite. We discuss the methodology, the technical and practical limitations of driver synthesis, and provide an evaluation of non-trivial drivers for Linux, generated using our tool. We show that the performance of the generated drivers is on par with the equivalent manually developed drivers. Furthermore, we demonstrate that device specifications can be reused across different operating systems by generating a driver for FreeBSD from the same specification as used for.
The Motorola Evoke QA4 - A Case Study in Mobile Virtualization
By Gernot Heiser
In this white paper we will take a closer look at the Evoke. We will see how it demonstrates some of the power of virtualization. Moreover, we will see how the Evoke benefits from the unique aspects of the technology provided by OK Labs, which enables designs not supported by plain hypervisors.
Android Migration at the Speed of Light
By Josh Matthews
The advantages of the Android OS are many. This paper looks at the OKL4 Microvisor and shows how Android works in a virtualized environment, explains how this simplifies the migration task, and describes some specific examples of its application.
Virtualization and Componentization in Embedded Systems
By Josh Matthews
This paper reviews how a microkernel-based hypervisor providing virtualization and componentization supports an evolution to a more fault resilient, secure, and easily maintained software architecture and implementation.
Virtualization for Embedded Systems
By Gernot Heiser
This white paper presents an introduction to virtualization technology in general, and specifically discusses its application to embedded systems.
Role of Virtualization in Embedded Systems
By Gernot Heiser
Starting from a comparison of key characteristics of enterprise systems and embedded systems, the difference in motivation for the use of system virtual machines, and the resulting differences in the requirements for the technology. We argue that high-performance microkernels, specifically L4, are a technology that provides a good match for the requirements of next-generation embedded systems.
Your System is Secure? Prove it!
By Gernot Heiser
Computer security is an old problem which has lost none of its relevance - as is evidenced by the annual Security issue of login. The systems research community has increased its attention to security issues in recent years, as can be seen by an increasing number of security-related papers published in the mainstream systems conferences SOSP, OSDI, and USENIX. However, the focus is primarily on desktop and server systems.
Towards Trustworthy Computing Systems: Taking Microkernels to the Next Level
By Gernot Heiser
This paper argues that microkernels are the best approach for delivering truly trustworthy computer systems in the foreseeable future. It presents the NICTA operating-systems research vision, centred around the L4 microkernel and based on four core projects. The seL4 project is designing an improved API for a secure microkernel, L4.verified will produce a full, formal verification of the microkernel. Through close collaboration with Open Kernel Labs (a NICTA spinoff) the research output of these projects will make its way into products over the next few years.
Secure Embedded Systems Need Microkernels
By Gernot Heiser
The immense popularity of all sorts of electronic devices means that they have become an integral part of our lives; it is becoming difficult to imagine living without them. In the process, they are increasingly trusted with sensitive data, the loss of which can cause serious distress or financial harm. Security is therefore becoming a significant issue.
Yet, as we know from the PC world, commodity computer systems are not well-defended against security threats. In this article we examine the security threats facing embedded systems, and what needs to be done to make them secure.