Securing Edge AI in Contested Environments: Formal Methods for Protection and Continuous Authorization

ABSTRACT

Practical deployment of edge AI systems introduces two fundamental risks beyond the behavior of the AI models themselves.

First, AI models and their supporting software are inherently complex, creating a large attack surface. The protection of edge AI platforms is significantly enhanced when the underlying kernel and operating system are formally verified, providing strong isolation and communication filtering. This can protect the AI from external attackers while constraining AI actions to authorized behaviors.

Second, edge AI systems require frequent updates to model weights and mission packages. For example: an autonomous drone may not have its mission package loaded until time of use. Each update traditionally invalidates the system’s Authorization to Operate (ATO). By leveraging formal isolation properties and precise system composition knowledge, we can reduce the ATO problem to the point where AI components can be updated without violating authorization at all.

This talk presents how formally verified systems, and their supporting evidence, can address both challenges in a practical, deployable manner—enabling edge AI systems that are both resilient to cyber threats and maintainable under real-world operational demands.

BIO

Boyd Multerer is the founder and CEO of Kry10, with over 25 years of experience building software systems and engineering organizations.  He is best known as the creator of Xbox Live (the online gaming platform that has generated over $1 billion annually since its launch in 2002) and held Senior Director roles at Microsoft across Xbox, Windows, and hardware. Boyd founded Kry10 to bring the power of formal verification and secure separation architecture to operational technology and critical systems, giving developers the tools they need to build provably secure systems without needing expertise in formal methods.