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

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

現状の方針

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

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

    • VSTによる検証

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

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

  • 非技術的な動機

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

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

Specification & Proof status

symbol status

wip

実装・証明に取り組み中(未完)

done

完了(以後問題が発覚しなければ)

(empty)

他のタスクを優先中、あるいはブロッキングタスクがあるため手を付けていない
rlsfの関数 実装の移植 形式仕様記述 証明

insert_free_block_ptr_aligned

wip

search_suitable_free_block_list_for_allocation

done

done

map_floor

done

done

wip

map_ceil

done

done

wip

allocate

done

done

deallocate

wip

wip

link_free_block

done

done

unlink_free_block

done

done

  • この表に現れないブロッキングタスク

    • 仕様記述は、実行可能関数に依らないモデル化のタスクによってブロックされている可能性がある

    • Verusの非対応機能に対するworkaround、その他Verusのプラクティス上の問題

    • 補題の証明

Porting Implementaion

Formal Specification

  • ❏ data structure wf-ness

    • ✓ correctness doubly linked list on free block headers

    • ❏ singly-linked list on all headers

  • ✓ bitwise operations

    • ✓ rotate shift

    • ✓ relation between spec mode math & bitwise ops

  • ✓ index calculation

    • ✓ BlockIndex type

    • ✓ state lemmas for uniqueness/existance of block size classes cf. zhang et.al.

Proof

  • ❏ data structure wf-ness

    • ✓ correctness doubly linked list on free block headers

    • ❏ singly-linked list on all headers

  • bitwise operations

    • ❏ lemmas for rotate shift properties

      • ✓ 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

    • ❏ relation between spec mode math & bitwise ops

      • ❏ usize_trailing_zeros_is_log2_when_pow2_given

  • index calculation

    • ❏ uniqueness: index_unique_range

      • ❏ lemma_index_unique_range_fl

      • ❏ lemma_index_unique_range_sl

    • ❏ existance: index_exists_for_valid_size

TODO

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

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

      • ❏ usecase

      • ❏ TCB

      • ❏ about rational_numbers module

    • global directiveの管理

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

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

    • インデックス計算

      • bits

        • ❏ usize_trailing_zeros_is_log2_when_pow2_given

      • rotate_rightの形式仕様

      • 理論的性質

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

        • ✓ 有理数の形式化

      • ❏ optional: 四則演算に関する自動化を整備する e.g. more broadcast

    • メモリ操作

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

      • ❏ Tlsf構造体内の情報に関する証明内追跡用の構造体の設計

        • ❏ realisticなリンクリストの検証PoCを移植する

      • ❏ Deallocation tokenの設計

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

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

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

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

references