seL4 – Open source formally verified bug free microkernel OS released

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.

What’s being released?

It includes all of the kernel’s source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All is under standard open-source licensing terms — either GPL version 2, or the 2-clause BSD licence.

via Home | seL4.

Unique about seL4 is its unprecedented degree of assurance, achieved through formal verification. Specifically, the ARM version of seL4 is the first (and still only) general-purpose OS kernel with a full code-level functional correctness proof, meaning a mathematical proof that the implementation (written in C) adheres to its specification. In short, the implementation is proved to be bug-free (see below). This also implies a number of other properties, such as freedom from buffer overflows, null pointer exceptions, use-after-free, etc

Aero Glass – AR for pilots using Epson Moverio glasses

Using the Epson Moverio glasses, Augmented reality projects the following features onto the lenses in 3D.

Airports
Navigation Aids
ADS-B traffic
Flight Plan route & waypoints
Airways
Geographic points of interest (cities, villages, visual navigation points)

Soon followed by:

Airspaces
Terrain elevation
Procedures
ILS approach cones
FLARM traffic (for glider)
Weather
Dynamic Data (NOTAM, TFRs)
Ground Phase stuff other than runways (taxiways, gates etc)
3D Terrain Avoidance
Obstacles

They plan to sell them for around $700,- which is very cheap for a fighter pilot helmet / Heads up display / HUD!

Aero Glass.

Malware without files on the PC, encoded in the registry

As the entry point, they exploit a vulnerability in Microsoft Word with the help of a crafted Word document they spread via email. The same approach would work with any other exploit.
After that, they make sure that the malicious activities survive system re-boot by creating an encoded autostart registry key. To remain undetected, this key is disguised/hidden.
Decoding this key shows two new aspects: Code which makes sure the affected system has Microsoft PowerShell installed and additional code.
The additional code is a Base64-encoded PowerShell script, which calls and executes the shellcode (assembly).
As a final step, this shellcode executes a Windows binary, the payload. In the case analyzed, the binary tried to connect to hard coded IP addresses to receive further commands, but the attackers could have triggered any other action at this point.
All activities are stored in the registry. No file is ever created.

Malware that resides in the registry only – a rare and rather new approach

via .

BadUSB – Turning USB peripherals into hacking vectors

Once reprogrammed, benign devices can turn malicious in many ways, including:

A device can emulate a keyboard and issue commands on behalf of the logged-in user, for example to exfiltrate files or install malware. Such malware, in turn, can infect the controller chips of other USB devices connected to the computer.

The device can also spoof a network card and change the computer’s DNS setting to redirect traffic.

A modified thumb drive or external hard disk can – when it detects that the computer is starting up – boot a small virus, which infects the computer’s operating system prior to boot.

via Turning USB peripherals into BadUSB | Security Research Labs.

Looks like Karsten Nohl has done it again!