seL4 Secure Micro kernel

"A nippy microkernel mathematically proven to be bug free*, and used to protect drones from hacking, will be released as open source tomorrow."

Has anyone heard about or seen this? How applicable is this to the Pixhawk, Pi or BeagleBone flight controller efforts? The best bit is that it seems to assure that all user mode code execution is isolated from the Kernel in such a way as to prevent crashing the kernel. I don't think this actually prevents bad FC code but it sounds like it could be a step in the right direction surely.

Without reading too much into this I did note that in the video they seem to say that the software "detects" malicious groundstations by monitoring for those that attempt to authenticate with the wrong password too many times. They also said that the GCS link was encrypted. I think what they actually mean is that their software overlays encryption to MAV connections and the FC detects attempts to communicate over unencrypted links. I'd hate for this to be another WEP style weak cipher that encrypts with a shared key or worse still some kind of authenticated SSL style link using a password based challenge response in each conversation

More details here

E-mail me when people leave their comments –

You need to be a member of diydrones to add comments!

Join diydrones


  • Developer

    When "drones" becomes sanctioned and the sky is filled with Amazon deliveries, then remote attacks becomes a very real threat.

    But at the moment it is a case of diminishing returns. Meaning there are probably hundreds of more basic issues that should be address first, having a higher impact on making the average system more robust and safe for most users.

  • Agree with Chris Norris, NICTA seems to be an attempt to protect against Kernel attacks and maybe a set of User space tools to react. Any other kind of attack remains being a threat.

  • Moderator

    "But if a hacker can logon in the FC then you probably have lost the game anyway." - Agreed but that isn't what we're talking about or even what this protects against. It's about isolation of code execution and memory. 

    The actual GPS signal itself is well documented and given that hobbyists can build their own GPS receivers from scratch ( it isn't an overly large leap to assume that a transmitter is possible. The RC gear is probably even more susceptible as there are already plenty of open source transmitters available. 

    All of that aside bugs can exist in any part of the code that can accidentally lead to crashes, if this kernel can protect itself from this it could be used to build a more robust overall system. My RC and GPS example was really just taking the scenario to extremes 

  • But if a hacker can logon in the FC then you probably have lost the game anyway.

    To insert code over analog RC link or through a manipulated GPS signal ... is difficult. Nothing that the average hacker will do. It requires advanced knowledge of the radio building. The hackers probably have to build its own transmitters for GPS or analog RC.

    Build a transmitter for GPS??? While we're in the area of terrorism ... you can also get the drone to crash by hitting the pilot in the head with a brick. But that applies both ways. We're talking about a radio signal with a range of 50 - 200m. So if my drone gets hacked, never mind about the drone, I will beat the hacker in the head with a brick ... and hand him over to the police.

  • Excellent point @Chris - as time goes on attacks become more sophisticated and I can imagine injecting a NMEA string into GPS switching it from Text to Binary mode or something that causes loss of GPS. Better isolation between threads/processes will help with those.

  • Moderator

    I think where this project stands out is the protection of the kernel and code execution in user space. Most hacks that we hear of involve hijacking one process and causing it to crash or break in such a way as to permit the hijacker to write to a protected area of kernel memory and inject their own process/over write an existing process' memory. If this product really can guarantee protection of the kernel and kernel memory and the kernel can monitor processes for abnormal behavior then this is really quite clever. 

    Encrypted links are definitely a good start but I don't think that encryption is the only solution and removing the links isn't a solution either. For instance taking Scott's example above - where the car is compromised via hijacking of code running on the radio and therefore (I guess) finding a way to write out to the CAN bus. Imagine someone determines there is a bug in the GPS handling or RC handling of a flight controller that allows them to arbitrarily run their own code. If the Kernel monitors abnormal execution behavior by (for example) protecting memory access by preventing writes by threads/processes that the memory wasn't allocated to that in itself would be a huge leap ahead of where we are now. 

  • Encrypted data links are the next thing we should be working more on. There is some work in that space already. We can't stop jamming altogether, but then the Pixhawk can respond appropriately (RTL etc). The examples given such as Pacemaker problem is all about communication links, not the kernel.

    That said however, the attacks I have seen done on cars was done through the Stereo - no idea of the deeper details, but in that case it is more likely to be problems with the components talking - and those sort of spaces could benefit from better design.

    Recently I worked on a project which had a lot of encrypting, an amazing amount of security at the hosting end, firewalls, tripwires, encrypted database connections, audited code, etc - and a test in one day from an intrusion person found a hole giving them shell access through one tiny bit of code. No matter how hardened the kernel is, it only take one weakness to open connection.

    Think about the more obvious things - we could have a lovely hardened kernel, which didn't allow any motor control. But we allowed ground station links to program waypoint - including altitude. So now we don't need to disable motors remotely, we can just drive it into the ground. Control of these links - from inadvertent (the radio in the car), to by design (ground control) is the place we need to concentrate on.

  • OK... thank you very muchVery kind of you!

    I really do not understand what this is supposed to be good for. Hackers are not magic, it's not Gandalf with his magical wand that writes magical code.

    - If the drone has a communication link, the communication link needs to be protected (if you believe that there is a hacking risk).

    - If the drone does NOT have a communications link, it can NOT be hacked via the non-existent communication link (but it can still crash in other way).

    - If a hacker can communicate with the drone ... well, then he can add the next waypoint to the North Pole. Works just as good as killing the FC program!

    I do not know how many drones that actually has a core. APM has, what I know, not one. Exactly what you gain in having a core in the extremely critical FC management? An academic gold star in the teacher attendance book? For all the love of god, do not let the FC manage your personal website... or Skype, or Outlook.

    A larger drones probably have an hardened version of Linux ... and yes ... it's pretty safe... already.

    Then again, it's probably easier to just shoot down a small drone with a 50 buck shotgun ... and a big drone with a 100 buck hunting rifle ... than let 100 hackers work for months to find a back door in the wireless protocol.

    and the police have an easier option, saying: - "Land or go to jail."

  • MR60

    It won't be long before NSA will get its backdoors enforced (by force, they have ways) in whatever HW/SW of this microkernel....

    Now I put my tin hat on for the rest of the day....

This reply was deleted.