back to article Brains behind seL4 secure microkernel begin RISC-V chip port

The first RISC-V port of the seL4 microkernel was last week released by the Data61 division of the Australian government's Commonwealth Scientific and Industrial Research Organisation (CSIRO). seL4 is an open-source and highly secure version of the L4 microkernel that aims to be mathematically proven to be bug free, in that it …

  1. John Smith 19 Gold badge
    Holmes

    "If you don't have a complete model of a CPU,..“it's very difficult,.. to analyse the processor.”

    And if the mfg drops in a completely separate "management processor" blob it's completely impossible.

    In fact this seems like the sort of software that such a processor should be running.

  2. Lee D Silver badge

    "In Apple phones, the microkernel forms the basis of the secure enclave that helps secure the device against unauthorised access."

    You mean that one that all the law enforcement agencies are buying the software that lets them into it?

    This is part of the problem - even with a "provably" secure microkernel, you still have to see what it is that you have proven, and quite what that means for taking over or leaking information from the applications themselves.

    Basically, when something is compromised, you can say "Well, it wasn't the microkernel which does almost nothing but pass basic information back and forth, it must be in one of the myriad services which actually contain all the real code that does stuff". Reassuring, I'm sure.

    1. Anonymous Coward
      Anonymous Coward

      Uh, no. They're buying things to bruteforce the passcode. The secure enclave is where fingerprints, credit cards for Apple Pay, etc are stored. They're not breaking into THAT.

    2. Dave 126 Silver badge

      @Leed D

      It is proven, in the same way as a mathematical thereom can be proven. Under its design, a buggy app can't be used to gain further access into the system. Nor are Apple the only customers for SEL4 - DARPA develop with it too:

      https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/

      https://en.m.wikipedia.org/wiki/Formal_verification

      https://en.m.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4

      1. Anonymous Coward
        Anonymous Coward

        It is proven that it does what the specs say

        If the specs leave a security hole, too bad.

        Some security holes are due to weak specs, but most are due to incorrect implementation of specs. You can't solve all the problems, but solving the majority gets you closer to where you want to be.

  3. Anonymous Coward
    Thumb Up

    I thought 'The Secure Enclave' was the name of Zuckerberg's house.

  4. Cem Ayin

    Πόλεμος πάντων μὲν πατήρ ἐστι

    A research group that is really serious about computer security and has been for years is still receiving government funding? And its technology gets (albeit to a limited extent) adopted by mainstream IT industry giants? What's happening? Is the world of computing slowly being turned downside-up?

    Could it be that the New Cold War will bring us reasonably secure computing devices eventually? So Heraclitus was right after all?

    OTOH: Will "reasonably secure computing devices" (if indeed we ever get to see them) mean anything more for Joe End-User than a black box that is even more secretive about its phoning-home activities while being, due to its security features, completely opaque to even advanced computer nerds? It this what e.g. Google is aiming at with Fuchsia? Will the new world of computing be a truely "brave" one?

    1. Arthur the cat Silver badge
      WTF?

      Re: Πόλεμος πάντων μὲν πατήρ ἐστι

      Google Translate claims that title means

      "War of all is a father"

      Jolly good this AI lark.

  5. Anonymous Coward
    Anonymous Coward

    Data61 aka Australian Department of Defence aka suposidly ! secure Sel4

    Sounds like a publicity stunt more than a serious effort.

    Data61 are also joint sponsors of Asia Crypt 2018 later this year with Defence Science and Technology. This all reads as an attempt to cover up the back doors Sel4 and conflicts of interests with the DSGL and DTCA., et, et al

  6. John Savard

    Great News!

    I'm gad this is becoming available for RISC-V, and also glad it's al,most here for x86, which will be more immediately useful for many.

  7. Rajesh Kanungo

    Key management/Crypto operations

    I looked through the ISA and somethings I work with on a regular basis are not there. I guess ISA can be used to implement a secure element? But then, how does it beat a Javacard? The instruction set is too rich for a standard Javacard. Some of the things I do regularly:

    1. Secure keys stores including One Time Programmable key stores

    2. Secure boot

    3. Cryptographic operations

    4. Secure elements for operating on sensitive data with sensitive keys. The moment you pul keys into regular memory you are toast; just freeze the DRAM and read it out. Or rely on a software bug.

    5. Handling large numbers of keys (i.e. a key-chain).

    6. Introduce new cryptographic algorithms.

    7. Optimizing energy consumption/peak performance/speed depending upon use-case.

    Just protecting address spaces hasn't worked: most applications will need to pull keys from somewhere to use them and therein lies the problem.

  8. Anonymous Coward
    Anonymous Coward

    Easy to code too!

    10 Print "Hello, Possums!"

    20 Goto 10

  9. JassMan
    Trollface

    so its ieL4 coming up then?

    That kernel has been tweaked by Apple to meet its needs.

    Given the recent security errors in iOS can we expect seL4 to become ieL4 (insecurity enhanced Linux)? Take a mathematically tested secure system and change it, and every bit you add exponentially increases the risk of creating an insecurity.

  10. Anonymous Coward
    Anonymous Coward

    I wonder

    If Apple wanted to reduce exposure to ISA implementation issues like Meltdown and Spectre, having the secure enclave use RISC-V while the 'real' CPU uses ARM64 might not be a bad idea. And if Apple decided it wanted to use RISC-V for that, throwing a little funding to the "brains behind seL4" for the port would be money well spent.

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