TLSFアロケータのdeductive verification

• Rust実装の正当性を保証したい

• 現在やったこと・やっていること 現状

現状の方針

• [DOING] option 1: Verusによる検証を検討中

• option 2: Cのコードベースを検証する

  • VSTによる検証

  • Rustコードベースから使うことを想定しており、 FFIを通じたバグの混入を避けるためRustコードベースの検証を先に検討したい

• RefinedRustの適用を試みる 利用したいRustの言語仕様の多くに未対応なため断念

• 非技術的な動機

  • safety criticalな利用目的なので出来るだけfoundationalな検証を目指したい

  • 自分のスキルセットなどを鑑みて定理証明による手法が使いたい

TODO

• Verusで Tlsf::allocate を検証する

  • ❏ 対象とするユースケースやTCB,証明のためのproof constractなどの設計をまとめたdesign docを作る

  • ❏ DeallocToken の再考: deallocateで前後のブロックを結合する際にヘッダ全体の権限をユーザーが持っていると問題になりそう

  • global directiveの管理

    • プラットフォーム毎に唯一の usize 幅を想定してほしい

    • cfgで公理を含むモジュールのインポートを分岐させる

  • インデックス計算

    • rotate_rightの形式仕様

      • ❏ lemma_usize_rotate_right_0_eq

      • ❏ lemma_usize_rotate_right_low_mask_shl

      • ✓ lemma_usize_rotate_right_mod0_noop

      • ❏ lemma_usize_rotate_right_distr

      • ❏ lemma_usize_rotate_right_reversible

    • 理論的性質

      • ❏ 有理数上の半開区間に移植する

      • ❏ 有理数の形式化

      • ❏ index_unique_range

      • ❏ index_exists_for_valid_size

      • ❏ lemma_block_size_range_mono (optional)

  • メモリ領域の正当性の公理化・伝播

    • Tlsf構造体内の情報に関する証明内追跡用の構造体の設計(各 (.*)Block によるリンクリストの情報など)

    • Deallocation tokenの設計

      • mimallocの検証コードベース内の MimDealloc の調査

• 検証の対象とする性質の検討

  • Rustのアロケータとして要求される仕様について検討する

  • メモリプールの扱い(固定長/動的に拡張可能？)

references

• 現状

• TLSFのインデックス計算に関する正当化

• 検証の対象とする性質の検討

• rlsfに関するメモ

• RefinedRustに関するメモ

• ZhangらによるTLSFの形式仕様に関するメモ

• rr-ex のcoqdoc

• RefinedRust webpage

• rlsf repository

• Iris webpage