← すべての記事

数学的な「証明」が投票を正しく集計したことを示す — 秘密の裏口が組み込まれている

スイスは電子投票システムのソースコードを公開して誰もが検査できるようにしました。数週間以内に、暗号学者たちは、内部関係者が数学的に有効な証明を作成しながら、投票をひそかに改ざんすることを可能にする裏口を発見しました。

2019年春のことです。スイス・ポスト社のオフィスのどこかで、急進的な透明性に見える決定が下されようとしていました。スペインのベンダーであるScytlと協力した連邦郵便事業局は、スイスのインターネット投票システムの完全なソースコードを公開しようとしていたのです。要約ではありません。パンフレットでもありません。実際のコード — あらゆる行 — 世界中がそれを読み、攻撃し、判定するために公開されるのです。

これは議論に決着をつけるはずの瞬間でした。

スイスはインターネット投票をめぐって何年も争ってきました。批評家たちはブラックボックスを信頼できないと言っていました。関係者はシステムが検証され、監査され、認証されていると言いました。そこでスイス・ポストはほぼ世界中のどの選挙当局も敢えてしたことのないことをしました。それはボックスを開けることでした。見に来てください、と言ったのです。隠すものは何もありません。

3人の独立した研究者 — Sarah Jamie Lewis、Olivier Pereira、Vanessa Teague — はスイス・ポストの言葉を信じました。彼らは見ました。

彼らが見つけたものは不可能だったはずです。

何も証明しなかった証明

Lewis、Pereira、Teagueが発見したものを理解するには、システムが何をすると主張していたのかを理解する必要があります。

インターネット投票には根本的な問題があります。投票者がインターネット経由で投票を提出するとき、誰が — 投票者自身も含め — それが正しく集計され、ネットワークの途中のサーバーによって別の投票に置き換えられていないことを確認できるのでしょうか？暗号学者が開発した答えは mixnet または mix network と呼ばれるものです。投票は暗号化されて入ってきます。システムはそれらをシャッフルします — デッキをカットするように — そしてその後、重要なことに、シャッフルが正直であったことを証明する数学的な証明を公開します。つまり、投票を周りに移動させましたが、そのいずれも変更していません。

この証明はシステムの検証可能性の中核的な主張です。適切なソフトウェアを持つ誰もがそれをチェックできます。証明が通れば、投票は完全です。証明が失敗すれば、何か問題があることがわかります。

しかし、証明自体に仕掛けられた裏口がありました。

Lewis、Pereira、Teagueは彼らの発見を — マグリットへの敬意を込めて — Ceci n'est pas une preuve（「これは証明ではない」）というタイトルの論文で記録しました。彼らは、スイス・ポスト–Scytlシステムのシャッフル証明がtrapdoor commitment scheme（裏口約束スキーム） を使用していることを発見しました。これは、通常の条件下では正直に機能する数学的構造ですが、隠された値のセット（裏口）を知っていれば、それを利用することができるものです。これらの値を持つ権限のある者は、すべての検証チェックを通過するシャッフル証明トランスクリプトを生成することができ、その一方で実際には投票を改ざんしていたのです。

それをゆっくり読んでください。証明は通る可能性があります。数学はチェックアウトします。すべての監査者のソフトウェアは検証済みと言うでしょう。そして投票は間違っていることになります。

これは理論的なこじつけではありませんでした。これはシステムが整合性の保証として提供していた仕組みの中に組み込まれた機能的な裏口でした。あなたが集計を確認するために見ることになっていたものが、偽造される可能性のあるものだったのです。

「検証可能」が本当に必要とするもの

スイス・ポストとScytlは発見を認めました。スイス当局は修復の保留中に電子投票システムを中止しました。不完全なシステムで結合選挙は実行されなかったため、投票が実際に改ざんされることはありませんでした。しかし、このエピソードは、すべての選挙技術の主張が答える必要がある問題の骨にメスを入れます。

誰にとって検証可能か？

