2026年8月5日 Metaはプログラムを実行しない静的解析ツールで本番コードから10万件のバグを発見した MetaのInferは抽象解釈と双方向誘導を用いて、コードの構造を推論することでヌル参照、メモリリーク、競合状態を検出する。実行は不要だ。仕組みと自社コードベースでの活用方法を解説する。 abstract-interpretationstatic-analysismetainfer
2026年8月4日 静的解析は飛行機が墜落しないことを証明できない。だが、もっと有益なことは証明できる。 抽象解釈はあらゆる可能なプログラム状態を過大近似する。抽象化の中でゼロ除算が到達不可能なら、実際のコードでも到達不可能である。以下に、その仕組みと限界を解説する。 abstract-interpretationstatic-analysissafety-criticalaviation
2026年8月3日 コードにランタイムエラーがないことを証明する方法（そして、なぜ諦めるかもしれない理由） 抽象解釈を使えば、実行前にランタイムエラーが発生しないことを証明できる。実際の仕組み、難しさ、そしてツールチェーンでの位置づけを解説する。 abstract-interpretationstatic-analysisruntime-errorsverification
2026年8月2日 Cコードを全面的に rewrite しなくても、キャパビリティハードウェア上で動作させられる CHERIのハイブリッドABIを使えば、Cコードを段階的にキャパビリティハードウェアへ移植できる。コンパイル方法、どこが壊れるか、そして codebase 全体を rewrite せずに修正する方法を解説する。 hardware-assisted-safetychericporting
2026年8月1日 ケイパビリティ・ハードウェアは失敗しなかった。40年早すぎただけだ。 1970年代から、ハードウェアレベルでのメモリ安全性は可能だった。なぜケイパビリティ・アーキテクチャがフラット・メモリ・モデルに敗れ続けたのか、そしてなぜCHERIがついに状況を変えているのか。 hardware-assisted-safetycapability-hardwarecherisoftware-history
2026年7月31日 C言語の依存ライブラリがプロセス全体をクラッシュさせる。WebAssemblyがそれを防ぐ。 単一のCライブラリを隔離するためにコンテナを使うのは大げさすぎる。WebAssemblyにコンパイルし、WASIサンドボックス内で実行すれば、メモリ安全性、ケイパビリティベースのファイルシステムアクセス、クラッシュ封じ込めをDockerなしで実現できる。 hardware-assisted-safetysandboxingcwebassembly
2026年7月30日 あなたのスマートフォンはすでにメモリ破損を検出するハードウェアを搭載している ARM Memory Tagging ExtensionとGWP-ASanにより、最新のモバイルデバイスで本番環境のメモリ安全性検出が可能になった。その仕組みとトレードオフについて解説する。 hardware-assisted-safetymemory-corruptionmobileasan
2026年7月29日 バッファオーバーフローが頻発するのは、我々がソフトウェアで対処しているからだ CHERIは、すべてのポインタを境界付きcapabilityに変換するハードウェア拡張である。CPUレベルでバッファオーバーフローを阻止する仕組み、コスト、および実機での試用方法を解説する。 hardware-assisted-safetybuffer-overflowmemory-safetycheri
2026年7月28日 LLMはコードの正しさを証明できないが、証明のための定型作業は書ける クリーンルーム検証では、検証条件の生成と解消が必要である。ここでは、LLMがアノテーションとVC生成を自動化し、開発者が実際に難しい証明に集中できるようにする方法を説明する。 cleanroom-correctnessllmformal-proofsautomation
2026年7月27日 Cleanroom は 1KLOC あたり 0.1 defect を達成する。フル導入しなくてもそこに到達できる。 Cleanroom software engineering は defect rate を 100 倍に削減するが、フル導入には分離した test team と formal proof が必要。ここでは、overhead なしにその大半の benefit を得られる pragmatism なサブセットを紹介する。 cleanroom-correctnessprocessefficiencypragmatism
