HackMDStarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
モチベ
- mallocは複雑でよく使われてるやつでもバグが多い→形式検証
- おそらく初めての平行性を考慮した高パフォーマンスで互換性のある形式検証されたmalloc実装
方法論
- F*/KaRaMeLでextraction
- Steelという分離論理検証フレームワークで↑の検証
- 実装はGrapheneOSで使われているhardened_mallocを参考にした
評価
- 2-core, 8-thread machine with an Intel® Xeon® CPU E5-1620 0 @ 3.60GHz processor and 12GB memory, using Linux 6.1 and glibc 2.38
- glibcなどの実装といろいろベンチを回している
- redisのベンチが爆発してる
- ページより少し大きい程度のアロケーションが多いかららしい
ある最適化がまだ実装されていないかららしいがそれも難しくないとのこと
- ページより少し大きい程度のアロケーションが多いかららしい
- DieHarderよりは全体的に勝っている
- セキュリティ重視の実装としてはよくやっている？
- 省メモリ指標においても他のセキュリティ重視の実装よりは優秀
- というかhardened_mallocのスコア全部1.0になってておかしい
- FireFoxのmallocとして使ってglibcから12%,もとのhardened_mallocから5%のオーバーヘッド
- 全体として2人年で済んでいる