システムは数学的証明を提供することができ、それでも嘘をついている可能性があります — 証明の構造自体に、システムの操作者のみが引く方法を知っている秘密のレバーが含まれている場合です。スイス・ポストシステムは単に安全であることを主張しただけではありませんでした。それはuniversal verifiability（普遍的検証可能性） を提供することを主張しました。つまり、公開されたデータで武装した誰もが、単一の権限を信頼することなく、投票が正しく集計されたことを確認できるという保証です。その主張は偽りでした。検証は権限が誠実に行動した場合にのみ実際でした。それはまさに検証可能性が防ぐべきものです。

ドイツ連邦憲法裁判所は10年前の2009年の判決で、公が独立して検査できない投票機を禁止した際にこのロジックを理解しました。裁判所は投票および結果の決定の本質的なステップは、市民によって確実かつ専門知識なしに検査可能でなければならない と判示しました。完璧さを求めていたわけではありません。専門家でない人が追うことができるものを求めていたのです。訓練された研究者だけが分析できる暗号証明は、すでにその標準から一歩離れています — そして裏口化されたスキームが生成する証明は、証拠を装いながら積極的に誤解させるため、証明がないよりも悪いのです。

スイス・ポストのケースはより深い問題を示しています。「私たちを信じてください」と言うブラックボックスシステムは明らかに信仰を求めています。しかし、「数学をチェックしてください」と言い、その数学に裏口を組み込んでいる公開コードシステムは、同じ信仰を求めており、それを証拠として偽装しているのです。検証可能性の外観は不透明性の認容よりも危険です。なぜなら、それは問題を排除するからです。

オープンコードが認証が見逃した欠陥を見つけた方法

保持する価値のあることがあります。欠陥はコードが公開されたために発見されたということです。

スイス・ポストはそのソースを開く必要はありませんでした。ほとんどのベンダーはそうしません。ほとんどの民主主義に存在する認証機構 — 米国ではElection Assistance Commissionの任意投票システムガイドライン、他の管轄区では国家試験機関 — は、専門家が管理された条件下、しばしば秘密保持契約の下でシステムを検査することを含み、彼らの調査結果は要約されますが、常に公開されるわけではありません。検査官が「我々がそれをテストしてそれは通過した」と言う場合、公開はその検査官を信頼しているのです。推論は隠されています。

スイス・ポストがコードを公開したとき、それは別の種類の検査を可能にしました。敵対的、独立的、無制限の検査です。Lewis、Pereira、Teagueはスイス・ポストからお金をもらっていません。彼らは秘密保持契約を持っていません。彼らは読んで異議を唱える者が誰でもいるように、引用と方程式を含む彼らの完全な分析を公開しました。これは認証プロセスではありません。これは科学的なプロセスです — そして認証プロセスが見つけなかったものを見つけました。

これら2つのプロセス間のギャップを正確に命名する価値があります。認証は、システムが予期された条件下で正しく動作するかどうかをテストします。独立した暗号レビューは、システムの主張された保証が敵対的条件の下で成り立つかどうかをテストします — システムの操作者が敵対者である場合を含めて。その2番目の質問が最も重要で、オープン公開のみが許可する質問です。

2010年のDCインターネット投票トライアルと比較してください。ミシガン大学のチームは、管轄区がシステムを実際の投票がキャストされる前に公開テストに開放したため、約48時間以内に公開投票パイロットのほぼ完全な制御を得ました。脆弱性は誰かが攻撃することが許可されたため見つかりました。または2015年のニューサウスウェールズiVoteシステムを検討してください。研究者たちは、すでに約280,000票を集めていたライブ選挙で深刻な欠陥を見つけました — 選挙前のセキュリティレビューでクリアされていた欠陥です。各ケースで、発見は公式プロセスからではなく、外部からの発見でした。

パターンは続きます。オープン検査は閉じられた認証が見逃したものを見つけます。 常にではありません。自動的ではありません。しかし一貫して十分なため、証拠の負担はシフトする必要があります。当局が「それを認証しました」と言うとき、尋ねるべき質問は。誰によって認証されたのか、どの脅威モデルに対してなのか、どのようなアクセスで、そして調査結果はどこで公開されているのか？

