Is it correct?

If I ask you if some code is correct, there are broadly two things I could be asking: (1) does this code have the desired behavior for the set of inputs that users will provide, and (2) does it have the desired behavior for all possible inputs. In general, we care about (1) because that defines the sort of experience users will have, and we care about (2) for security.1 All other things being equal, (2) is a better property of course – it’s strictly more correctness than (1) offers. Alas, proving to ourselves that code is correct for all possible inputs is harder than proving it’s correct for some specific set of inputs – the latter can be done with a test suite, while the former requires something more. As a result, the verification we do for most software is a hybrid: testing to ensure the code has the right behavior on the set of inputs we care about, and other more expensive techniques to ensure it doesn’t have security vulnerabilities (with adversarially chosen inputs).

Even with hybrid verification, where the set of properties we want to verify over all possible inputs is limited to not having security vulnerabilities, verifying these properties for all inputs is frequently more expensive than verifying the code is correct for a fixed set of inputs. Therefore, any properties of the code that we can make adversarially robust by construction, rather than by post-hoc verification, are extremely valuable in reducing the overall costs of verification. Importantly, what properties are true by construction is the sort of thing we can control through the use of better tools, libraries, and abstractions.

Let’s say we have a small kernel of an algorithm (say, a checksum algorithm) that can be significantly sped up through the use of SIMD instructions. If we write that kernel in assembly, we need to write some tests to verify it works as expected on some inputs, and we need to do something to verify there are no security vulnerabilities on any other inputs. Verifying things about assembly is fiddly and annoying for many reasons, not the least of which is that not that many engineers know assembly well. Assembly doesn’t have structured control flow like higher level languages, it’s types are less expressive, any read/write to memory is something you need to ensure is to a valid pointer. However, if instead we can write the algorithm’s kernel using a higher-level SIMD abstraction (e.g., Go’s simd or Rust’s fearless_simd) then our adversarial verification is much simpler: we check if there’s any use of unsafe, we check that the function doesn’t perform any IO or do anything else that might lead to a vulnerability (this should be easy, it’s a checksum algorithm, so doing anything other than looking at the input bytes is a red flag!), and we’re done.

Because of this, as a first order matter, I’m a huge fan of safe SIMD abstractions. They make high-performance SIMD accessible to more engineers. More broadly, they exemplify the way better APIs make it possible to dramatically change the shape of what it means to verify software is correct. This is particularly true in the era of LLMs – it’s dramatically easier to verify an LLM-authored algorithm using a safe SIMD abstraction than it is an implementation written entirely in assembly. More broadly, understanding how verifying software against adversarially chosen inputs is a different problem than verifying it doesn’t have bugs that impact users, and how the abstractions and tools you develop and choose can reduce the burden in doing this verification can be a skeleton key for building better software.

  1. Security isn’t the only reason to care about this. There are some systems (e.g., flight control) that are so impactful that we care about ensuring their behavior in all possible circumstances. But for the systems most software engineers will encounter, we’re ok with garbage in/garbage out, as long as it doesn’t introduce a vulnerability. ↩︎