F6 Project


Kestrel has participated in the DARPA System F6 program for fractionated satellites (= satellites composed of free-flying modules that communicate wirelessly), as part of the Vanderbilt team.

The team has designed and implemented a novel information architecture for fractionated satellites, which includes a multi-level secure operating system, a middleware that provides facilities for high-level component interactions, a component model to build applications, and a model-based development tool.

Kestrel has contributed to the design of the security aspects of the information architecture and has used the Isabelle/HOL theorem prover to formalize and prove properties of the multi-domain security labels used by the operating system to enforce multi-level secure information flow among applications. Kestrel has also implemented a C library that provides operations to manipulate such multi-domain security labels (e.g. to perform Mandatory Access Control checks).


  1. A Software Platform for Fractionated Spacecraft
    Abhishek Dubey, William Emfinger, Aniruddha Gokhale, Gabor Karsai, William Otte, Jeffrey Parson, Csanád Szabó, Alessandro Coglio, Eric Smith, and Prasanta Bose
    2012 IEEE Aerospace Conference
    March 2012
  2. DREMS: A Model-Driven Distributed Secure Information Architecture Platform for Managed Embedded Systems
    Tihamer Levendovszky, Abhishek Dubey, William R. Otte, Daniel Balasubramanian, Alessandro Coglio, Sandor Nyako, William Emfinger, Pranav Kumar, Aniruddha Gokhale, and Gabor Karsai
    IEEE Software, Volume 31, Number 2, pages 62-69
    March/April 2014
  3. Establishing Secure Interactions Across Distributed Applications in Satellite Clusters
    Subhav Pradhan, William Emfinger, Abhishek Dubey, William Otte, Daniel Balasubramanian, Aniruddha Gokhale, Gabor Karsai, and Alessandro Coglio
    5th IEEE International Conference on Space Mission Challenges in Information Technology (SMC-IT), pages 67-74
    September 2014