Thoughts on Formal Verification for Software Safety

Background:

• The ‘Pain in the Ass’ Math That Could Save Vibe Coding From Itself

We have known since the beginning of time that people make mistakes, and the mistakes can be costly when an adversary exploits it. Computer programming amplified this. AI amplified this further. We either try to prevent mistakes before they happen (static checks) or wait until it happens and put a bandaid on it (dynamic checks). Even so, some consequences are not painful enough to warrant action which has a cost to implement.

Limit on Formal Verification

Although we prefer to prevent mistakes before they happen, we often don't know something is wrong until we experience the undesirable consequences of the mistake. The consequences are not always obvious.

For a few centuries, mathematicians figured that using propositional logic defined by simple rules like modus ponens and a few axioms might allow us to check for mistakes. It turns out that coming up with these axioms is also not obvious because they are far removed from the mistakes (contradictions) that happen after many induction steps.

Therefore, practically, we can only prevent mistakes from our past experience, wait until something else bad happens, try to figure out the root cause, then learn from it.

Type and Memory Safety in Programming Languages

Programming language researchers tend to think of formal verification as type safety and memory safety. These cover vulnerabilities such as "buffer overflow" and "use after free" leading to Remote Code Execution exploits, and "memory leak" leading to Denial of Service exploits.

At compile time, static type safety can be enforced by something like simply typed lambda calculus, static memory ownership enforced by linear logic, and static array bounds enforced by dependent types. At runtime, dynamic memory safety can be achieved by garbage collection and array bounds checking.

Back in 2024, there was renewed interest urged by the Biden administration calling for the use of memory safe languages. Most type and memory safe languages use a hybrid approach:

• The likes of JavaScript and Python check for type and memory safety at runtime.
• The likes of Java, C#, Go, and TypeScript check for type safety at compile time, but achieve memory safety at runtime through garbage collection.
• Rust checks for type safety and memory ownership during compile time, but checks for array bounds during runtime.

However, a lot of vulnerabilities still happen in code that are both type and memory safe. Ed Woodruff in his YouTube channel Low Level TV deep dives the vulnerabilities and asks the question "would Rust solve this" and the answer is often "no."

There can also be formal verification outside of software systems, such as checking for physical constraints and checking for operational logistics.

Vulnerabilities Besides Type and Memory Safety

In a broad stroke, we could group software vulnerability causes in the following categories:

• Injection flaws such as Code injection, Command injection and SQL injection are caused by improper check or use of user-supplied data.
• "Log4Shell" (CVE-2021-44228) where log string substitution design flaw in Java allowed an attacker to fetch an arbitrary URL and exfiltrate sensitive data.
• Critical logic flaw (Business logic vulnerability) are caused by improper checks in software.
• "dirty pipe" (CVE-2022-0847), "copy fail" (CVE-2026-31431) and "dirty frag" (CVE-2026-43284) are Linux kernel bugs where improper in-place modification allowed unprivileged users to modify the disk cache of setuid binaries.
• "goto fail" (CVE-2014-1266) is an Apple library bug where a misplaced goto statement caused the acceptance of invalid X.509 certificates.
• Side-channel attack exploits the computational side-effects such as timing and power consumption.
• In 2017, Meltdown and Spectre were vulnerabilities discovered in the CPU speculative execution that prompted significant CPU redesigns.
• Cryptanalysis exploits flaws in cryptography design that allows an attacker to recover symmetric encryption keys by deducing the probability of reused keys, recurring ciphertext or recurring plaintext.

Each of these vulnerability causes could lead to practical exploits such as Remote Code Execution or leaking of sensitive data. Some of these vulnerability categories can be prevented by creative use of programming language features (apart from type and memory safety checks).

Solution to Injection Flaws

Go disallows using unexported types from outside of a package, but compile time literals can be implicitly converted to an unexported type.

Suppose we have a package:

package trusted // import: "example.com/unexported/trusted"

import "strings"

type trustedString string

func Join(sep trustedString, args ...trustedString) trustedString {
	elems := make([]string, len(args))
	for i := range args {
		elems[i] = string(args[i])
	}
	return trustedString(strings.Join(elems, string(sep)))
}

And main.go:

package main

import (
	"fmt"

	"example.com/unexported/trusted"
)

func main() {
	fmt.Println(foo.Join(" ", "hello", "world")) // This compiles!

	var hello, world string
	fmt.Scanln(&hello, &world) // From user input.
	fmt.Println(foo.Join(" ", hello, world)) // Compiler error!
}

This "language feature" can be used by SQL libraries to enforce that query strings are compile time literals and cannot be user-supplied data. Similarly, many injection flaws can be prevented in this manner.

Partial Solution to Cryptanalysis Attacks

I have also recently implemented an encryption library that disallows reuse of encryption key by designing the cipher interface as follows.

type Cipher interface {
        Encrypt(dst, src, aad []byte) (c CipherState, cek []byte, err error)
        Decrypt(dst, src, aad []byte, c CipherState, cek []byte) error
}

type CipherState struct {
        IV  Bytes `json:"iv,omitempty"`
        Tag Bytes `json:"tag,omitempty"`
}

The Encrypt() function enforces single use of the Content Encryption Key (cek) by always creating a new key on encryption. The caller does not have any control over the encryption key and IV. This prevents cryptanalysis attack due to reused encryption key and IV.

Final Thoughts

Last week, I explored the use of arena memory allocation to separate data stack and code call stack as an alternative to Shadow Stack to prevent Return Oriented Programming. This is not a solution to buffer overflow, but it mitigates most of the exploit path. I would argue that partial solutions like this is still valuable.

Even with the solutions and partial solutions, formal verification is opt-in. As long as code not using the expressly permitted construct still exists, code would still be vulnerable. There is cost in bringing legacy code into compliance. This cost can be reduced by having AI rewrite the code into a form that can be checked by former verification.

However, there are many vulnerability categories that still need formal verification. For critical logic flaw, each application domain would need their own specs expressed in a formal language:

• Validity of X.509 certificates for "goto fail"
• POSIX pipe semantics for "dirty pipe" and "copy fail"

And the side-channel attacks prevention would probably require something like Temporal Logic of Actions. AI could potentially synthesize some of these specs from natural language.

I think it is safe to say that propositional logic and TLA as the basis of formal verification are probably enough for the foreseeable future. Humans will still need to first bear the cost of mistakes before deciding which ones need to be acted upon.