When is a Verified Program Secure?

Early in my research trajectory, before I developed a narrower focus, I often told people at programming languages conferences that I worked on “security and programming languages”. The most common response: “Oh, you mean verification?”

Looking back now, this reaction makes me wince. Not because it’s inaccurate to my research—I do, in fact, spend a lot of time on verification!—but because it reveals a fundamental misconception about the relationship between verification and security. Namely, that a verified program is clearly a secure one.

I want, first, to convince you that this idea is essentially false; and second, to discuss why. It’s not just because formally defining and proving security is technically difficult, though it certainly is. The real challenge to verifying a program’s security is this: “Security” can only be defined in context. And the context is a product of not only the program in question, but where it’s used, who is using it, and why.

So when is a verified program secure? Can it ever be?

Verification (A Bird’s-Eye View)

At a very, very high level, verifying a program usually goes something like this:

1. Start by defining a specification, or model, for how the program should behave. Doing this correctly is usually quite hard. (Even determining what it means for a specification to be “correct” can be a challenge!)
2. Then you need to prove the program adheres to the specification, e.g., with a theorem prover like Rocq or Lean. This is also very hard.
3. Once you get through 1 and 2, you’re done! The program is verified, and you can be confident in its correctness.

Of course, there are a lot of details I’m abstracting away here. Nonetheless, the overarching framing typically holds: If you can overcome the challenge of defining a specification and proving the code meets it, you’re rewarded with a program that is provably (mathematically) correct.

But is a correct program necessarily secure? Or, to put it another way: When does correctness imply security?

As with all things in programming languages, and in computer science broadly, everything depends on your definitions. “Correctness”, here, we can define simply as adherence to the specification. Generally speaking, a correct program should “do what it’s supposed to do”—like a sum function returning the result of adding two or more numbers—and “not do what it’s not supposed to do”—like modifying some part of memory that should be left unchanged.

That’s a pretty expansive definition! If “correctness” just means that our program obeys the specification, then can’t we simply define security as a part of the spec? Then proving the program is correct would also mean we’d proved it secure.

Correctness\(\implies\)Security?¹

In fact, plenty of researchers have done just that.

There is, for example, a long history of efforts to verify that cryptographic code is constant-time. Because cryptographic programs handle deeply sensitive data, like passwords and secret keys, we care very much that no one can, e.g., measure how long it takes to check a guessed password in order to learn what your real password is. These days, constant-time properties are considered so important and well-established that projects on verifying cryptographic code often take them as a given, such as in the prominent Fiat-Crypto library.

Another example, generally also applied to cryptographic code, lies in verifying security under speculation. This property, or family of properties, is used to show that a cryptographic function keeps passwords, keys, etc. confidential even in the presence of speculative execution. Research on proving speculative security is much more nascent than constant-time verification, but there is still plenty of work in the space (e.g., ProspeCT, Speculative Taint Tracking, Leakage Contracts). (For more reading on speculation and verification, you can also check out one of my previous blog posts.)

With speculative security, however, we run into a problem. Notice that when we defined correctness, we did so as a function of the software, or the program itself: We said that a correct program was one that met its specification. Yet speculative execution, and thus speculative security, is not actually a property of software, but of hardware. It’s an optimization built into the very machine that runs our program.²

The details of how speculative execution works aren’t especially important here. What is important is that it occurs not just as a function of the one program that we want to verify, but also of the environment where we run that program. That environment includes the physical hardware, and also, potentially, as much as every other program running on the same machine as ours.

Speculative security is just one of the many kinds of security that cannot be defined purely as a function of a single program. So how can we embed security into a program’s specification, if security might depend on so many factors external to that program?

Correctness\(\implies\)A Model of Security

The short answer: We can’t. At least, not without making explicit our assumptions about where we’re running the program, and what kinds of security we’re even considering to begin with.

Luckily, security researchers have a solution to this problem.

Threat Modeling

In security research, threat modeling provides a framework for explicitly defining the kinds of security we’re concerned with. To build a threat model, we have to answer a few important questions:

1. Who is our adversary, and what are their capabilities?

   • Is the adversary running a program (like a piece of malware) on the same machine as our code?
   • Do they have physical access to the computer?
   • Or are they attempting to leak information from afar?

2. What are we trying to protect? What are our security policies or goals?

   • Are we trying to keep a password or cryptographic key secret (confidentiality)?
   • Are we concerned with making sure data we send isn’t modified (integrity)?
   • Or is our goal entirely different, like keeping our service online and available no matter what?

Notice that our answers to these questions might have very little to do with the literal code we want to verify! Our answers will, however, vary heavily by the reasons why we’re using that code—and by the environment where we’re running it.

This variance is important, and intentional. The threat model for a secure messaging app, concerned with confidentiality and integrity over a network, can and should be different from the threat model for an online marketplace, which may place a higher priority on availability. Still other models need to consider adversaries in the real world, like an untrusted party gaining physical access to your devices.

Whatever your threat model turns out to be, it represents a structured way of enumerating your security needs and assumptions. With these, you can finally, formally, define what security means for your program and its specification.

Then, when you verify that your program is correct, you will have also proven it secure… but only under your particular threat model. And if (or rather, when) your or your users’ threat model changes, your proof will have to change with it.

Security is About People, Not Programs

If you’re the sort who prefers to find perfectly technological or mathematical solutions to your problems, this conclusion might feel a bit unsatisfying. Why should your verification proof have to depend on such a squishy, human-centered concept as a threat model before you can assert any kind of security guarantee?

The not-so-dirty secret of computer security is that, despite how many papers might try to convince you otherwise, security is an inherently human discipline. We can—and should!—try our best to encode security goals into the kind of precise, formalized terms that let us say something provable about our programs. But where a proof of “adherence to the spec” will always remain true of that particular program and specification, any “proof” of security is forever subject to the changing needs of and threats to the people it affects.

Security is not a property of data, or programs. It’s a property of people, and their goals, needs, and rights. As researchers, we forget that at our own peril.³

Footnotes