DARPA joins math-secured microkernel race

In a discussion that will sound familiar to Australian readers, US military development agency DARPA wants to create provably-secure software.

According to Threatpost, DARPA director Arati Prabhakar told a Washington Post security conference that embedded systems are among the kinds of applications for which it's feasible to create such OSs.

As the Department of Defense's write-up of the speech, Prabhakar described the project as seeking “a mathematical proof that this particular function can't be hacked from a pathway that wasn't intended. That won't solve the entire problem, but it might make it more manageable.”

The scale of a desktop operating system makes “provably secure” a pretty big stretch goal, but she told the conference that it's feasible “for embedded systems with a modest number of lines of code”.

It's a fair bet that Australia's NICTA will be taking a keen interest in the project. That group developed a provably secure microkernel which it spun off into a company called OK Labs, acquired in 2012 by General Dynamics.

In July of this year, NICTA open-sourced the code for its seL4 microkernel, identifying DARPA among the software's users.

At the WashPo conference, Prabhakar also highlighted the Grand Cyber Challenge DARPA plans for 2016. For that event, she said, DARPA has created a purpose-built operating system: “It’s a separate environment with a new OS. We’re creating a league of their own for machines to fight it out”, she said, with 90 teams already registered to try their hand at the capture-the-flag contest.

The wrinkle is that contestants have to defend networks against high-speed threats without human interaction, because she said DARPA wants “to get to where we can do cybersecurity defence at machine speed”. ®