Assured Isolation of AI (AI^2) for HPSC Platforms (AI^2)

Our reliance on space systems continues to increase yet there has been little focus on securing these systems. The same cybersecurity methods that have been adopted on Earth based systems have not yet made their way into space. This may in part be due to the lack of performance and capabilities of Space hardware. Seeing this need to increase the performance and capabilities of space systems, Microchip developed a new High-Performance Spaceflight Computing (HPSC) series of processors that are designed to significantly improve computational capacity for future space missions. With this increased capability, space systems can take advantage of more modern and emerging technologies such as AI. Despite this increase in capability, adoption of emerging technologies within space systems can still be difficult due to the high safety requirements of such systems. For example, adoption of non-deterministic AI algorithms can be difficult because of the unpredictable effects on the safety critical aspects of the system. Also, as space systems become more capable and more complex, they become larger and more impactful targets for malicious actors who may want to compromise these systems through cyber-attack. This proposal presents a solution to mitigate these issues by providing a high assurance base platform using the seL4 Hypervisor on the Microchip HPSC processor. The seL4-based hypervisor on Microchip HPSC solution addresses these challenges by providing a robust and formally verified platform capable of running emerging technologies such as AI algorithms in a secure, isolated, and resilient environment. This solution will provide space system developers with a method to isolate non-deterministic or untrusted applications from the safety-critical subsystems while also providing robust security in their next generation space systems.

This project contributes to the developing HPSC ecosystem by enabling use of a open-source hypervisor supporting high assurance VM-architectures. The HPSC platform is targeted for Rovers, Landers, High Bandwidth Instruments, and SmallSat/Constellation missions. Immediate projects considering use of the HPSC include WFIRST/Chronograph, Gateway, and SPLICE/Lunar Lander. This project also provides benefits to current missions targeting other modern hardware that can run seL4, like the AMD Zynq UltraScale+ MPSoC, which is being used in devices like Innoflight’s, space hardened, high-performance CFC-400 and NASA’s SpaceCube 3.0. Providing the ability to isolate non-deterministic software such as AI algorithms can allow NASA to more easily take advantage of innovation in earth based systems such as robotics and apply that technology to next-generation space systems. The seL4 microkernel and Microchip HPSC separately provide many benefits and when combined these benefits complement each other to create a base platform that enables cyber resiliency, improved safety, and high performance for next generation applications. The seL4 microkernel can leverage the virtualization extensions provided by the HPSC to host virtual machines that can be used to isolate legacy software from other parts of the system which allows newer, more secure software to be built up around this legacy software. This feature also reduces the barrier to upgrade legacy software by enabling incremental upgrades. Components can be pulled out of the virtual machine run as native seL4 components or added to another virtual machine running a different operating system all while providing a working solution at each iteration. With the strong isolation guarantees provided by the formal proof of the microkernel, which encourages the design strategy of least privilege, software processes can be given the hardware components they need and nothing else which reduces the effect of a compromised or faulty software component on the rest of the system. This type of isolation also enables flexibility for system designers to leverage the capabilities of the HSPC hardware in ways not possible by traditional operating systems. A provably correct microkernel is valuable for applications and products requiring high assurance software design for safety and/or security. These applications and products are found in industrial, medical, finance, automotive, and aviation markets, but cyber security concerns are growing in all markets. Providing easy-to-use hypervisor capabilities built on this microkernel allows customers to benefit from the advantages of using high-assurance virtualization, such as application disaggregation and mixed criticality operation.

This is a mature technology (TRL 7+) — the realistic path in is usually NASA's Technology Transfer Program: licensing an existing NASA patent, or a Space Act Agreement to use NASA facilities/expertise directly. NASA also runs a startup licensing program with no upfront fee for companies formed to commercialize a specific NASA technology.

None of these are guaranteed paths for this specific project — TechPort itself doesn't have an "apply" button. Reaching out to the contact(s) above with a specific question is usually the fastest way to find out what's actually open.