A computer scientist writes some code on one side of a chalkboard while a mathematician proves the code is correct on the other side.

Introduction

Secure program synthesis (SPS) is the problem of automatically generating, or “synthesizing”, software which is known to be secure. In practice, this manifests as the triple-task of synthesizing some software S, a specification φ saying what it would mean for S to be “secure”, and a proof P that S satisfies φ. Depending on your formalism, you might write something impressive-looking like:

P ⊢ ( S ⊨ φ )

… meaning that P proves (⊢) that S satisfies (or “models”, ⊨) the security specification φ. The word “secure” here is an informal descriptor of the kinds of qualities enforced by φ, which could be things like, “the program S is not subject to IDOR or SQL injection attacks” or “the smart-contract S does not allow double-spending”, or whatever.^[1] That is to say, security is a social construct -- there is no mathematical way to define “secure” versus “insecure” without first presuming to know which functions of a given program are desirable versus undesirable to the user.^[2]

Note that tons of engineers write, or vibe, code every day in Rust, which does provide some intrinsic formal guarantees. When we talk about SPS, we’re imagining something similar, but with much stronger guarantees like “the program eventually terminates”, and “the code is immune to SQL injection attacks” or “IDOR attacks”. The reason Rust doesn’t do this stuff today is because either those problems are undecidable, or we don’t yet have efficient decision procedures for them (more of the former than the latter). But, decidability stops being a concern when we can just whip the language model into proving the theorem.

Until the advent of LLMs, program synthesis was an academic exercise studied by mostly Greek and Israeli professors with grey hair and chalkboards full of difficult-looking model and automata theory. The methods they proposed typically involved zooming in on a really specific kind of programming challenge, defining a mathematical search-space for solutions to said challenge, and then building search algorithms out of the standard arsenal of computer science tools from operations research, statistical learning theory, SAT/SMT, etc. These research projects could be very intellectually rewarding to work on, but due to their necessary and inherent constraints, rarely produced anything practically useful outside of some notable examples in chip design and ...

Secure Program Synthesis

Secure Program Synthesis