Software is infrastructure: failures, successes, costs, and the case for formal verification

ビッグアイデア：ソフトウェアは新しい「コンクリート」である

私たちの道路、橋、発電所が、鉄やコンクリートではなく、目に見えないコードで作られている世界を想像してみてください。著者たちは、ソフトウェアは現代社会のインフラ（基盤）になったと主張しています。橋がトラックを支え、崩落しない必要があるのと同様に、私たちのソフトウェア（病院、銀行、飛行機、さらにはトースターまで動かしているもの）は、完璧に動作する必要があります。

この論文は、シンプルかつ恐ろしい問いを投げかけます。もし橋が不正確な計算に基づいて建てられたら、それは崩落します。もしソフトウェアが不正確な計算に基づいて作られたら、何が起きるでしょうか？ その答えは、数十億ドルが消え去り、人々が傷つき、時には命が失われるということです。

問題点：私たちは「砂の上の城」を築いている

著者たちは、私たちがソフトウェアを物理的なエンジニアリングとは異なるものとして扱っていると指摘しています。

• 壁を築くこと： 壁を築けば、物理学がテストを行います。もし壁が弱すぎれば、塗装する前に重力がそれを倒します。壁が機能するかどうかを確認するために、壁を「実行」することはできません。ただ築き、その数学的根拠が成立することを願うだけです。
• ソフトウェアを書くこと： ソフトウェアは単なるテキストです。バグを「感じる」ことはできません。コードが機能するかどうかを知るには、実行しなければなりません。しかし、コードを実行することは、パラシュートが開くかどうかを確認するために、車を崖から突き落とすようなものです。バグを見つけたときには、すでに衝突（クラッシュ）は起きています。

論文では面白い例を挙げています。もしコンピュータのターミナルで rm -rf ~ と入力したら、あなたのホームフォルダ全体が削除されます。それが危険であることを知るために実行する必要はありません。マニュアル（「数学」）を読めば、それが何をするのか理解できるからです。しかし、複雑なコードの場合、マニュアルを読むだけでは不十分なのです。

「不正確な計算」の代償：1兆ドルの漏れ

論文は、過去40年間のソフトウェアの失敗事例を「恥の殿堂」として挙げ、これらがどれほど高価なミスであったかを示しています。これらはデジタル世界の「橋の崩落」と言えるでしょう。

• Therac-25（ヘルスケア）： コードの不備により、ボタンを素早く2回押すと過剰照射が行われる放射線治療装置。結果： 6名の死亡。
• ロンドン・アンビュランス（緊急サービス）： 新しい指令システムにメモリリーク（穴の開いたバケツのようなもの）がありました。古いデータが溜まり、システムがクラッシュしました。結果： 救急車が患者を見つけられず、20〜30人が死亡。
• ボーイング737 MAX（航空）： MCASと呼ばれるソフトウェアシステムが、単一のセンサーの誤作動に基づいて機首を押し下げました。結果： 2件の墜落事故、346名の死亡、200億ドルの損失。
• ホライゾン事件（銀行）： 不備のある会計システムが、何千人もの商店主に「彼らが金を盗んでいる」と告げました。結果： 900人以上が不当に投獄され、システムの修復に税金が10億ポンド以上費やされました。
• CrowdStrike（グローバルIT）： 極めて小さなアップデートのミスにより、世界中の何百万台ものコンピュータがブルー画面になり、停止しました。結果： 世界的な混乱を招き、ビジネス損失は数十億ドルに達しました。

著者たちの計算によれば、質の低いソフトウェアは、米国経済に年間1兆5600億ドルの損失を与えています。これは多くの国のGDP全体よりも多い金額です。これは、防げたはずのミスを修正するために純粋に浪費されたお金です。

解決策：「数学的な設計図」

論文は、私たちは推測をやめ、実行する前にソフトウェアが機能することを証明すべきだと主張しています。これが**形式検証（Formal Verification）**と呼ばれるものです。

比喩：
あなたが超高層ビルを建てていると想像してください。

• 現在の手法（テスト）： 100階を作り、次に101階、102階を作ります。そしてエレベーターが動くかチェックします。もし102階が崩落したら、すべて壊してやり直します。これは高くつき、危険です。
• 形式検証： コンクリートを一杯流し込む前に、高度な数学を用いて、その設計がどんな重さでも崩れないことを証明します。設計図を物理法則と照らし合わせ、それが完璧であることを確認するのです。

ソフトウェアにおけるこれは、コードがまさに意図した通りに動き、それ以外のことは一切しないことを、数学を使って証明することを意味します。

それは報われるのか？ はい、非常にお買い得です

あなたはこう思うかもしれません。「数学は難しくてコストがかかる。それだけの価値があるのか？」 論文はこう答えます。「はい、間違いなく」。

• 空...