Remix.run Logo
amluto 6 days ago

IMO the obvious answer is formally verified security.

We can do this today for user mode, and we can mostly do it for ARM64 virtualization. It will be a while and would require substantial assistance from Intel or AMD to achieve it for x86 virtualization because the hardware is Too Darn Complicated and Too Poorly Specified.

Formal verification of the hardware should also be possible.

pixl97 6 days ago | parent [-]

Are people willing to pay the cost of this formal verification. Especially when it needs done at the hardware, firmware, and kernel levels.

amluto 6 days ago | parent [-]

seL4 is willing to pay, but they're mostly targetting a different use case: running programs targeting seL4, which isn’t what typical agentic workflows want. You can, however, run Linux on seL4, and maybe agent sandboxes should start using it. And ARM is, at least sometimes, interested in helping out with security and formal verification research.

Also, the cost of verification is trending pretty sharply downwards.