Provably correct code and methodology offer mobile OEMs and ecosystem partners security and reliability in critical applications
Chicago – August 13, 2009 – Open Kernel Labs (OK Labs), the leading global provider of embedded virtualization software for mobile phones and broadband Internet devices, today announced completion of long-term research and development to provide formal mathematical proof of the correctness of the microkernel technology underlying OKL4, the company’s mobile virtualization platform. This groundbreaking project involved NICTA, the company’s incubator and investor, OK Labs staff, researchers from the University of New South Wales (UNSW), and other prestigious institutions. Moreover, as commercialization partner for NICTA, OK Labs will bring the results of the project to market in future generations of mobile virtualization products.
The project centered on the need to assure extremely high levels of reliability and security in mission-critical domains that include aerospace and transportation. By mathematically proving the correctness of underlying kernel functioning, NICTA and OK Labs pave the way for validating and deploying mobile virtualization under certification and security regimes like Common Criteria for business-critical applications in mobile telephony, business intelligence, and mobile financial transactions.
This is an important result for trusted computing both in the mobile space and elsewhere. I caught up with Prof Gernot Heiser yesterday at the NICTA (http://nicta.com.au) Techfest (http://nicta.com.au/nicta_events/techfest2009) and he and the rest of the team were very excited. With the combination of OK Labs (http://www.ok-labs.com/) existing work in building the OKL4 kernel into mobile phones world wide, the interest from the security conscious space, and some other work shown on automated generation of device drivers from driver and OS specifications, OK Labs faces a very bright future. (NICTA press release: http://nicta.com.au/news/home_page_content_listing/world-first_research_break…
Citrix Labs is working with OK Labs on bringing XenClient-like (http://www.citrix.com/English/ps2/products/feature.asp?contentID=1685500) functionality to the mobile phone. That is, the combination of the Citrix Receiver, with completely separate Android images for work and home on a single device. (OK Labs relationship: http://community.citrix.com/blogs/citrite/michaelha/2009/07/28/Citrix+Receive… http://www.citrix.com/English/ne/news/news_print_p.asp?newsID=1690174)
I’ve known Gernot since my time as student/researcher/lecturer at the University of NSW (http://www.cse.unsw.edu.au).