Featured image above: Gernot Heiser. Credit: Quentin Jones
We trust computer systems every day – but trusted systems are rarely entirely trustworthy. Laptops can crash, servers can freeze, and personal details can be stolen. Even pacemakers can be hacked.
“The complexity of the systems we’re building has grown much faster than our ability to deal with it,” says Gernot Heiser, a professor of operating systems at UNSW and chief research scientist at Australia’s digital research network, Data61, a division of the national science agency CSIRO. “The result is an appalling lack of dependability.
“As critical tasks like controlling medical devices, mobile phones, industrial plants and airplanes become ever more technology-dependent, trust should not be taken for granted,” he adds.
Is it even possible to write truly trustworthy code? Heiser thinks so – which is why he has spent the past decade developing secure microkernels, the core on which dependable operating systems can be built. By itself, a microkernel does not provide useful services, but contains the core mechanisms on which to build them.
Working with UNSW colleagues Gerwin Klein and Kevin Elphinstone, Heiser sparked excitement among experts when the team proved that all 7,500 lines of C code in his seL4 microkernel were mathematically correct. May not sound like much, but this is incredibly difficult to achieve.
“It is hard to comment on this achievement without resorting to clichés,” quipped Lawrence Paulson, a noted leader in theorem proving and a professor of computational logic at the University of Cambridge.
June Andronick, a principal research scientist at Data 61, who specialises in the verifiability of software systems, adds: “What Heiser and his team have done, and keep doing, is to strengthen the guarantees that can be provided about software by orders of magnitude, while maintaining very good performance for real-world use.”
A big test of Heiser’s seL4 microkernel came in 2015, when the US Defense Advanced Research Projects Agency gave hackers unfettered access to the on-board computer of an autonomous Boeing AH-6 helicopter gunship. Their task was to hijack the microkernel and take control. While hackers easily commandeered the helicopter when it hosted other software, they could not crack the on-board computer when it ran on seL4 .
A predecessor of the secure seL4 software – known as OKL4 – may already be in your pocket. Heiser set up Open Kernel Labs in 2006 to commercialise his OKL4 microkernel. The company was later bought by General Dynamics, after which “our technology ended up in the pockets of billions of consumers,” says Heiser. OKL4 is now on the security processor of all Apple iOS devices.
But there are still important weaknesses. “Observing exact timings of actions can leak secrets, via so-called ‘timing side channels’, giving attackers the ability to eavesdrop on communication or even masquerade their malicious code as legit services,” says Heiser. His team is now working to prevent such failures by blocking any given process from unduly influencing the execution speed of another process – and eventually proving that this works.
The second weakness is price. The development cost of the seL4 microkernel was about three times that of comparable unverified, vulnerable software. But Heiser thinks he can make the software affordable for everyone.
“If we manage to eliminate this factor-three cost gap to standard software, we’re totally changing the world of software systems.”
– Ben Skuse
For more stories at the forefront of engineering research, check out Ingenuity magazine.