スマートコントラクトの脆弱性対策に向けた形式検証手法の新たなアプローチ
プログラミング言語に形式仕様の構造を直接組み込むことで、スマートコントラクトの開発に革命をもたらし、その脆弱性を根絶できる可能性がある。
プログラミング言語に形式仕様の構造を直接組み込むことで、スマートコントラクトの開発に革命をもたらし、その脆弱性を根絶できる可能性がある。
enum と never 型を用いてゼロコスト抽象化を実現する「タグレスイニシャル」パターンの Rust 実装を深掘りし、最適化されたアセンブリ出力を示します。
分散型取引所(DEX)プロトコルにゲーム理論モデリングを適用し、設計上の弱点や戦略的な攻撃ベクトルを特定する方法を探求します。Uniswap、SushiSwap、Cetus、KyberSwapにおける参加者のインセンティブと戦略について議論し、ゲーム理論がどのようにエクスプロイトを明らかにし、より安全なDEX設計に貢献できるかを解説します。
PhantomData ベースのヒント技法を用いてジェネリクスを自動推論し、カーソルベースの抽象 Method トレイトを定義する方法を解説します。
glibcのような標準ライブラリが大きすぎる、または複雑すぎるリソース制約環境向けに設計された、Newlib、picolibc、nanolib、dietlibcといった特殊なC標準ライブラリを解説します。
本記事では、ローカルメモリポインタと「矢印」ステートメントを活用して抽象的なプログラムを宣言する、先進的な CPS(継続渡しスタイル)の実装例を探ります。
アリーナベースの割り当ては、大きなメモリ ブロックを事前割り当てし、そのブロックから多数の小さなオブジェクトをすばやく切り出すメモリ管理戦略です。
Cランタイム(CRT)は、プログラムが実行されるために必要な初期化ルーチン、ライブラリのサポートコード、システムコールのラッパなどをまとめた仕組みです。本記事では、CRTのスタートアップオブジェクトに含まれる crt0.o、crt1.o、crti.o、crtn.o などのファイルがどのような役割を持ち、なぜ存在するのか、そしてC(およびC++)プログラムがスムーズに動作するためにどのように連携しているのかを解説します。
このブログでは、「計算機科学における論理」という本で説明されている命題論理の基礎を概説します。
レスリー・ランポートによる「TLA+入門」コースのコンスペクトの第2部。