> The EverCrypt project did phenomenal work producing formally verified (including side-channel resistant) cryptography libraries but a formally verified progra

> The EverCrypt project did phenomenal work producing formally verified (including side-channel resistant) cryptography libraries but a formally verified program only has the properties that are proven if the axioms hold. If you don't have memory safety then these axioms don't hold. This is not true. You can have formally verified programs in a non-memory safe language. The author is mixing discussions of memory-safe languages vs memory-safe programs. They make this "anti-distinction" because they actually want to run both kinds of programs (w/ and w/o compile-time memory guarantees) in a sandbox that itself provides the memory-safe guarantees. Of course, they will sell you that sandbox. But who wrote the sandbox, and and here we are: what are its guarantees conditioned on: > You can take for granted the fact that any out-of-bounds access and any use-after-free will trap. And that means that you can share an object with another compartment by passing it a pointer. You can rely on the fact that, if you pass another compartment a pointer to an on-stack object (or any pointer that you've explicitly marked as ephemeral), any attempt to capture that pointer will trap. You can share a read-only view of a buffer, by providing a pointer without write permission, or of a complex data structure by providing one without transitive write permission. So, forgive my ignorance, but this is great for _your_ code, but not helpful for the code of others. They could still read the data from a buffer the not-so-safe code used to copy the data you sent to it, and no amount of "marking it ephemeral" can save you unless somehow the safety is transitory. This doesn't seem possible. > vacuum-cleaner model of software development': point your vacuum cleaner at the Internet, vacuum up all of the components you need, and ship them. Only now you can audit exactly what each of those third-party components has access to. Because even assembly code has to follow the core rules for memory safety, you can write policies about what they should be able to access and audit them before you sign a firmware image. Yeah - find. You allow openssl to see your data, then component X is exploited and reads data from an openssl _copy_ of that data. right?