back to article 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 …

  1. Mark 85

    Lofty goal(s)

    I hope that someone can hit it. The bigger question is will the whole thing be sabotaged or backdoored by one of the snooping organizations. Or maybe it's to prove it can't be done?

  2. Neoc

    Weasel wording?

    "...can't be hacked from a pathway that wasn't intended".

    ...but kindly leave alone the security holes that were intentionally placed by various TLA agencies.

    1. Destroy All Monsters Silver badge
      Pint

      Re: Weasel wording?

      Speaking of TLA, we have recommended reading in Leslie Lamport's "Specifying Systems - The TLA+ Language and Tools for Hardware and Software Engineers". Downloadable legally, too.

      Do it now.

  3. Peter Brooks 1

    This would be a good open-source project

    An Ada microkernel - the long-awaited APSE (Ada Programming Support Environment) could be built on it.

    If it was designed and coded well, it could be used under Unix - eventually you could replace the c-based UNIX with a superior (faster as well as more secure) Ada OS. If you start with the microkernel then, over time, you can re-code the other parts, leaving things like the user GUI until last.

  4. Christian Berger

    There are a lot of such projects

    Probably the most promising ones try to make proving code easier. Essentially you have your code as well as abstract conditions next to it. You can have conditions like "integer power of 2" and the compiler will make sure they are satisfied. This can detect certain classes of bugs and therefore potentially eliminate them. Essentially it would mean you'd have to program around additional compiler errors which would make your code more secure.

    However we are talking about military projects here. Those are closed source projects often written in C++. Considering there are perhaps 20 people out there who actually fully understand C++, and C++ is a minefield of complexity, this is perhaps not the best language to write secure systems in.

    1. Anonymous Coward
      Anonymous Coward

      Re: There are a lot of such projects

      The problem with that is the same with a lot of 'new language' ideas, it assumes the orginal coder has correct logic in the first place.

      Now I'm not knocking the use of languages that enforce proper memory management/bounds checking, etc, but out side of a few special cases like a microkernel I don't see "maths assisted" coding helping much.

      Most security flaws come from bad/carless ideas and inadequate testing due to budget/marketing pressure. The language is just a choice of which type of gun to shoot one's foot with...

  5. Chris Miller

    Good luck with that

    But even if it were possible to create provably secure software (ah hae ma doots), all you'd need then would be provably secure hardware to run it on and provably secure people to operate it. As Bruce Schneier points out:

    the mathematics are impeccable, the computers are vincible, the networks are lousy, and the people are abysmal. - Secrets and Lies: Digital Security in a Networked World

    1. Adam 1

      Re: Good luck with that

      Plus provably secure compiler. Even this can only secure against software bugs (buffer overruns etc). What about side channel attacks? The area of the various chips that heat up effectively leaks information too.

  6. jzlondon

    Maths. Not math.

    <shudder>

  7. DropBear

    ...DARPA wants “to get to where we can do cybersecurity defence at machine speed”

    So this is how Black ICE first emerges, then (well, minus the black part - for now)...?

  8. gerryg

    micro v macro

    Has the discussion on reliable OSes moved on from Tanenbaum-Torvalds debate?

    For me it seems that it's all about risk - you throw it over the fence and hope it doesn't come back to bite you (micro) or you attempt to contain it and avoid getting bitten (macro). Neither approach eliminates the problem

  9. jzlondon

    Easiest way to compromise a network? Bribe a sysadmin.

    Job done.

    1. Martin Budden Silver badge
      Joke

      Easiest way to bribe a sysadmin?

      Has to be either sex or shiny new kit. Probably shiny new kit.

  10. NP-Hardass

    Just a reminder...

    IIRC, NICTA announced that their 'provably secure' microkernel, seL4 was not mathematically proven secure when DMA is used. seL4 is a great achievement, but there is still a long way to go.

  11. Anonymous Coward
    Anonymous Coward

    That assumes there aren't hardware bugs in the CPU. On a modern CPU the list of bugs is always rather long.

POST COMMENT House rules

Not a member of The Register? Create a new account here.

  • Enter your comment

  • Add an icon

Anonymous cowards cannot choose their icon

Other stories you might like