You are here

Porting RTK to High Assurance Kernel


OUSD (R&E) CRITICAL TECHNOLOGY AREA(S): Trusted AI and Autonomy; Advanced Computing and Software

OBJECTIVE: Develop innovative techniques and tools to run the Robotic Technology Kernel (RTK) software library securely and efficiently on a high-assurance separation kernel. Demonstrate feasibility via proof-of-concept and practical prototype. Validate the new capabilities using a high-assurance separation kernel, Robot Operating System (ROS) test suite, RTK applications and a representative hardware platform under realistic concept of operations.

DESCRIPTION: This topic seeks innovative technology and demonstration that showcases the feasibility, security and performance of running the RTK and ROS software library on a high-assurance separation kernel. Supported by the DARPA High-Assurance Cyber Military Systems (HACMS) program, both seL4 and CertiKOS have made great leaps in terms of software capabilities and maturity. However, significant challenges exist to bridge the gap between research prototypes and adoption. It is critical to leverage such innovative techniques and tools and build assured systems based on appropriate techniques and tools applying sound security design and engineering principles. The ported RTK/ROS over a separation kernel should function and perform with added security and it should maintain the features of (1) cross-platform: new RTK capabilities can be leveraged by all RTK-enabled platforms; (2) cross-controller: any RTK-enabled platforms can be controlled by any RTK compatible controller; and (3) cross-effort: an effort delivers new capabilities to the RTK, which in turn is leveraged for new efforts. In addition to memory isolation, the ported RTK/ROS should be amenable to other security checks such as the concept of Monitor and Policy Enforcement, as applicable and needed in DoD use cases including Autonomy and Swarm.

PHASE I: Develop the technical approach, analyze trade-off options, and justify design choices. All design choices, including a representative hardware platform, should be made in agreement with the Government counterpart. Finalize the overall design that can securely and efficiently run RTK (and ROS) on a high-assurance separation kernel. Analyze the costs and benefits, accounting for practical implementation constraints in Army platforms and use cases. Prepare the path for a proof-of-concept demonstration. Document all lessons learned for way forward.

PHASE II: Fully develop the technology and a practical prototype. Test and evaluate the security and performance of the ported RTK (and ROS) running on a high-assurance separation kernel, under various ROS/RTK test cases as well as relevant mission scenarios. Demonstrate the capabilities using a representative hardware platform under realistic concept of operations, such as those adopted in previous Army efforts [5]. Enhance and mature the technology and prototype for transition.


  • High Assurance Kernel Technology and Robotic Technology Kernel (RTK) have medium adoption across a range of industries including autonomous vehicles, aerospace and defense, and Internet of Things (IoT). The use of this technology helps to enable security, reliability, and trustworthiness of critical systems.
  • The IoT and software segment registers in highest share of revenue as well as innovation. The growing use of digital manufacturing and IoT integration in production of smart and autonomous vehicles will likely drive continued growth.
  • The integration of high assurance kernel security solutions will enable companies to improve their cybersecurity stature as well as offer more security in a myriad of arenas, including the continued growth of autonomous offerings, signaling sustained demand for this technology in future years as technology evolves and new economies accelerate digitalization and industrialization in manufacturing processes. 

KEYWORDS:  Robotics; Robot Operating System; Robot Technology Kernel; Cybersecurity; Software; Performance


  1. M. Vai, D. Whelihan, K. Denny, R. lychev, J. Hughes, D. Kava, A. Lee, N. Evancich, R. Chark, D. Lide, K. Kwak, J. Li, D. Schafer, M. Lych, K. Tilloton, and W. Tirenin, “Agile and Resilient Embedded Systems”, IEEE Conference on Military Communications, 2021.
  2. D. Whelihan, M. Vai, N. Evanich, K.J. Kwak, J. H. Li, M. Britton, B. Frantz, D. Hadcock, M. Lynch, D. Schafer, J. DeMatteis, and D. Russo, “Designing Agility and Resilience into Embedded Systems,” IEEE Conference on Military Communications, 2017.
  3. Cynthia Irvine, “Combining ROS with seL4 for Trustworthy Autonomous Systems,” Second Annual Trusted Computing Center of Excellence Summit, 2019.
  4. Robot Operating System (ROS) -
  5. US Army – TARDEC Ground Vehicle Robotics, “Introduction to Robotic Technology Kernel (RTK),” Distribution Statement A.
  6. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser, “Comprehensive formal verification of an OS microkernel,” ACM Trans. Comput. Syst. 32, 1, Article 2, February 2014.
  7. Certified Kit Operating System (CertiKOS),
  8. Trusted Computing Center of Excellence -
  9. TCCOE Summits -
  11.  Daniel Limbrick, “Performance Evaluation of ROS on an seL4-based Raspberry Pi / Jetson TK1,” Second Annual Trusted Computing Center of Excellence Summit, 2019.
  12. Gernot Heiser, “The seL4 Microkernel - An Introduction.” White Paper. The seL4 Foundation, Revision 1.2 of 2020-06-10.
US Flag An Official Website of the United States Government