Nail the need.
Start with what matters.
How can we protect critical infrastructure when AI can find and exploit software vulnerabilities?
Start with what matters.
How can we protect critical infrastructure when AI can find and exploit software vulnerabilities?
Turn the need into a family of research questions, with or without AI.
Can a compromised component be provably contained?
AI finds bugs faster than we patch them. Bound the damage instead: $$\operatorname{reach}(c) \subseteq \operatorname{policy}(c).$$
Humans decide. Are we asking the right questions?
Can a whole seL4 system provably contain a compromised component?
AI finds bugs faster than we patch them. Bound the damage along every path, not just direct ones: $$\operatorname{reach}^*(c) \subseteq \operatorname{policy}(c).$$
Anyone may take it up: a student, an AI lab, a meandering agent.
Can a whole seL4 system provably contain a compromised component?
AI finds bugs faster than we patch them. Bound the damage along every path, not just direct ones: $$\operatorname{reach}^*(c) \subseteq \operatorname{policy}(c).$$
A proof checker, not a reputation, decides what holds.
Can a whole seL4 system provably contain a compromised component?
Theorem 1. Every component $c$ of the system, compromised or not, satisfies $$\operatorname{reach}^*(c) \subseteq \operatorname{policy}(c).$$