Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
F*でプログラムの正しさを証明する
Search
Ushitora Anqou
August 08, 2021
Technology
1
1.2k
F*でプログラムの正しさを証明する
セキュリティ・キャンプ全国大会2021 オンラインで行われたLT用のスライド資料です
Ushitora Anqou
August 08, 2021
Tweet
Share
More Decks by Ushitora Anqou
See All by Ushitora Anqou
Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
anqou
1
930
「自作CPUでサイゼリヤ問題」を支える技術
anqou
2
350
ぼくのかんがえたさいきょうのマリオAI
anqou
1
580
10ステップで作るお手軽インタプリタ開発
anqou
3
1.1k
seccamp2018でセルフホストCコンパイラをつくった
anqou
8
5.5k
Other Decks in Technology
See All in Technology
やる気のない自分との向き合い方/How to Deal with Your Unmotivated Self
sanogemaru
1
520
生成AI時代のセキュアコーディングとDevSecOps
yuriemori
0
130
AWS Control Tower に学ぶ! IAM Identity Center 権限設計の第一歩 / IAM Identity Center with Control Tower
y___u
1
200
Codexとも仲良く。CodeRabbit CLIの紹介
moongift
PRO
1
250
CoRL 2025 Survey
harukiabe
1
220
Contract One Engineering Unit 紹介資料
sansan33
PRO
0
8.9k
組織改革から開発効率向上まで! - 成功事例から見えたAI活用のポイント - / 20251016 Tetsuharu Kokaki
shift_evolve
PRO
1
150
Introdução a Service Mesh usando o Istio
aeciopires
0
220
なぜAWSを活かしきれないのか?技術と組織への処方箋
nrinetcom
PRO
5
990
『バイトル』CTOが語る! AIネイティブ世代と切り拓くモノづくり組織
dip_tech
PRO
1
130
All About Sansan – for New Global Engineers
sansan33
PRO
1
1.2k
ガバメントクラウドの概要と自治体事例(名古屋市)
techniczna
3
240
Featured
See All Featured
Practical Orchestrator
shlominoach
190
11k
Large-scale JavaScript Application Architecture
addyosmani
514
110k
Build your cross-platform service in a week with App Engine
jlugia
232
18k
Cheating the UX When There Is Nothing More to Optimize - PixelPioneers
stephaniewalter
285
14k
Typedesign – Prime Four
hannesfritz
42
2.8k
StorybookのUI Testing Handbookを読んだ
zakiyama
31
6.2k
Improving Core Web Vitals using Speculation Rules API
sergeychernyshev
21
1.2k
The Psychology of Web Performance [Beyond Tellerrand 2023]
tammyeverts
49
3.1k
[RailsConf 2023 Opening Keynote] The Magic of Rails
eileencodes
31
9.7k
Done Done
chrislema
185
16k
How to Think Like a Performance Engineer
csswizardry
27
2.1k
Refactoring Trust on Your Teams (GOTO; Chicago 2020)
rmw
35
3.2k
Transcript
F⋆ でプログラムの正しさを証明する 艮 鮟鱇(@ushitora_anqou) 2021 年 8 月 9 日
1
あなたが書いたそのプログラム、正しいですか? テストはプログラムの正しさを保証しない • テストした値では正しいと言える(かも) • テストしていない値では? • 入力値は加算無限個ある プログラムが「数学的に」正しいことを示したい •
プログラムの正しさを「証明」する • どんな入力に対しても正しく動作することを保証する プログラムの証明を人力でチェックする⋯⋯? 2
形式証明 証明の正しさを機械的に検証する • 証明を特殊なプログラムとして記述し、コンパイラに入力 • (コンパイラが間違っていなければ)コンパイルが通ると証 明が正しいことが分かる • こういうコンパイラを「証明支援系」と呼ぶ 背後には
Curry-Howard 同型対応などの理論がある⋯⋯ • ⋯⋯が今回は省略 • 気になる人は「計算と論理」で検索して五十嵐先生のスライ ドとかをチェック 3
F⋆ 最近出てきた証明支援系 • Microsoft Research や INRIA が作っている(2016 年~) •
依存型・篩型・エフェクトなどの格好いい機能がある • 証明をある程度省略して書いてもいい感じに推論して検証 してくれる • プログラミング言語 OCaml に酷似した文法 今日の主役 4
F⋆ 使われています HACL*:F⋆ で検証された暗号ライブラリ • TLS の実装を F⋆ で検証することを目標にしている(Project Everest)
• Firefox(ブラウザ)や Wireguard(VPN)や Tezos(暗号通 貨)に組み込まれている Plebeia:暗号通貨 Tezos 用のストレージシステム • F⋆ で実装が正しいことを保証 • 現在絶賛開発中 5
本日のお題:フィボナッチ数列 前項と前々項の和でできる数列 an =
1 (n = 0, 1) an−1 + an−2 (n ≥ 2) an = 1, 1, 2, 3, 5, 8, 13, . . . (n = 0, 1, 2, . . . ) 定理 n = 2, 3, 4, . . . について an ≥ n 6
日本語での証明 n に関する数学的帰納法により証明する。すなわち 1. a2 ≥ 2 かつ a3 ≥
3 を示す。 • 定義より a2 = 2 ≥ 2 かつ a3 = 3 ≥ 3 なのでこれは成り立つ。 2. 任意に n = 4, 5, 6, . . . をとり、an−2 ≥ n − 2 かつ an−1 ≥ n − 1 を仮定して an ≥ n を示す。 an = an−1 + an−2 (定義より) ≥ (n − 1) + (n − 2) (帰納法の仮定より) = (n + 1) + (n − 4) ≥ n + 1 (n ≥ 4 より) 7
F⋆ で証明する:fibの定義 まずフィボナッチ数列を計算する関数 fib を定義 8
F⋆ で証明する:定理の宣言 続いて示したい定理を宣言 定理 n = 2, 3, 4, .
. . について an ≥ n 9
F⋆ で証明する:証明をプログラムとして定義 何を書けばよいか • F⋆ は証明のかなりの部分を自動化してくれる • しかし帰納法をどう行えばよいかはまるっきり分からない • より具体的には「帰納法の仮定をどう使うか」
• 人間がヒントとして帰納法の仮定の使い方を教える必要 • プログラム上では再帰関数呼び出しとして表現される 10
F⋆ で証明する:証明をプログラムとして定義 11
F⋆ で証明する:検証結果 fstar.exe に食わせると証明が正しいことを検証できる F⋆ コードを OCaml コードに変換(コード抽出)することで、検 証された fib
関数を実行することができる • 今回は省略 12
Let’s write F⋆! 13