The eChronos project @ NICTA and Breakaway
In collaboration with Breakaway Consulting, the eChronos project builds and formally verifies, a small, versatile, high-assurance real-time operating system (OS) for embedded micro-controllers. In contrast to other OS work at NICTA, the eChronos RTOS is for tightly constrained devices without memory protection. Current implementations are available for Intel 80251 and ARM Cortex M4 micro-controllers.
The eChronos RTOS is open source, available under AGPLv3 on github. For separate commercial licenses, please contact us (see below).
On modern powerful embedded hardware, like in smartphones, OS kernels such as NICTA's formally verified seL4 kernel can provide isolation and gatekeeper functionality - controlling what the user-level programs can do with the hardware, or with other programs. For instance, it could stop a malicious app from crashing your smartphone.
On less powerful hardware - such as small medical implant devices, extremely resource-constrained spacecraft, or simple logic controllers used in industrial plants - such gatekeeper functionality is not possible. Instead, these systems run small, so-called real–time operating systems (RTOS) such as the eChronos RTOS. The constrained nature of the hardware devices the RTOS runs on makes it even more challenging to provide assurance and evidence that it works reliably.
This project is part of the Trustworthy Systems umbrella. The eChronos RTOS is also used on the flight-control processor of the DARPA-funded SMACCM project (both on the research platform and later on the commercial Boeing helicopter).
Problem: Modern critical systems - such as medical devices and car braking systems - rely on software. At the heart of these devices sit real-time operating systems such as the eChronos RTOS.
Software at this level can lead to injury or damage or worse. So it is important that such software be reliable and safe, and it is essential to ensure that it performs precisely as intended.
Approach : Formal machine-checked verification of the eChronos RTOS, initially for functional correctnes, later also for worst-case execution time.
eChronos RTOS functionality :
The eChronos RTOS is highly configurable and comes in multiple variants, so only the functionality that is actually needed runs on the device.
- Suitable for devices with constrained resources
- Tasks: user defined, perform syscalls
- Scheduler: round robin or strict priorities
- Multithreading: cooperative or preemptive
- Signals: tasks send and wait for signals
- Interrupts: Interrupt handlers raise events
- Synchronisation: mutex and sempaphore modules
To achive maximum reliablilty, we are using formal machine-checked proof to verify functional correctness of the eChronos RTOS with respect to its functional specification.
- Formal functional specification (completed)
- Prove higher-level correctness properties on specification (first properties completed)
- Show that code refines functional specification (in progress)
- Utilise autocorress and other existing verification tools
- Concurrency and interrupt reasoning
- Kernel can be preempted by interrupts
- Tasks can be preempted
- Low-level context-switching code
- Aug 2015: Released under AGPLv3, available on github.
- Feb 2014: Formal verification of code-level assertions completed by model checking.
- Jan 2014: the eChronos RTOS flies the SMACCMPilot quadcopter and at the DARPA HACMS demo day.
- Oct 2013: Functional C implementation verification starts on eChronos RTOS code.
- Sep 2013: Example code for PX4 board shipped to project partners.
- Sep 2013: Version 0.0.2 shipped to project partners, support for preemption, semaphores, and strict priority scheduling.
- Apr 2013: Version 0.0.1 shipped to project partners for QEMU and STMF32 discovery board.
- Apr 2013: Proved a number of higher-level properties about the eChronos RTOS specification: schedule fairness and signal handling.
- Nov 2012: First version of a formal functional specification complete.
The eChronos RTOS is open source, available under AGPLv3 on github.
The eChronos RTOS is also available for commercial deployment. For separate commercial licenses, please contact us (see below) for further information.
Gerwin Klein, gerwin.klein nicta.com.au