• Home
  • Cyber Crime
  • Cyber warfare
  • APT
  • Data Breach
  • Deep Web
  • Digital ID
  • Hacking
  • Hacktivism
  • Intelligence
  • Internet of Things
  • Laws and regulations
  • Malware
  • Mobile
  • Reports
  • Security
  • Social Networks
  • Terrorism
  • ICS-SCADA
  • POLICIES
  • Contact me
MUST READ

SECURITY AFFAIRS MALWARE NEWSLETTER ROUND 55

 | 

Security Affairs newsletter Round 534 by Pierluigi Paganini – INTERNATIONAL EDITION

 | 

Law enforcement operations seized BlackSuit ransomware gang’s darknet sites

 | 

Arizona woman sentenced for aiding North Korea in U.S. IT job fraud scheme

 | 

Operation CargoTalon targets Russia’s aerospace with EAGLET malware,

 | 

Unpatched flaw in EoL LG LNV5110R cameras lets hackers gain Admin access

 | 

Koske, a new AI-Generated Linux malware appears in the threat landscape

 | 

Mitel patches critical MiVoice MX-ONE Auth bypass flaw

 | 

Coyote malware is first-ever malware abusing Windows UI Automation

 | 

SonicWall fixed critical flaw in SMA 100 devices exploited in Overstep malware attacks

 | 

DSPM & AI Are Booming: $17.87B and $4.8T Markets by 2033

 | 

Stealth backdoor found in WordPress mu-Plugins folder

 | 

U.S. CISA adds CrushFTP, Google Chromium, and SysAid flaws to its Known Exploited Vulnerabilities catalog

 | 

U.S. CISA urges FCEB agencies to fix two Microsoft SharePoint flaws immediately and added them to its Known Exploited Vulnerabilities catalog

 | 

Sophos fixed two critical Sophos Firewall vulnerabilities

 | 

French Authorities confirm XSS.is admin arrested in Ukraine

 | 

Microsoft linked attacks on SharePoint flaws to China-nexus actors

 | 

Cisco confirms active exploitation of ISE and ISE-PIC flaws

 | 

SharePoint under fire: new ToolShell attacks target enterprises

 | 

CrushFTP zero-day actively exploited at least since July 18

 | 
  • Home
  • Cyber Crime
  • Cyber warfare
  • APT
  • Data Breach
  • Deep Web
  • Digital ID
  • Hacking
  • Hacktivism
  • Intelligence
  • Internet of Things
  • Laws and regulations
  • Malware
  • Mobile
  • Reports
  • Security
  • Social Networks
  • Terrorism
  • ICS-SCADA
  • POLICIES
  • Contact me
  • Home
  • Hacking
  • Security
  • seL4, Hack-proof DARPA-derived micro kernel goes open source tomorrow

seL4, Hack-proof DARPA-derived micro kernel goes open source tomorrow

Pierluigi Paganini July 29, 2014

DARPA-derived secure micro kernel seL4 goes open source tomorrow, it is the a first prototype mathematically proven and hacker-repelling software.

The National ICT Australia (NICTA) has completed the development of the first micro kernel mathematically proven seL4 to be bug free, its  project will be released as open source tomorrow and could be deployed on drones to prevent hacking.

The formal-methods-based secure embedded L4 (seL4) microkernel was derived from the DARPA program High-Assurance Cyber Military Systems. The microkernel seL4‘s entire source code, including proofs and additional code used to build trustworthy, will be released under the GPL v2 license.

“General Dynamics C4 Systems and NICTA are pleased to announce the open sourcing of seL4, the world’s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. It is still the world’s most highly-assured OS.”

The NICTA is Australia’s Information Communications Technology (ICT) Research Centre of Excellence, it is an organization born to conduct, promote and sustain ICT research, it is composed by experts in maths and aviation working with primary companies Boeing and Rockwell Collins.

The micro kernel was the result of High-Assurance Cyber Military Systems program promoted by DARPA, HACMS has a four-year effort and an estimated cost of $60 million with the purpose of define an innovative and secure practice of coding to avoid that software could be affected by a “pervasive vulnerability”.