カテゴリ問題としての裏口

スイス・ポストシステムの特定の欠陥 — 暗号証明の裏口 — は、通常の意味での実装バグではありません。バッファオーバーフローまたは誤って設定されたサーバーではありません。これらはエラーです。これは数学的構造の設計上の選択、または最小限度の設計の失敗であり、システムの検証可能性の保証がそれに基づいていました。

この区別が重要なのは、それがテストの限界についてあなたに何かを教えてくれるからです。ソフトウェアシステムを無期限に任意のバグについてプローブすることができますが、それでも裏口約束スキームを見逃す可能性があります。なぜなら、スキームは外側から正しく機能する — それは正しく形成された出力を生成し、正しく形成されたチェックを通過するからです。欠陥は数学的仕様を調べて、使用された約束スキームが設計者が知らなかった、または開示しなかった特性を持っていることに気付かない限り、見えません。

これが選挙における暗号検証可能性の議論が「私たちはコードを公開しました」で止まることができない理由です。それは次のように拡張する必要があります。数学的証明構造自体が、ベンダーまたは権限ではない、そして問題を認証するよりも見つけることに動機付けられている人々によって独立して監査可能でなければなりません。

Lewis、Pereira、Teagueは問題を見つけることに動機付けられていました。彼らはそれを見つけました。これはスイス・ポストの意図の告発ではありません — 会社は発見を認め、それを修正するために移動しました。これは発見を生み出したプロセスのための議論です。

「監査がそれを確認した」が開いたままにするもの

スイス・ポストシステムが中止されたとき、公務員は言うことができました。プロセスは機能しました。欠陥が見つかり、展開が停止され、修復が続くでしょう。狭い意味で、それは本当です。しかし、コードが公開されていなかった場合に何が起こったかを自問する価値があります。

答えは、同じ証明が実行され、同じトランスクリプトが生成され、それらをチェックする人は見たでしょう。検証済み。認証は通過しました。公務員は次のように言ったでしょう。システムは監査されました。公開は知る方法を持たなかったでしょう。証明は何も証明していません。

独立して検査できない検証可能性の主張は、検証可能性がまったくないことと区別がつきません。 これは電子投票に固有の批評ではありません。選挙システムのあらゆる正確性の主張に適用されます — 紙の集計も含めて。ジョージア州の2020年の約500万票の手動集計は、機械が集計した結果をほぼ10分の1パーセント以内で確認しました。これは素晴らしいです。しかし、それは独立して検査することができる耐久性のある紙の投票の存在に依存していました。初めて数えた機械を信頼することではなく。紙は独立したチェックでした。あなたが実際に検査できた証明。

スイス・ポストのケースは暗号の等価物です。コードは公開されると紙でした。そして紙は証明が虚構であることを示しました。

本当にチェック可能にするもの

スイス・ポストのエピソードは、暗号的に検証可能な選挙の場合を終わらせません。それは、その場合が実際に何を必要とするかを定義します。

シャッフル証明は正しい種類のメカニズムです — 投票がネットワーク中に改ざんされなかったことの数学的保証であり、それを検証するソフトウェアを持つ誰もがチェック可能です。しかし、その保証が実装される代わりに実際であるために、いくつかの条件が同時に成り立つ必要があります。

第一に、暗号スキームは裏口値を含まないはずです。 これは数学的要件です。シャッフル証明で使用されるコミットメントスキームは、裏口なしでバインディングおよびハイディングである必要があります。この条件を満たす十分に理解されたスキームがあります。どれを使用するかの選択はベンダーの詳細ではなく、公開設計の質問です。

第二に、証明は結果に利害関係を持たない当事者による独立検証可能である必要があります。 ただ1つの認証研究所ではなく。複数の独立した暗号学者が、完全な仕様と実装を持ち、公開批評のために彼らの調査結果を公開しています。

