仕様は存在しない (2025)

仕様は存在しない

‍この記事は、フォーマルメソッドの販売でうまくいっていること（そしてうまくいっていないこと） の補足記事です。もともとは2024年末に行った講演 の一部として始まりました。

物事には、難しいものと、単に高価なだけのものがあります。

想像してみてください。エイリアンが我々全員を殺しに来るとします。人類は最高の交渉人を送り込み、エイリアンは、もし我々がGCC の形式検証済みのバージョンを、コードの全ての行を… 1年以内にリリースすれば、恐ろしい襲撃を中止すると発表します。

当然の混乱の後、G7の首脳はグザビエ・ルロワ を呼び出し、莫大な小切手を渡して、彼に任せろと言います。すぐに、世界中の数学者の倉庫で、夜昼なくRocq の定理が証明されます。調整の課題は膨大ですが、彼らはやり遂げます！エイリアンは帰り、グザビエはフィールズ賞、EGOT、そしてノーベル賞すべてを受賞し¹、他の皆はAIの心配に戻ります。

私が言いたいのは、形式検証済みのコンパイラを構築する方法は基本的に知っているということです—既に作成しました。形式検証済みの暗号ライブラリ、パーサー、マイクロカーネルについても同様です。GCCが形式検証されていない理由は、それを行うことが途方もなく高価だからです。コストに見合うだけの利益が得られないでしょう。しかし、もしエイリアンが現れるなら、MCUフェーズ3（22億〜24億ドル）の費用より安くできると bet します。

さて、別の話です。エイリアンが我々全員を殺しに来て、形式検証済みのウェブブラウザを要求します。グザビエが手を挙げます（今回は彼を連れてきました）。そして、「ええと…具体的に何を求めているのですか？そもそも、ウェブブラウザとは、形式的には何なのでしょうか？」と尋ねます。この質問はエイリアンを混乱させ、激怒させます！確かにChromeの形式仕様があるはずですよね？そして、まあ、これで人類は終わりです。

問題は、Chromeやワードプロセッサ、あるいはPDFドキュメント形式のような単純なものでさえ、形式仕様を持っていないということです。これは、まだ誰も書いていないという意味だけでなく、正確で首尾一貫した仕様は書けないと考える理由があるということです。もし2番目の種類のエイリアンが現れたら、私たちはすぐに全く新しいコンピュータサイエンスを考案しなければならないでしょう。MCUのお金でも間に合うかどうか分かりません。

形式仕様は形式的かつ具体的であるべき

そもそもなぜ形式仕様が欲しいのでしょうか（エイリアンはさておき）。

A formal specification says what we want in a precise enough way to serve as a summary or explanation for a system. Rather than examining the system, we can examine the specification instead. This generally doesn’t dictate every single thing about the system (it’s a map, not the territory). For example, the Rust borrow checker guarantees a simple specification, “this program will not generate memory errors.” If you give me a safe Rust program, it might do a lot of things, but it won’t do that.

We need a formal specification if we want to formally verify anything. Otherwise, what are we verifying? Actually doing the verification might mean a warehouse of math grads writing Rocq theorems, or it might mean running the Rust borrow checker. But without a specification, we can’t get started.

Formal methods are old, and people have tried specifying a lot of things. But as a rule of thumb, the most useful formal specifications often have the following characteristics:

• Mathematically clean: we can write the specification in some relatively simple collection of mathematical notions.
• Easy to reason about: we can use the specification as a way of understanding the system, either by human intuition or formal analysis.
• Encapsulated: there’s a clear boundary between the ‘inside’ of the system and the ‘outside’, and the specification describes what happens at this boundary.
• Broadly agreed upon: the designers and users of the system agree it should in fact match the specification—the map is a good description of the territory.
• Stable under change: when the system evolves, the specification doesn’t change too much—the map abstracts away from small differences.

Some systems seem to fit these requirements very naturally—for example, compilers, cryptographic libraries, parsers, and microkernels. We might say these systems are *naturally formalizable.*² If that list looks familiar, you’re right: these are exactly the success stories for formal verification!

I have a hypothesis: once you have a good-quality formal specification, verifying a system is not difficult, merely expensive. And there’s a lot of unsqueezed juice here for formal verification fans. Compilers, microkernels, and the rest are security-critical components, but almost no such system we use today is formally verified. Call the G7, it’s time, let's verify GCC! *

Wait, no, there’s more. Some people look at CompCert and SeL4 and ask, “why can’t we formally verify my system?” Well, I think naturally specifiable systems are a tiny and very unrepresentative niche. Out in the wild, most systems are very un-specifiable, and that’s a big problem if we want to formally verify a lot more of the world.

実際には、仕様が多すぎる

形式仕様がないかもしれませんが、開発者は常に非形式的な仕様を書いています。システムには、重要な情報を持つさまざまな種類の仕様が存在する可能性があります。

• Prose documentation - internal-facing design documents, external-facing user manuals and guides, and also white papers, RFCs, and similar.
• Slide decks - astoundingly common, especially in the US Government.
• The system itself - especially for a legacy system, the system may ‘do what it does’ and any change is by definition against specification.
• User stories - for a user-facing application like a web browser, the set of user stories might be the real top-level specification, but it's typically very hard to express these formally.
• Unit and integration tests - often the closest thing to a formal specification, but restricted to a single input or scenario.
• Many many other things, including reference implementations, inline comments, tacit / practical know-how in the team, customer preferences, regulatory requirements, scribbled notes on coffee-shop napkins…

