Feeds

Secure microkernel that uses maths to be 'bug free' goes open source

Hacker-repelling, drone-protecting code will soon be yours to tweak as you see fit

Website security in corporate America

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

The formal-methods-based secure embedded L4 (seL4) microkernel was developed by boffins backed by National ICT Australia (NICTA). In 2012, the software was enlisted to help stop hackers knocking unmanned birds out of the sky, and it's used in the US Defense Advanced Research Projects Agency's High-Assurance Cyber Military Systems program.

It was noted as the most advanced and highly-assured member of the L4 microkernel family due to its use of formal methods that did not impact performance. A microkernel differs from monolithic kernels – such as the Linux and Windows kernels – by running as much code as possible – from drivers to system services – in user space, making the whole thing more modular and (in theory) more stable.

Tomorrow at noon Eastern Australian Standard Time (GMT +10) seL4's entire source code including proofs and additional code used to build trustworthy systems will be released under the GPL v2 licence.

A global group of maths and aviation gurus from the likes of Boeing and Rockwell Collins joined a team of dedicated NICTA researchers on the project which involved the seL4 operating system designed to detect and foil hacking attempts.

NICTA senior researcher Doctor June Andronick said the kernel should be considered by anyone building critical systems such as pacemakers and technology-rich cars.

"If your software runs the seL4 kernel, you have a guarantee that if a fault happens in one part of the system it cannot propagate to the rest of the system and in particular the critical parts," Andronick said earlier this month.

"We provide a formal mathematical proof that this seL4 kernel is correct and guarantees the isolation between components."

NICTA demonstrated in a video how a drone which running the platform could detect hacking attempts from ground stations that would normally cause the flight software to die and the aircraft to crash.

"What we are demonstrating here is that if one of the ground stations is malicious, and sends a command to the drone to stop the flight software, the commercially-available drone will accept the command, kill the software and just drop from the sky," Andronick said.

The researchers' demo drone would instead detect the intrusion at temp, flash its led lights and fly away. This could ensure that real drone missions could continue in the event of hacking attempts by combatants.

Andronick said seL4 would come into play as the team added more functionality including navigation, autonomous flight and mission control components.

In depth information about seL4 was available on the NICTA website and within the paper Comprehensive Formal Verification of an OS Microkernel. ®

* That's bug free according to the formal verification of its specification; design flaws in the specs aren't counted by the team.

Youtube Video

Protecting users from Firesheep and other Sidejacking attacks with SSL

More from The Register

next story
Hackers pop Brazil newspaper to root home routers
Step One: try default passwords. Step Two: Repeat Step One until success
UK.gov lobs another fistful of change at SME infosec nightmares
Senior Lib Dem in 'trying to be relevant' shocker. It's only taxpayers' money, after all
Critical Adobe Reader and Acrobat patches FINALLY make it out
Eight vulns healed, including XSS and DoS paths
Spies would need SUPER POWERS to tap undersea cables
Why mess with armoured 10kV cables when land-based, and legal, snoop tools are easier?
TOR users become FBI's No.1 hacking target after legal power grab
Be afeared, me hearties, these scoundrels be spying our signals
Blood-crazed Microsoft axes Trustworthy Computing Group
Security be not a dirty word, me Satya. But crevice, bigod...
Snowden, Dotcom, throw bombs into NZ election campaign
Claim of tapped undersea cable refuted by Kiwi PM as Kim claims extradition plot
Freenode IRC users told to change passwords after securo-breach
Miscreants probably got in, you guys know the drill by now
THREE QUARTERS of Android mobes open to web page spy bug
Metasploit module gobbles KitKat SOP slop
prev story

Whitepapers

Secure remote control for conventional and virtual desktops
Balancing user privacy and privileged access, in accordance with compliance frameworks and legislation. Evaluating any potential remote control choice.
WIN a very cool portable ZX Spectrum
Win a one-off portable Spectrum built by legendary hardware hacker Ben Heck
Storage capacity and performance optimization at Mizuno USA
Mizuno USA turn to Tegile storage technology to solve both their SAN and backup issues.
High Performance for All
While HPC is not new, it has traditionally been seen as a specialist area – is it now geared up to meet more mainstream requirements?
The next step in data security
With recent increased privacy concerns and computers becoming more powerful, the chance of hackers being able to crack smaller-sized RSA keys increases.