アイデアとインサイト

AI ファースト開発、コーディングガードレール、使い捨て前提のアーキテクチャを探求します。

abstract-interpretationstatic-analysismetainfer

Metaはプログラムを実行しない静的解析ツールで本番コードから10万件のバグを発見した

MetaのInferは抽象解釈と双方向誘導を用いて、コードの構造を推論することでヌル参照、メモリリーク、競合状態を検出する。実行は不要だ。仕組みと自社コードベースでの活用方法を解説する。

Metaは、コードがユーザーに到達する前に静的解析ツールが捉えた10万件以上のバグ修正をリリースしてきた。そのツールはInferと呼ばれ、オープンソースであり、コードを実行しない。コードを読み込み、コードが可能な動作の数学モデルを構築し、特定の有害な事象が起こりえないことを証明する。あるいは、それが起こりうる経路を発見…
abstract-interpretationstatic-analysissafety-criticalaviation

静的解析は飛行機が墜落しないことを証明できない。だが、もっと有益なことは証明できる。

抽象解釈はあらゆる可能なプログラム状態を過大近似する。抽象化の中でゼロ除算が到達不可能なら、実際のコードでも到達不可能である。以下に、その仕組みと限界を解説する。

静的解析は、飛行機が墜落しないことを証明することはできない。しかし、高度計の制御ループが決してゼロ除算を起こさないこと、配列の範囲外を決して参照しないこと、固定小数点アキュムレータが決してオーバーフローしないことは証明できる。この区別が重要なのは、一方は物理、空気力学、そして応力下のアルミニウムに関する主張であり、他方…
abstract-interpretationstatic-analysisruntime-errorsverification

コードにランタイムエラーがないことを証明する方法（そして、なぜ諦めるかもしれない理由）

抽象解釈を使えば、実行前にランタイムエラーが発生しないことを証明できる。実際の仕組み、難しさ、そしてツールチェーンでの位置づけを解説する。

テストスイートは通過した。型チェッカーも緑色だ。リリースする。2時間後、本番環境で誰もテストしようとしなかったエッジケースで が発生する。…
hardware-assisted-safetycapability-hardwarecherisoftware-history

ケイパビリティ・ハードウェアは失敗しなかった。40年早すぎただけだ。

1970年代から、ハードウェアレベルでのメモリ安全性は可能だった。なぜケイパビリティ・アーキテクチャがフラット・メモリ・モデルに敗れ続けたのか、そしてなぜCHERIがついに状況を変えているのか。

CVEの70%はメモリ安全性の欠陥である。バッファオーバーフロー、use-after-free、二重解放。不正なJPEGからroot権限への横展開を可能にする、そういった種類の脆弱性だ。…
hardware-assisted-safetysandboxingcwebassembly

C言語の依存ライブラリがプロセス全体をクラッシュさせる。WebAssemblyがそれを防ぐ。

単一のCライブラリを隔離するためにコンテナを使うのは大げさすぎる。WebAssemblyにコンパイルし、WASIサンドボックス内で実行すれば、メモリ安全性、ケイパビリティベースのファイルシステムアクセス、クラッシュ封じ込めをDockerなしで実現できる。

Cライブラリ内でのたった一つのヌルポインタ参照が、アプリケーション全体をクラッシュさせることがある。そのライブラリがユーザー入力を解析したり、画像を展開したり、ネットワークプロトコルを扱うのであれば、一つの異常なパケットがクラッシュを引き起こす危険性がある。コンテナはこの問題を解決するが、一つの依存関係のためにDock…
hardware-assisted-safetymemory-corruptionmobileasan

あなたのスマートフォンはすでにメモリ破損を検出するハードウェアを搭載している

ARM Memory Tagging ExtensionとGWP-ASanにより、最新のモバイルデバイスで本番環境のメモリ安全性検出が可能になった。その仕組みとトレードオフについて解説する。

あなたのスマートフォンは、本番環境でメモリ破損を検出できる。CIで実行する完全なインストルメンテーションを使うわけでも、すべてのアロケーションに適用するわけでもない。しかし、あなたのポケットの中のハードウェアはここ数年、必要なプリミティブを搭載して出荷されており、増え続ける本番アプリが静かにそれを有効にしている。…
hardware-assisted-safetybuffer-overflowmemory-safetycheri

バッファオーバーフローが頻発するのは、我々がソフトウェアで対処しているからだ

CHERIは、すべてのポインタを境界付きcapabilityに変換するハードウェア拡張である。CPUレベルでバッファオーバーフローを阻止する仕組み、コスト、および実機での試用方法を解説する。

バッファオーバーフローは二十年間にわたりCWE Top…
cleanroom-correctnessllmformal-proofsautomation

LLMはコードの正しさを証明できないが、証明のための定型作業は書ける

クリーンルーム検証では、検証条件の生成と解消が必要である。ここでは、LLMがアノテーションとVC生成を自動化し、開発者が実際に難しい証明に集中できるようにする方法を説明する。

クリーンルーム・ソフトウェア工学では、コンパイルする前にコードの正しさを証明することが求められる。それは立派に聞こえるが、10個の整数をソートする関数のループ不変条件を3時間かけて書いていると、そうは思わなくなる。…
cleanroom-correctnessprocessefficiencypragmatism

Cleanroom は 1KLOC あたり 0.1 defect を達成する。フル導入しなくてもそこに到達できる。

Cleanroom software engineering は defect rate を 100 倍に削減するが、フル導入には分離した test team と formal proof が必要。ここでは、overhead なしにその大半の benefit を得られる pragmatism なサブセットを紹介する。

Cleanroom software engineering は 1,000 行あたり 0.1 の defect を達成する。業界平均は 10 から 50 だ。問題は、フルの Cleanroom ではチームを author と verifier に分割し、すべての module の前に formal…