FWS2024
形式検証とセキュリティ
ワークショップ

F*ハンズオンのページ

FWS企画の「F*ハンズオン」についてのページです．

資料


テキスト
スライド

サンプルコード


※保存の場合は 右クリック→「リンク先を別名で保存」
※実際のF*のファイルの拡張子は.fstですが，見やすさのためにテキストファイルで置いてあります．必要に応じて拡張子を変更してください．

基礎編

  • 演習2.1（TypesAndFuncs.fst）
  • 演習2.1 参考解答
  • コード1: アクセスポリシーのリスト（ACLs.fst）
  • コード2: ファイルアクセスプリミティブ（FileIO.fst）
  • コード3: クライアントコードの例（ClientCode.fst）
  • 演習2.2 参考解答
  • 演習2.3 参考解答（ClientCodeNG.fst）
  • 基礎編のコードを全部くっつけたコード（演習の参考解答入り，てっとり早く出力を見たい方向け）

    • 応用編

  • コード5: マークルツリーの定義（MerkleTree.fst）
  • コード6: データアクセス関数の定義（MTAccess.fst）
  • コード7: 証拠付きデータアクセス関数の定義（MTAccessEvidence.fst）
  • 演習3.2 参考解答
  • コード8: 証拠を検証する関数の定義（VerifyEvidence.fst）
  • 演習3.3 参考解答
  • コード9: 安全性の証明（ProofSecurity.fst）
  • 応用編のコードを全部くっつけたコード（演習の参考解答入り，てっとり早く出力を見たい方向け）

    • 各種リンク


    F* Online Tutorial
    F*公式ページ
    Proof-Oriented Programming in F*（公式のチュートリアル資料）
    F*における検証されたプログラミング（公式のチュートリアル資料，一部日本語）