Gernot Heiser, one of the main brains behind the extremely hard to hack seL4 microkernel, is set to leave Australia for Germany to work in a cyber security startup.
SeL4 was developed at the old NICTA federally funded digital research organisation, before NICTA was swallowed by the CSIRO and rebadged as Data61.
The SeL4 microkernel allows ironclad separation between software systems so that hackers cannot dive into the critical innards of an operating system by entering through a poorly protected hatchway.
What makes seL4 a showstopper in the security world, is that its structures have been mathematically verified.
The seL4 software has applications in everything from hack proofing industrial controllers to fencing off the virtual machines sitting inside cloud computing clusters, and Professor Heiser will join a startup called Secure Elements that will develop commercial applications based on the open source seL4.
In tech jargon, a secure element is a tamper resistant hardware platform that can securely host applications and store confidential and cryptographic data.
“It’s a company building security solutions for embedded systems based on seL4,” said Professor Heiser who led the Software Systems Research Group at NICTA that developed the seL4 microkernel.
Being based in Germany puts Professor Heiser and his startup at the centre of European industry and research. Germany has a vast pool of aerospace, automotive and industrial ventures requiring the sort of hardened digital security that seL4-based applications could provide.
Professor Heiser will be moving into a familiar research and collaboration neighbourhood. In the past he has collaborated with many of Germany’s top research institutions including Dresden University of Technology, the Max Planck Institute for Software Systems and the University of Karlsruhe.
He said Secure Elements was not associated with any of the German research institutions but included people who had come out of research institutions as well as private industry. German company registration documents list Secure Elements Gmbh as based in Munich with 25,000 euro in share capital and a Klaus Winter as CEO.
Professor Heiser does not yet have a date set in stone for the move. ‘It’s a bit up in the air but if it happens, it will be some time this year,” he said.
“It’s not operational, it’s working on attracting funding, we are not developing anything yet, but we have very clear plans on what to do.”
“We are in negotiations with potential investors so it could happen very quickly,” Professor Heiser said of the move.
Secure Elements is not a spin-off from Data61, but Professor Heiser, who is currently a researcher at Data61, said there was likely to be collaboration with Data61 on some projects. He said he was the only Data61 person involved with Secure Elements.
Professor Heiser was one of the original employees at the old NICTA concern. He joined during NICTA’s inception in 2002, while remaining on the academic staff of the UNSW, which he joined in 1991.
He is no stranger to startups. In 2006 Professor Heiser co-founded Open Kernel Labs, a company dedicated to commercialising the predecessor to seL4. He was on OK’s board until the company was acquired by General Dynamics in 2012.
SeL4 is well known in international system security circles. The US Defence Advanced Research Projects Agency’s (DARPA) is using sel4 in its research project to hack proof the systems in autonomous fighting vehicle like drones.
Known as HACMS or High-Assurance Cyber Military Systems, the DARPA program has already tested sel4 in the wild, allowing hackers to try and do their worst on a pilotless Little Bird helicopter flying over a military range last year. The hackers had no joy in trying to take over the helicopter.