In fact, there are too many partial specifications, with incomplete coverage, none of which match each other. When I’m scoping projects for Galois clients, I’ve often had this kind of conversation:

              Me: “Do you have a specification for [your giant system]”

              Client: “Yes, here’s a two-slide powerpoint deck”

                 ~ and/or ~

              Client: “Yes, here’s a 7000-page requirements document in semi-structured prose”

All of which leads to this kind of conversation, when trying to formally verify the system in question:

              Me: “We found the system does [something] but your specification implies [something else].”

              Client: “Oh, huh, that doesn’t matter”

                    ~ or ~

              Client: “Yeah, we changed that 6 months ago”

After a person has this conversation about 40,000 times, I find they consider retraining as a circus clown or just throwing themselves in the river.

You can also try sitting down with clients and writing formal specifications:

              Me: “Do you want the specification to allow [some behavior]?”

              Client: “Er… I don’t know, I haven’t thought about that situation”

              Me: “If you allow it, you’ll also have to permit [some other behavior]. Does that matter?”

              Client: “I don’t know about that situation either… how long is this going to take?”

I’ve come to think writing formal specifications is just a very difficult task. It requires a top-down view of the system that designers and engineers typically don’t have or, more importantly, need. In contrast, informal specifications can be ambiguous, partial, flexible. Informal specifications are intended as communication mechanisms between humans, and as a result they can be ‘wrong but useful’, and elide aspects of the system that are not of interest. This is a strength, but it also results in systems that can’t be easily formalized.

I think systems are typically both designed from the top and grown incrementally. Most systems have some degree of top-down structure, but few systems have a mathematically coherent specification that covers every behavior. The effect is that most systems obey some formal specification for some core functionality, but if outside this core, we rapidly enter muddy territory where it is unclear what the system should do, or whether the designer should even care.³

Le PDF n’a pas eu lieu⁴

Let’s dig into a particular example, the Portable Document Format, PDF. In many ways, this should be an easy case for specification. After all, a PDF isn’t some esoteric thing - you can download one and open it on any one of a billion devices. PDF also has a well-maintained standard developed by the PDF Association, a huge body of examples, and many many implementations, ranging from hobbyist projects to security-critical systems.

But even so, PDF does not have a consensus about what implementations should do, nor does it have a specification that matches the behavior of existing implementations, nor a clear definition of a bad or insecure document. As a result, it seems impossible today to write a precise and coherent formal specification for PDF.

In a large PDF dataset, we will have some examples that are known-bad—ill-formed in a way designed to elicit some vulnerability—and some that are known-good, in that they conform tightly to the standard. But we also have a large number (the majority in fact) where all that we can do is shrug. They might be good or bad, we just don’t know.

［画像: 둠のポテト］

We called this diagram "the potato of doom"

This seems like an absurd situation, what’s going on? One reason for this is that PDF readers have an incentive to parse as many documents as possible. If you receive a PDF and it doesn’t open, you’re likely to blame the PDF reader, and not the program that created the document. To avoid this, every PDF reader tries to fix up mistakes in non-standard documents, and all of them do it slightly differently. The same non-standard document might get interpreted two different ways by different PDF readers.

I feel like Jacques Derrida writing this, but the result is that PDF does not exist, at least in the sense of a discrete category that can be formalized. Instead, there’s a fuzzy boundary where something might or might not be considered a PDF. That wouldn’t be so bad, except that a large proportion of actual PDFs exist in this liminal region!

［画像: PDFの曖昧な境界］

‍

On the DARPA SafeDocs project, Galois spent several years working on formalizing PDF. We worked closely with the PDF Association using a new language we built for the purpose, DaeDaLus. I’m proud of the work we did, but at the end of the project, our formal PDF specification was non-descriptive (it differs from real PDF readers), non-normative (it doesn’t characterize what we think should be correct behavior), and it’s unclear how to get to a more rigorous and accepted specification.

You can read about Galois’s work on PDF here, and you can read about DaeDaLus, the language we built to help describe document formats, here.

結論：意図した通りに実行する

xkcd 568 の画像

xkcd 568。ライセンス: CC BY-NC 2.5

Okay here’s another story: the current era of formal verification has been dominated by the cost of proof. Specification has taken second place—we can’t even verify systems with simple specs, so why worry about everything else? Now, thanks to advances in modern AI, we may soon live in a strange world where proofs are cheap and abundant. If that happens, I think we will quickly verify every compiler and microkernel, then find that we’re stuck. Even Claude can’t tell us what to want.

Formal verification today is very useful, but for most systems it’s very difficult to write the kinds of complete specifications that verification needs. However, other kinds of specifications are popular: for example, a test case is a kind of limited, partial specification. The key is that a test case is immediately useful, and doesn’t impose undue costs on the development team. We need to find ways to specify systems that have these virtues, and avoid the trap of imposing a complete and coherent view that fundamentally does not exist.

It’s a formal verification cliché that writing the specification tends to uncover most of the bugs in a system. To me, this suggests an analogy between specification and programming—both are tools for expressing what we want. In one way, this is a pessimistic thought: no tool can remove the burden of clarifying our ideas. But also, it gives me some hope. Programming is very difficult, but through careful tool design, we’ve made it available to hundreds of millions of people. With luck and skill, perhaps we can do the same for specifications.

We’re just getting started. There’s a lot to do. And we need to keep our eye out for those aliens.

‍

‍

¹ Not the fake one for Economics
² I don’t want to undersell the work it took to invent the specification technologies we have now. The systems that are naturally specifiable are only so with the specification tools of today, which represent half a century of concerted work
³ Ah-ha, you say, what we should do is insist that engineers build every system starting with a rigorous formal specification. In most cases, I’m skeptical this would pass the cost/benefit test
⁴ Avec toutes mes excuses à Jean Baudrillard