The most widely deployed mobile virtualization solution
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. We assume correctness of compiler, assembly code, and hardware, and we used a unique design approach that fuses formal and operating systems techniques. To our knowledge, this is the first formal proof of functional correctness of a complete, general-purpose operating-system kernel. Functional correctness means here that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as the kernel will never crash, and it will never perform an unsafe operation. It also proves much more: we can predict precisely how the kernel will behave in every possible situation.
seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels.
The Hacker's Guide for smartphone attacks
Defense-Grade Security for the Rest of Us
Build Secure Smartphones for the Enterprise
Learn How to Build a More Secure Smartphone
Build Mass-Market Smartphones with Mobile Virtualization
SecureIT Mobile Government White Paper (Chinese Version)
SecureIT Mobile Enterprise (Chinese Version)
Build a Smartphone for the Mass-Market (Korean Version)
The NirvanaPhone Concept Specification and Reference Architeture
Motorola Evoke Teardown
seL4: Formal Verification of an OS Kernel
Automatic Device Driver Synthesis with Termite
The Motorola Evoke QA4 - A Case Study in Mobile Virtualization
Android Migration at the Speed of Light
Virtualization and Componentization in Embedded Systems
Virtualization for Embedded Systems
Role of Virtualization in Embedded Systems
Your System is Secure? Prove it!
Towards Trustworthy Computing Systems: Taking Microkernels to the Next Level
Secure Embedded Systems Need Microkernels