Frontier AIs are already smart enough to find ways to get out of sandboxes, circumvent permissions, and devise side-channels. Anthropic has shown formal verification is possible at scale. [1]
What this means is that the only hope for secure applications is security by construction, with formal methods. The race is on for constructing formally verified primitives with more and more expansive guarantees. The Anthropic/Theorem proofs show lack of memory sanitization issues. But that's just one class of problem.
Imagine a chip, a minimal boot loader, a minimal Linux, and an application library stack - all verified with high level guarantees. Then, you can plug in your application development to give you end-to-end verification guarantees. ie: no way to leak credentials at any level from the chip up to the application. No sense in your foundation being so strong if your application has easy RCEs. You need a full stack approach.
I know I'm describing a far off dream world, but it may be what's required to quell the economic "bomb" of so much dev time "wasted" in patching vulns, against actual feature dev / business value generation.
[1]: https://www.anthropic.com/research/formal-verification
What this means is that the only hope for secure applications is security by construction, with formal methods. The race is on for constructing formally verified primitives with more and more expansive guarantees. The Anthropic/Theorem proofs show lack of memory sanitization issues. But that's just one class of problem.
Imagine a chip, a minimal boot loader, a minimal Linux, and an application library stack - all verified with high level guarantees. Then, you can plug in your application development to give you end-to-end verification guarantees. ie: no way to leak credentials at any level from the chip up to the application. No sense in your foundation being so strong if your application has easy RCEs. You need a full stack approach.
I know I'm describing a far off dream world, but it may be what's required to quell the economic "bomb" of so much dev time "wasted" in patching vulns, against actual feature dev / business value generation.
[1]: https://www.anthropic.com/research/formal-verification