第三に、投票者から最終集計までのエンド・ツー・エンドのチェーンは、チェーン内の単一のポイントを信頼することなく監査可能である必要があります。 インターネット投票をキャストした有権者は、彼らの暗号化された投票がミックスに含まれていることを確認することができるはずです。どの観測者も、ミックスが正直であることを確認することができるはずです。そして最終的な復号化は独立して再現可能である必要があります。これらのステップのいずれも、権限の協力または誠実さに依存すべきではありません。

第四 — そしてこれが最も難しいです — 検証プロセス自体がドイツ憲法裁判所の標準を満たすのに十分アクセス可能でなければなりません。つまり、専門家暗号学者だけでなく、一般市民も本質的なステップを確認できる必要があります。 それには、現在のシステムが提供するものをはるかに超えるソフトウェアツール、インターフェース、およびドキュメントが必要かもしれません。

これらの条件のいずれもが、2019年のスイス・ポストシステムによって完全に満たされていました。そのうちのいくつかは、世界のどの現在展開されている選挙システムによっても満たされていません。それは正直な立場です。スイス・ポストのケースは、見つかって修正された欠陥についての物語であり、今ではすべてが問題ないというわけではありません。これは、外部者が問題を見つけるために十分なものを公開するときに何が起こるかについての物語です — そして、発見が展開の前に体系的に起こることができるために出版するのに十分なものが何であるかについてです。独立した研究の幸運な偶然としてではなく。

悪役はあなたがチェックできない証明です

1つのスイスベンダーのシャッフル証明の特定の裏口は、ポイントではありません。ポイントは主張のカテゴリです。数学的に正しいことが証明された、外部検査を排除する形で提供されています。すべての選挙システムが主張を立てます。ベンダーが認証を主張します。公務員が監査を主張します。暗号学者が検証可能性を主張します。これらの主張のすべてが、独立した部外者がそれを確認または反論することを可能にするメカニズムと同じくらい強いです。

そのメカニズムがブラックボックスである場合、主張はボックスを作った人への信頼に基づいています。コードが公開されている場合、主張は少なくとも精査することができます — そして時には反論することができます。公開された暗号証明で、裏口のあるスキームを使用している場合、それは検証可能性のパフォーマンスです。物質のない物の外観。

スイス・ポストの物語の悪役はスイス・ポストではなく、Scytlでもありません。それは透明性を装った不透明性 — チェック可能に見えますが、そうではない証明です。修正は、暗号検証可能性をあきらめることではなく、その実際のバージョンを要求することです。裏口のないスキーム、秘密保持契約のないレビュー、独立した研究者がチェックでき、必要に応じて反論できる証明。

それはTrustVotingが向かっていることです。誰もが検査できる形で証拠が公開されているため、誰もが正確性を信仰に基づいている必要がないシステム。「それを監査しました」ではなく。「数学がチェックアウトしました」ではなく。ここに数学があります。自分でチェックしてください。

共有可能なバージョン： スイスはそれが信頼できることを証明するために電子投票コードを公開しました。研究者たちは、投票を変更しながら有効な証明を偽造することを可能にする裏口を見つけました。証明は通りました。投票は間違っていたでしょう。「検証済み」は、独立した誰かが検証することを許可され、「いいえ」と言うことができる場合にのみ意味があります。

まだチェック不可能なもの。他の現在展開された暗号電子投票システムが同様の問題のあるコミットメントスキームを使用しているかどうか、およびそれらのシステムが通過した認証プロセスが公開された調査結果を伴う敵対的独立暗号レビューを含んでいるかどうか。そのレビューが存在し、その結果が公開されるまで、「システムは認証されました」は依然として主張であり、証明ではありません。

それをチェック可能にするもの。暗号仕様とソースコードの完全な公開、NDAsなしの独立した複数当事者のレビュー、および公開された調査結果 — 否定的なものを含む — 結合選挙が実行される前に。

世界中のこの検証ギャップがどのように一般的であるかを見る →

この問題の2分間バージョンを読む →

検証不可能な選挙結果の文書化されたケースを調べる →

出典

すべての記事を表示ギャップを探索