It seems like this only guarantees security along some particular vector. Which might be why current software doesn’t actually use this type of security.
And if you did actually close off software security as a threat model from ASI, wouldn’t it just choose a different, physical attack mode?
The vectors are classes of software error. Since ultimately it is all binary messages between computers, it is likely possible to build a robust set of solvers that covers all classes of software error that the underlying programming language permits, resulting in code that cannot be compromised by any possible binary message.
And if you did actually close off software security as a threat model from ASI, wouldn’t it just choose a different, physical attack mode?
Yes. It becomes a battle between [ASI with robotically wielded weapons] and [humans plus weaker, more controllable ASI with robotically wielded weapons].
All computer systems are actually composed of hardware, and hardware is much messier than the much simpler abstractions that we call software. There are many real-world exploits that from a software point of view can’t possibly work, but do in fact work because all abstractions are leaky and no hardware perfectly implements idealized program behaviour in reality.
It seems like this only guarantees security along some particular vector. Which might be why current software doesn’t actually use this type of security.
And if you did actually close off software security as a threat model from ASI, wouldn’t it just choose a different, physical attack mode?
https://github.com/project-everest/mitls-fstar
It mostly doesn’t.
The vectors are classes of software error. Since ultimately it is all binary messages between computers, it is likely possible to build a robust set of solvers that covers all classes of software error that the underlying programming language permits, resulting in code that cannot be compromised by any possible binary message.
Yes. It becomes a battle between [ASI with robotically wielded weapons] and [humans plus weaker, more controllable ASI with robotically wielded weapons].
All computer systems are actually composed of hardware, and hardware is much messier than the much simpler abstractions that we call software. There are many real-world exploits that from a software point of view can’t possibly work, but do in fact work because all abstractions are leaky and no hardware perfectly implements idealized program behaviour in reality.