Reachability Logic
Kでの形式的検証
https://gyazo.com/2aca544bbac8b90f3c4b6007f250aa41
様々なoperational semanticsに対して適当できるフレームワーク構築
operational semanticはterm rewritingとして与える
a symbolic model checker equipped with coinductive reasoning about loops and recursions
Language-independent
Operational Sementicsを公理とする
in-code annotationはまだサポートされていない
https://gyazo.com/675a309927c42fbc68a317a5132a715d
https://gyazo.com/7c548f5464254efdcfe1d87fa1ea6b02
Mathemetical domains
map, stacks, tree
Matching logic
patternはvariables, symbols, connectives and quantifiersにより成る
関数と述語のsymbols
Separation Logicとの違い
新たな結合記号(*)を導入しなくても、termのレベルで分離を実現できる
heapに限らず全てのレベルのconfigurationを分離できる
一階述語論理の範囲内、拡張していない。よって、既存のSMTソルバが使える。
Frame separation logic over a map model
推論体系
ヒルベルト流
参考
後半からMatching Logicについて書かれている
Reachability logic
Rewriting is both the execution mechanism and the reasoning model in K, with all KEVM rules and proof properties expressed as rewrites over the configuration.
言語のsemanticによりinstantiateされる
https://gyazo.com/c8f6dff9f833a302a096b8f40c408ad3
Aはaxioms, Cはcircularities
Reachability ruleのセット
最初はどちらもempty(∅), A, Cという文字が省略されている場合はこれのこと。
相対的完全性
健全性と合わせ、Hoare Logicと異なり、言語に依存しないで証明
φ ⇒ ψの形式をとる
φ, ψはstatic logic(static logicはMatching logicの一部分)であり、コードを含む
φ ⇒ ψの意味
「所与の言語セマンティックで実行した場合に、φに含まれる全ての状態は、ψに行き着く、または停止しない」
ホーア論理との比較や対応
ホーア論理での$ \{Pre\}Code\{Post\}は、$ \overline{Code} \land \overline{Pre} \Rightarrow \epsilon \land \overline{Post}と表される
ε(paperだと記号違ったけど)は、空を表す
オーバラインの意味: $ \overline{Code}$ \overline{Pre}などでは変数は全て論理値になる
ホーア論理では、プログラムと論理値に区別はないためこうなる
ホーア論理からの自動変換もできるよう
推論規則
https://gyazo.com/2a5a1d7856feaf30f8c3bb35a2125846
Circularitiesの流れ
During the proof, circularities can be added to C via $ Circularity, flushed into A by $ Transitivity, and used via $ Axiom
:$ Circularity
coinductive nature,
allowing us to make new circularity claims. We typically make such claims for code with repetitive behaviors, such as loops, recursive functions, jumps, etc.
If there is a derivation of the claim using itself as a circularity, then the claim holds.
This would obviously be unsound if the new assumption was available immediately, but requiring progress (taking at least on step before circularities can be used) ensures that only diverging executions correspond to endless invocation of a circularity
Circularity is a language-independent generalization of the typical language-specific invariant proof rules associated to language constructs with repetitive behaviors, such as loops, recursive functions, jumps, etc.
参考
KにおけるReachability Logicを使った検証システムの理論的解説
reachability logicのsoundness, relative completenessの証明に加え、各ruleの解説がある
Reachability Logic Prover アルゴリズム
概要
参考
paper 第5章
generates queries to a theorem prover
fully automated
https://gyazo.com/da6821418175e198ca600f415688106fを示す時
https://gyazo.com/74826ce249dece7b6e9a5a19ec9e6a10
"⊭"は "⊨ true" の否定
推論規則との対応
Implementing the computation of multiple steps of symbolic execution across multiple paths with a queue
-$ Transitivity$ Reflexivity
Computing successors (line 1 and line 9)
-$ Step
splitting the subsequent disjunction
-$ Case Analysis
Finishing an execution path (line 5)
-$ Consequence
Using a specification rule (lines 6-7)
-$ Consequence, $ Abstraction, $ Axiom
Since $ Q is initialized with the successors of $ \phi, a step of $ Transitivity already moved $ C to $ A
$ Consequence and $ Abstraction simplify a pattern before adding it to $ Q
We use $ Circularity on the set $ C before the beginning of the algorithm. (line 0)
This is sound because in line 1, we compute the successors of $ \phi outside the while loop, which amounts to $ Step + Transitivity
and then we use the rules in C with $ Axiom in the body of the loop in line 6.
Thus, we can conclude that all the rules in $ C hold.
実装
Matching Logic Proverを呼び出すところ
(1) to finish the proof (line 5)
(2) to use a specification rule to summarize a code fragment (line 6)
(3) to simplify a pattern (before adding it to Q).
Matching Logic Proverにおいて、SMTソルバ(Z3)を呼び出す
具体的には$ Consequence and $ Step
シンボリック実行
Ignoring circularities, these seven proof rules are the formal infrastructure for symbolic execution.
シンボリック実行
言語に依存しないシンボリック実行エンジン
明示的なコントロールフロー(ここは言語依存)がないため複雑
semantic rulesのLHSとのunificationによってコントロールフローを扱う
"narrowing"によってシンボリック実行を実現する
rewriting with unification instead of matching
Then we check the satisfiability of $ \psi \land \psi_u \land \psi_l using the SMT solver.
If it is satisfiable, then$ \pi_r \land \psi \land \psi_u \land \psi_l \land \psi_r is a successor of $ \pi \land \psi
where $ \pi_r \land \psi_r is the right-hand-side of the semantics rule.
実装
効率化
ruleのインデックス
unification結果のキャッシュ
Example
前提知識雑メモ
Separation Logic
用語定義雑メモ
patterns
constructed using variables, symbols, connectives and quantifiers
A conjunctive pattern
a formula π ∧ ψ with π a program configuration term with variables, and ψ a formula without any configuration terms.
Resources