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

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.