AirStash: The Next Generation OS

The AirStash operating system (OS) is an entirely new OS that was written from the ground up to meet today's demanding requirements:

  • Lossy connectivity
  • Low power (efficiency)
  • Security
  • Performance
  • Scalability

Meeting these requirements required a rethinking of how an operating system should be constructed. Lossy connectivity, which is common with wireless communications, should be able to minimize re-connection times. Low power requires sleeping whenever possible, fast wake-up, fast boot-up, and very efficient code. Security requires thinking about the entire process of OS creation: from language(s) used to write the OS itself, to how the architecture can isolate components and apps, to trusted booting on hardware, to secure and safe communications, among other areas. Performance requires re-designing the standard stacks with more efficient algorithms, reducing memory operations, and writing very efficient code. Finally, scalability requires a novel architecture for intelligent memory management, multiple component instantiation, and portability to new hardware.

AirStash OS has been developed and proven over the past five years, and continues to expand and grow. It enables the SanDisk Connect Wireless Stick to stream a 2 Mbps HD video over for over 7 hours on a 380mAh battery as a WiFi AP. To say its revolutionary is credible.

Architecture

The AirStash OS breaks new ground with a new architectural paradigm that consists of self-contained modules, or components. The motivation for its novel architecture was based upon two key requirements: security and scalability. The isolated components provide a security barrier to other parts of the operating system in the event of a breach such as a hardware memory corruption. A componentized architecture also increases flexibility that improves scalability. Individual components can be swapped out to take advantage of unique hardware. For example, for non MMU hardware architectures, a smaller kernel and MPU memory control is utilized. For more powerful processors with an MMU, an seL4 formally verified kernel can be used along with MMU memory management.

Component OS

Design

After the architecture decisions were made, the design was carefully crafted to reinforce the architectural decisions while providing clean functional boundaries for component re-use and memory management. An example of re-use is being able to instantiate multiple instances of the same component. This, for example, allows multiple TCP/IP stacks to be simultaneously utilized as needed. The very nature of the modular architecture keeps each TCP/IP stack isolated from each other, adding additional security within the operating system code. This contrasts with a monolithic OS such as Linux where a breach in the stack may bleed over into other areas of the operating system.

Implementation

Well engineered software provides inherent improvements in security and efficiency. Similar to engineering integrated circuits where there is no room for error, engineering software properly requires leveraging formal methods to verify that the code is correct and eliminate human coding errors. This requires leveraging the proper languages and coding techniques. The AirStash OS leverages decades of software process and engineering experience in this area by the AirStash team. New techniques were proven working with DARPA to build inherently secure code that did not sacrifice performance.

Security

There are many threat vectors in a complex system. Security techniques must be engineered at all levels to truly be effective. AirStash OS was architected to enable a reduction of the attack surface as much as possible through simplification. Simplification was achieved through componentization to enable clean data and code isolation between functions. After simplification, each major interface boundary was designed to reduce particular attacks:

  1. Sofware-hardware interface
  2. External communications interface
  3. Application interface

Security Boundaries

Once the interfaces were properly designed, implementation using formal methods was used whenever possible to remove buffer overflows, race conditions, deadlocks, etc. Applying formal methods everywhere was not possible due to time and resource constraints, so some areas, such as some low-level drivers, were encapsulated by their component to prevent errors from spreading to other parts of the OS. Over time these drivers can be updated using formal method techniques. This balance of time and resources with formal methods is discussed in our DARPA report D15PC00141.

Security requires continued support over time as novel attacks are discovered. The AirStash OS receives continual improvement. As new features are developed and the OS is ported to new platforms, the same verified components are utilized. Therefore, by virtue of the AirStash OS architecture, it is a simpler strategy to improve smaller, isolated components that do not reduce the integrity of the remaining OS components.

Scalability

The AirStash OS has been implemented on both MPU and MMU silicon architectures. It also has the scalability to additionally work on multi-core and wider datapath silicon. The JVM allows applications to be portable from one system to another to allow reuse. Finally, it is straight forward to add additional or new communication methods as new protocol components can easily be added.

Scalability