The program is described on the DARPA website with following statement:

“The High-Assurance Cyber Military Systems (HACMS) program seeks to create technology for the construction of systems that are functionally correct and satisfy appropriate safety and security properties,” explained, Kathleen Fisher, DARPA program manager. “Our vision for HACMS is to adopt a clean-slate, formal method-based approach to enable semi-automated code synthesis from executable, formal specifications.”

“In addition to generating code, HACMS seeks a synthesizer capable of producing a machine-checkable proof that the generated code satisfies functional specifications as well as security and safety policies. A key technical challenge is the development of techniques to ensure that such proofs are composable, allowing the construction of high-assurance systems out of high-assurance components.”

The formal-methods-based secure embedded L4 (seL4) microkernel aims to prevent the hacking of sophisticated devices without impacting performance.

seL4 design process

As explained in the Wiki of OS DEV.org:

“A Microkernel tries to run most services – like networking, filesystem, etc. – as daemons / servers in user space. All that’s left to do for the kernel are basic services, like memory allocation (however, the actual memory manager is implemented in userspace), scheduling, and messaging (Inter Process Communication).

In theory, this concept makes the kernel more responsive (since much functionality resides in preemptible user-space threads and processes, removing the need for context-switching into the kernel proper), and improves the stability of the kernel by reducing the amount of code running in kernel space. “

In other words a similar approach allows to develop more stable and responsive software respect canonical monolithic kernels such as the Linux and Windows kernels.

The micro kernel belonging to the seL4 family could be used in wide casuistry, every critical component could be equipped with hacking proof software.

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.” said Doctor June Andronick.

Experts at NICTA provided a fascinating video-POC which demonstrates how a drone which running the platform could detect hacking attempts and adopt necessary countermeasures.

In the video, once the demo drone has detected the intrusion it fly away preventing that the hack is successfully conducted.

“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.

Are we really close to the realization of a hack-proof machine?

Pierluigi Paganini

Security Affairs –  (seL4, DARPA)


facebook linkedin twitter

DARPA Drones Hacking HACMS micro kernel NICTA pervasive vulnerability seL4

you might also like

Pierluigi Paganini July 26, 2025
Arizona woman sentenced for aiding North Korea in U.S. IT job fraud scheme
Read more
Pierluigi Paganini July 25, 2025
Unpatched flaw in EoL LG LNV5110R cameras lets hackers gain Admin access
Read more

leave a comment

newsletter

Subscribe to my email list and stay
up-to-date!

    recent articles

    SECURITY AFFAIRS MALWARE NEWSLETTER ROUND 55

    Malware / July 27, 2025

    Security Affairs newsletter Round 534 by Pierluigi Paganini – INTERNATIONAL EDITION

    Breaking News / July 27, 2025

    Law enforcement operations seized BlackSuit ransomware gang’s darknet sites

    Cyber Crime / July 26, 2025

    Arizona woman sentenced for aiding North Korea in U.S. IT job fraud scheme

    Intelligence / July 26, 2025

    Operation CargoTalon targets Russia’s aerospace with EAGLET malware,

    Intelligence / July 25, 2025

    To contact me write an email to:

    Pierluigi Paganini :
    pierluigi.paganini@securityaffairs.co

    LEARN MORE

    QUICK LINKS

    • Home
    • Cyber Crime
    • Cyber warfare
    • APT
    • Data Breach
    • Deep Web
    • Digital ID
    • Hacking
    • Hacktivism
    • Intelligence
    • Internet of Things
    • Laws and regulations
    • Malware
    • Mobile
    • Reports
    • Security
    • Social Networks
    • Terrorism
    • ICS-SCADA
    • POLICIES
    • Contact me

    Copyright@securityaffairs 2024

    We use cookies on our website to give you the most relevant experience by remembering your preferences and repeat visits. By clicking “Accept All”, you consent to the use of ALL the cookies. However, you may visit "Cookie Settings" to provide a controlled consent.
    Cookie SettingsAccept All
    Manage consent

    Privacy Overview

    This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities...
    Necessary
    Always Enabled
    Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
    Non-necessary
    Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
    SAVE & ACCEPT