Automating Relational
Program Verification
Hiroshi Unno (University of Tsukuba, Japan)

January 16, 2024

VMCAI'24, London, UK

1

Relational Program Verification• Verification of properties that relate multiple executions of one or more programs• Clarkson and Schneider formalized such properties as sets of sets of program traces
and coined the term hyperproperties [CSF 2008]• 𝒌𝒌-safety is a notable subclass defined as hyperproperties that can be refuted byobserving 𝑘𝑘 finite traces (i.e., the bad thing never involves more than 𝑘𝑘 traces)• An important trend in formal methods with wide applications including security[CSF 2008] Clarkson, Schneider. Hyperproperties.
January 16, 2024

VMCAI'24, London, UK

2

Example Hyperproperties
on Multiple Programs
January 16, 2024

VMCAI'24, London, UK

3

Variants of Program Equivalence• Functional (i.e., input-output) equivalence

An execution of 𝑓𝑓 𝑥𝑥 terminates and returns 𝑦𝑦1• Termination-insensitive: 𝑓𝑓 =𝐷𝐷𝐷𝐷𝐷𝐷 𝑔𝑔 ≜ ∀𝑥𝑥, 𝑦𝑦1 , 𝑦𝑦2 . 𝑓𝑓 𝑥𝑥 ⇓ 𝑦𝑦1 ∧ 𝑔𝑔 𝑥𝑥 ⇓ 𝑦𝑦2 ⟹ 𝑦𝑦1 = 𝑦𝑦2• Termination-sensitive:

𝑓𝑓 =𝐷𝐷𝐷𝐷𝐷𝐷 𝑔𝑔 ≜ 𝑓𝑓 =𝐷𝐷𝐷𝐷𝐷𝐷 𝑔𝑔 ∧ ∀𝑥𝑥.

𝑓𝑓 𝑥𝑥 has a diverging execution

𝑓𝑓 𝑥𝑥 ⇑ ⟹ ¬∃𝑦𝑦. 𝑔𝑔 𝑥𝑥 ⇓ 𝑦𝑦

∧ ∀𝑥𝑥.

𝑔𝑔 𝑥𝑥 ⇑ ⟹ ¬∃𝑦𝑦. 𝑓𝑓 𝑥𝑥 ⇓ 𝑦𝑦

• Non-det. & Termination-sensitive: 𝑓𝑓 =𝑁𝑁𝑁𝑁𝑁𝑁𝑆𝑆 𝑔𝑔 ≜ ∀𝑥𝑥. 𝑦𝑦 ∣ 𝑓𝑓 𝑥𝑥 ⇓ 𝑦𝑦 = 𝑦𝑦 ∣ 𝑔𝑔 𝑥𝑥 ⇓ 𝑦𝑦

• Probabilistic & Termination-sensitive: 𝑓𝑓 =𝑃𝑃𝑃𝑃𝑃𝑃𝑃𝑃 𝑔𝑔 ≜ ∀𝑥𝑥, 𝑦𝑦. Pr 𝑓𝑓 𝑥𝑥 ⇓ 𝑦𝑦 = Pr 𝑔𝑔 𝑥𝑥 ⇓ 𝑦𝑦

• Trace equivalence: 𝑝𝑝 = 𝑇𝑇𝑇𝑇 𝑞𝑞 ≜ 𝑇𝑇𝑇𝑇 𝑝𝑝 = 𝑇𝑇𝑇𝑇 𝑞𝑞

The set of finite and infinite execution traces of 𝑞𝑞• Bisimilarity: 𝑝𝑝 ∼𝑏𝑏𝑏𝑏𝑏𝑏 𝑞𝑞 ≜ there is a strong bisimulation 𝑅𝑅 such that 𝑝𝑝, 𝑞𝑞 ∈ 𝑅𝑅
• Observational equivalence: 𝑝𝑝 =𝑂𝑂𝑂𝑂𝑂𝑂 𝑞𝑞 ≜ ∀𝐶𝐶, 𝑦𝑦. 𝐶𝐶 𝑝𝑝 ⇓ 𝑦𝑦 ⟺ 𝐶𝐶 𝑞𝑞 ⇓ 𝑦𝑦

• Captures non-trivial interactions between contexts 𝐶𝐶 and higher-order, object-oriented,
and effectful (e.g., non-det., probabilistic, stateful, exception-raising, …) programs• In security applications, attackers’ capabilities are reflected in the definition of contexts 𝐶𝐶
January 16, 2024

VMCAI'24, London, UK

4

Variants of Program Refinement• Functional (i.e., input-output) refinement:

Useful to transfer properties and proofs!

• Termination-insensitive: 𝑓𝑓 ≤ 𝑇𝑇𝐼𝐼 𝑔𝑔 ≜ ∀𝑥𝑥, 𝑦𝑦. 𝑓𝑓 𝑥𝑥 ⇓ 𝑦𝑦 ⟹ 𝑔𝑔 𝑥𝑥 ⇓ 𝑦𝑦
• If 𝑓𝑓 ≤ 𝑇𝑇𝐼𝐼 𝑔𝑔, then ⊨ 𝑃𝑃𝑃𝑃𝑃𝑃 𝑔𝑔 𝑃𝑃𝑃𝑃𝑃𝑃𝑃𝑃 implies ⊨ 𝑃𝑃𝑃𝑃𝑃𝑃 𝑓𝑓 𝑃𝑃𝑃𝑃𝑃𝑃𝑃𝑃• Termination-sensitive: 𝑓𝑓 ≤ 𝑇𝑇𝑇𝑇 𝑔𝑔 ≜ 𝑓𝑓 ≤ 𝑇𝑇𝑇𝑇 𝑔𝑔 ∧ ∀𝑥𝑥. 𝑓𝑓 𝑥𝑥 ⇑ ⟹ 𝑔𝑔 𝑥𝑥 ⇑• If 𝑓𝑓 ≤ 𝑇𝑇𝑇𝑇 𝑔𝑔, then ⊨ 𝑃𝑃𝑃𝑃𝑃𝑃 𝑔𝑔 𝑃𝑃𝑃𝑃𝑃𝑃𝑃𝑃 implies ⊨ 𝑃𝑃𝑃𝑃𝑃𝑃 𝑓𝑓 𝑃𝑃𝑃𝑃𝑃𝑃𝑃𝑃 (i.e., termination is also transferred)• Trace refinement: 𝑝𝑝 ≤ 𝑇𝑇𝑇𝑇 𝑞𝑞 ≜ 𝑇𝑇𝑇𝑇 𝑝𝑝 ⊆ 𝑇𝑇𝑇𝑇 𝑞𝑞• If 𝑝𝑝 ≤ 𝑇𝑇𝑇𝑇 𝑞𝑞, then trace properties of 𝑞𝑞 can be transferred to 𝑝𝑝• Similarity: 𝑝𝑝 ≤𝑠𝑠𝑠𝑠𝑠𝑠 𝑞𝑞 ≜ there is a strong simulation 𝑅𝑅 such that 𝑝𝑝, 𝑞𝑞 ∈ 𝑅𝑅

• If 𝑝𝑝 ≤𝑠𝑠𝑠𝑠𝑠𝑠 𝑞𝑞, then trace (but branching-time) properties of 𝑞𝑞 can be migrated to 𝑝𝑝• If 𝑝𝑝 ∼𝑏𝑏𝑏𝑏𝑏𝑏 𝑞𝑞, then branching-time (but hyper-) properties of 𝑞𝑞 can be migrated to 𝑝𝑝
January 16, 2024

VMCAI'24, London, UK

5

Program Refinement as Generalized Model Checking• Program refinement verification ⊨ 𝑝𝑝 ≤ 𝑞𝑞 generalizes ordinary model checking 𝑝𝑝 ⊨ 𝜙𝜙
• A specification of 𝒑𝒑 is given as a program 𝒒𝒒 instead of a logical formula 𝜙𝜙• 𝑞𝑞 can encode the given 𝜙𝜙 (if the programming language is expressive enough)• 𝑞𝑞 can be a reference implementation (cf. seL4 Project) oran abstract model represented as a highly non-deterministic program• This motivates me to investigate entailment checking problems 𝜓𝜓1 ⊨ 𝜓𝜓2 ina first-order fixpoint logic modulo theories we call 𝜇𝜇CLP [CAV 2017, LICS 2018, POPL 2023]• I will come back to this point:
relational verification via entailment checking in 𝝁𝝁𝝁𝝁𝝁𝝁𝝁𝝁[CAV 2017] Unno et al. Automating Induction for Solving Horn Clauses.
[LICS 2018] Nanjo et al. A Fixpoint Logic and Dependent Effects for Temporal Property Verification.
[POPL 2023] Unno et al. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification.

January 16, 2024

VMCAI'24, London, UK

6

Example Hyperproperties
on Single Program
January 16, 2024

VMCAI'24, London, UK

7

Information Flow Confidentiality & Integrity [JSAC 2003]• Deterministic programs• Termination-insensitive non-interference ∈ 𝟐𝟐-safety ⊂ Hypersafety :𝑇𝑇𝑇𝑇𝑇𝑇𝑇𝑇 𝑓𝑓 ≜ ∀ℎ1 , ℎ2 , 𝑥𝑥, 𝑦𝑦1 , 𝑦𝑦2 . 𝑓𝑓 ℎ1 , 𝑥𝑥 ⇓ 𝑦𝑦1 ∧ 𝑓𝑓 ℎ2 , 𝑥𝑥 ⇓ 𝑦𝑦2 ⟹ 𝑦𝑦1 = 𝑦𝑦2

A well-studied security policy formalizing the absence of information leakage• Termination-sensitive non-interference:
𝑇𝑇𝑇𝑇𝑇𝑇𝑇𝑇 𝑓𝑓 ≜ 𝑇𝑇𝑇𝑇𝑇𝑇𝑇𝑇 𝑓𝑓 ∧ ∀ℎ1 , ℎ2 , 𝑥𝑥. 𝑓𝑓 ℎ1 , 𝑥𝑥 ⇑ ⟹ ¬∃𝑦𝑦. 𝑓𝑓 ℎ2 , 𝑥𝑥 ⇓ 𝑦𝑦

• Timing attack resilience• Non-deterministic / concurrent programs• Observational determinism: 𝑂𝑂𝑂𝑂 𝑓𝑓 ≜ ∀ℎ1 , ℎ2 , 𝑥𝑥, 𝑦𝑦1 , 𝑦𝑦2 . 𝑓𝑓 ℎ1 , 𝑥𝑥 ⇓ 𝑦𝑦1 ∧ 𝑓𝑓 ℎ2 , 𝑥𝑥 ⇓ 𝑦𝑦2 ⟹ 𝑦𝑦1 = 𝑦𝑦2• Possibilistic non-interference• TI Generalized NI: 𝑇𝑇𝑇𝑇𝑇𝑇𝑇𝑇𝑇𝑇 𝑓𝑓 ≜ ∀ℎ1 , ℎ2 , 𝑥𝑥, 𝑦𝑦. 𝑓𝑓 ℎ1 , 𝑥𝑥 ⇓ 𝑦𝑦 ⟹ 𝑓𝑓 ℎ2 , 𝑥𝑥 ⇑ ∨ 𝑓𝑓 ℎ2 , 𝑥𝑥 ⇓ 𝑦𝑦

• TS Generalized NI: 𝑇𝑇𝑇𝑇𝑇𝑇𝑇𝑇𝑇𝑇 𝑓𝑓 ≜ ∀ℎ1 , ℎ2 , 𝑥𝑥, 𝑦𝑦. 𝑓𝑓 ℎ1 , 𝑥𝑥 ⇓ 𝑦𝑦 ⟹ 𝑓𝑓 ℎ2 , 𝑥𝑥 ⇓ 𝑦𝑦

• Bisimulation-based non-interface
January 16, 2024

[JSAC 2003] Sabelfeld, Myers. Language-based Information-flow Security.

VMCAI'24, London, UK

8

Availability• Denial of Service (DoS) attack resilience• Property that “the average response time over all executions is bounded” isrelational while “the maximum response time is bounded” is non-relational

January 16, 2024

VMCAI'24, London, UK

9

Algorithm Analysis• Robustness and sensitivity [CACM 2012, ICFP 2010]• Continuity:∀𝑥𝑥1 , 𝑥𝑥2 . ∀𝜖𝜖 > 0. ∃𝛿𝛿 > 0. 𝑑𝑑 𝑥𝑥1 , 𝑥𝑥2 < 𝛿𝛿 ⟹𝐶𝐶𝐶𝐶𝐶𝐶𝐶𝐶 𝑓𝑓 ≜∀𝑦𝑦1 , 𝑦𝑦2 . 𝑓𝑓 𝑥𝑥1 ⇓ 𝑦𝑦1 ∧ 𝑓𝑓 𝑥𝑥2 ⇓ 𝑦𝑦2 ⟹ 𝑑𝑑 𝑦𝑦1 , 𝑦𝑦2 < 𝜖𝜖
• Lipschitz Continuity:
𝑑𝑑 𝑦𝑦1 , 𝑦𝑦2
𝐿𝐿𝐿𝐿 𝑓𝑓, 𝑐𝑐 ≜ ∀𝑥𝑥1 , 𝑥𝑥2 , 𝑦𝑦1 , 𝑦𝑦2 . 𝑓𝑓 𝑥𝑥1 ⇓ 𝑦𝑦1 ∧ 𝑓𝑓 𝑥𝑥2 ⇓ 𝑦𝑦2 ⟹< 𝑐𝑐
𝑑𝑑 𝑥𝑥1 , 𝑥𝑥2[CACM 2012] Chaudhuri et al. Continuity and Robustness of Programs.
[ICFP 2010] Reed, Pierce. Distance Makes the Types Grow Stronger.
January 16, 2024

VMCAI'24, London, UK

10Specific Use Cases (1/2)• Regression verification [STVR 2013]• Check refinement 𝑇𝑇 ≤ 𝑆𝑆 for different versions 𝑇𝑇, 𝑆𝑆 of programs
where 𝑇𝑇 is obtained from 𝑆𝑆 by refactoring, bug fixes, or enhancements• Goal is to verify the absence of a software regression which is a bug of 𝑇𝑇
introduced by the modifications to 𝑆𝑆• Translation validation [TACAS 1998]• Check refinement 𝑇𝑇 ≤ 𝑆𝑆 for the source 𝑆𝑆 and target 𝑇𝑇 programs
obtained by compilation or optimization[STVR 2013] Godlin, Strichman. Regression verification: proving the equivalence of similar programs.
[TACAS 1998] Pnueli et al. Translation Validation.
January 16, 2024

VMCAI'24, London, UK

11

Specific Use Cases (2/2)
Verification of an implementation of an
abstract data type with algebraic specs.
• Arithmetic operations with:equivalence, associativity, commutativity,
distributivity, idempotency, monotonicity,
invertibility, symmetry, transitivity, …
(see the right table from [CAV 2017])• List operations with algebraic specs. like:append (take xs n) (drop xs n) = xs
Try out a web interface of our relationalverifier from http://lfp.dip.jp/rcaml/[CAV 2017] Unno et al. Automating Induction for Solving Horn Clauses.
January 16, 2024

VMCAI'24, London, UK

12

Goal of This Talk
Stimulate the “immature” research field and, hopefully, find research collaborators by
1. discussing the challenges in relational verification,

2. introducing our automated relational verification methods, and3. highlighting the current limitations as well as future research directions
Disclaimer: This talk will
• mainly deal with fully automated deductive relational verification,• target functional properties and will not address trace or contextual properties, and• focus on infinite-state systems that can exhibit effects such as non-terminationand non-determinism, and we will not cover other effects or finite-state systems
January 16, 2024

VMCAI'24, London, UK

13

Outline
1. Introduction

2. Challenges in Relational Verification

3. Automating Relational Verification
1. Self-Composition (or Product Programs) [CAV 2021]
2. Entailment Checking in 𝝁𝝁𝐂𝐂𝐋𝐋𝐏𝐏 [CAV 2017]
4. Current Limitations and Future Directions[CAV 2021] Unno et al. Constraint-Based Relational Verification.
[CAV 2017] Unno et al. Automating Induction for Solving Horn Clauses.
January 16, 2024

VMCAI'24, London, UK

14

Outline
1. Introduction

2. Challenges in Relational Verification

3. Automating Relational Verification
1. Self-Composition (or Product Programs) [CAV 2021]
2. Entailment Checking in 𝝁𝝁𝐂𝐂𝐋𝐋𝐏𝐏 [CAV 2017]
4. Current Limitations and Future Directions[CAV 2021] Unno et al. Constraint-Based Relational Verification.
[CAV 2017] Unno et al. Automating Induction for Solving Horn Clauses.
January 16, 2024

VMCAI'24, London, UK

15

Challenges in Relational Verification• Although each program execution is independent (except the input correlation
ensured by the precondition), proving relational properties is challenging
without reasoning about the correlation of intermediate execution states• Analyzing each execution separately does not work well as it necessitates
an exact summarization of the input-output relation for each execution• Thus, an automated verifier is required to simultaneously synthesize
1. a correlation of intermediate states, namely a relational invariant and2. a scheduler (or alignment) that preserves it!

January 16, 2024

VMCAI'24, London, UK

16

Comparison with Concurrent Programs Verification• Executions of programs that run concurrently can be highly dependent as states can besynchronized with locks or semaphores, and data races can occur due to shared memory• Concurrent program is checked to satisfy the specification
for all possible interleaving executions under a demonic scheduler• Multiple executions in relational verification are independent• It is sufficient to prove that the specification holds in a certain interleaving execution,chosen by an angelic scheduler• However, to reason about the correlation between states at the time of output,
it is still necessary to effectively synchronize at other intermediate points as well
• Therefore, the complexity of the verification is more significantly influenced by thedifferences between the programs than by the complexity of each program individually
January 16, 2024

VMCAI'24, London, UK

17

Example: Program Equivalence
int mult1(int x, int y) {a: int z=0;b: while(x>0) { x=x-1; z=z+y }c: return z;}

int mult2(int x, int y) {d: int z=0;
e: if(x % 2 == 1) { x=x-1; z=z+y }f: while(x>0) { x=x-2; z=z+2*y }g: return z;}

Let’s align the executions to preserve 𝑧𝑧1 = 𝑧𝑧2 as much as possible

mult1 𝑝𝑝𝑐𝑐1 , 𝑥𝑥1 , 𝑦𝑦1 , 𝑧𝑧1 : 𝑎𝑎, 3,4, ? → 𝑏𝑏, 3,4,0 → 𝑏𝑏, 2,4,4 → 𝑏𝑏, 1,4,8 → 𝑏𝑏, 0,4,12 → 𝑐𝑐, 0,4,12
𝑧𝑧1 = 𝑧𝑧2

𝑧𝑧1 = 𝑧𝑧2

𝑧𝑧1 ≠ 𝑧𝑧2

𝑧𝑧1 = 𝑧𝑧2

mult2 𝑝𝑝𝑐𝑐2 , 𝑥𝑥2 , 𝑦𝑦2 , 𝑧𝑧2 : 𝑑𝑑, 3,4, ? → 𝑒𝑒, 3,4,0 → 𝑓𝑓, 2,4,4 → 𝑓𝑓, 0,4,12 → 𝑔𝑔, 0,4,12

𝑧𝑧1 = 𝑧𝑧2

stuttering execution when 𝑥𝑥1 %2 = 1
A relational invariant preserved by the above alignment: instead of lock-step one recovers 𝑧𝑧1 = 𝑧𝑧2
But how to infer such predicate 𝑥𝑥1 %2 = 1?

𝑦𝑦1 = 𝑦𝑦2 ∧ 𝑝𝑝𝑐𝑐1 = 𝑏𝑏 ∧ 𝑝𝑝𝑐𝑐2 = 𝑓𝑓 ∧ 𝑥𝑥1 % 2 = 0 ⇒ 𝑧𝑧1 = 𝑧𝑧2 ∧ 𝑝𝑝𝑐𝑐1 = 𝑏𝑏 ∧ 𝑝𝑝𝑐𝑐2 = 𝑓𝑓 ∧ 𝑥𝑥1 % 2 = 1 ⇒ 𝑧𝑧1 + 𝑦𝑦1 = 𝑧𝑧2
January 16, 2024

VMCAI'24, London, UK

18

Example: Termination-Insensitive Non-Interference(TINI) ∈ 2-safety (1/2)• doubleSquare ℎ, 𝑥𝑥 [CAV 2019] computes 2 ⋅ 𝑥𝑥 2 in two different ways depending on
the high security input ℎdoubleSquare(bool h, int x) {int z, y=0;
if(h) { z=2*x } else { z=x }while(z>0) { z--; y=y+x }if(!h) { y=2*y }return y;}

Can an attacker infer the value of ℎ byobserving the low security input 𝑥𝑥 and thereturn value 𝑦𝑦?
No! TINI(doubleSquare) holds:∀𝒉𝒉𝟏𝟏 , 𝒙𝒙𝟏𝟏 , 𝒚𝒚𝟏𝟏 , 𝒉𝒉𝟐𝟐 , 𝒙𝒙𝟐𝟐 , 𝒚𝒚𝟐𝟐 .
doubleSquare 𝒉𝒉𝟏𝟏 , 𝒙𝒙𝟏𝟏 ⇓ 𝒚𝒚𝟏𝟏 ∧doubleSquare 𝒉𝒉𝟐𝟐 , 𝒙𝒙𝟐𝟐 ⇓ 𝒚𝒚𝟐𝟐 ∧𝒙𝒙𝟏𝟏 = 𝒙𝒙𝟐𝟐 ⇒ 𝒚𝒚𝟏𝟏 = 𝒚𝒚𝟐𝟐

[CAV 2019] Shemer et al. Property Directed Self Composition.

January 16, 2024

VMCAI'24, London, UK

19

Example: Termination-Insensitive Non-Interference(TINI) ∈ 2-safety (2/2)• The parallel executions of 2 copies of the program under the partial lock-stepscheduler makes a safe relational invariant “complex”

doubleSquare(bool h, int x) {int z, y=0;
ℓ1 : if(h) {z=2*x} else {z=x}ℓ2 : while(z>0) { z--; y=y+x }ℓ3 : if(!h) { y=2*y }return y; }Any “simple” but safe and ind. relational invariant
preserved by the partial lock-step scheduler?
↳ No! Safe ind. relational invariant for thescheduler is not expressible in LIA [CAV 2019]
Copy2 has exited the loop. Partial lock-step scheduler
waits for Copy1 to exit the loop to synchronize

Executions ℎ1 , 𝑥𝑥1 , 𝑦𝑦1 , 𝑧𝑧1 and ℎ2 , 𝑥𝑥2 , 𝑦𝑦2 , 𝑧𝑧2 with the partial lock-step scheduler:ℓ3ℓ1 ⊤, 2,0, ? →ℓ2 ⊤, 2,0,4 →ℓ2 ⊤, 2,2,3 →ℓ2 ⊤, 2,4,2 →ℓ2 ⊤, 2,6,1 →ℓ2 ⊤, 2,8,0 →⊤, 2,8,0𝑥𝑥1 = 𝑥𝑥2

ℓ1 ⊥, 2,0, ?

𝑦𝑦1 = 𝑦𝑦2

𝑦𝑦1 = 𝑦𝑦2

𝑦𝑦1 = 𝑦𝑦2

𝑦𝑦1 ≠ 𝑦𝑦2

𝑦𝑦1 ≠ 𝑦𝑦2→ℓ2 ⊥, 2,0,2 →ℓ2 ⊥, 2,2,1 →ℓ2 ⊥, 2,4,0 →ℓ3 ⊥, 2,8,0January 16, 2024

VMCAI'24, London, UK

How can we provethat 𝑦𝑦1 = 𝑦𝑦2 ?
20

Example: Co-Termination ∈ Hyperliveness (1/2)
prog1(int x, int y) { while(x>0) { x=x–y; } }prog2(int x, int y) { while(x>0) { x=x–2*y; } }Do prog1 𝑥𝑥1 , 𝑦𝑦1 and prog2 𝑥𝑥2 , 𝑦𝑦2 agree on termination
under the precondition 𝑥𝑥1 = 𝑥𝑥2 ∧ 𝑦𝑦1 = 𝑦𝑦2 ?

Yes! (Symmetric) co-termination holds:∀𝒙𝒙𝟏𝟏 , 𝒚𝒚𝟏𝟏 , 𝒙𝒙𝟐𝟐 , 𝒚𝒚𝟐𝟐 . 𝒙𝒙𝟏𝟏 = 𝒙𝒙𝟐𝟐 ∧ 𝒚𝒚𝟏𝟏 = 𝒚𝒚𝟐𝟐 ⇒∃𝒛𝒛𝟏𝟏 . prog1 𝒙𝒙𝟏𝟏 , 𝒚𝒚𝟏𝟏 ⇓ 𝒛𝒛𝟏𝟏
∃𝒛𝒛𝟐𝟐 . prog2 𝒙𝒙𝟐𝟐 , 𝒚𝒚𝟐𝟐 ⇓ 𝒛𝒛𝟐𝟐∧
⇒ ¬ prog2 𝒙𝒙𝟐𝟐 , 𝒚𝒚𝟐𝟐 ⇑⇒ ¬ prog1 𝒙𝒙𝟏𝟏 , 𝒚𝒚𝟏𝟏 ⇑One symmetric co-termination problem boils down to
two asymmetric co-termination problems
January 16, 2024

VMCAI'24, London, UK

21

Example: Co-Termination ∈ Hyperliveness (2/2)
prog1(int x, int y) { while(x>0) { x=x–y; } }prog2(int x, int y) { while(x>0) { x=x–2*y; } }How can we prove that this residual
execution always terminates?

𝑥𝑥1 = 𝑥𝑥2
∧ 𝑦𝑦1 = 𝑦𝑦2

Executions 𝑥𝑥1 , 𝑦𝑦1 and 𝑥𝑥2 , 𝑦𝑦2 with the partial lock-step scheduler:
4,1 → 3,1 → 2,1 → 1,1 → 0,1
4,1 → 2,1 → 0,1

January 16, 2024

prog2

terminated

VMCAI'24, London, UK

22

Example: (TI-/TS-)GNI ∈ ∀∃hyperproperties• gniEx ℎ, 𝑙𝑙 non-deterministically returns a value 𝑥𝑥 ≥ 𝑙𝑙 in two different ways
depending on the high security input ℎ

gniEx(bool high, int low) {Can an attacker infer the value of ℎ byif(high) {observing the low security input 𝑙𝑙 andint x = nondet_int();
the return value 𝑥𝑥?
Demonic (∀) choiceif(x >= low) { return x }No! TIGNI(gniEx) holds:
else { while(true) {} }∀𝒉𝒉𝟏𝟏 , 𝒉𝒉𝟐𝟐 , 𝒍𝒍, 𝒙𝒙𝟏𝟏 . gniEx 𝒉𝒉𝟏𝟏 , 𝒍𝒍 ⇓ 𝒙𝒙𝟏𝟏 ⇒} else {gniEx 𝒉𝒉𝟐𝟐 , 𝒍𝒍 ⇑ ∨Angelic (∃) choice
int x = low;∃𝒙𝒙𝟐𝟐 . gniEx 𝒉𝒉𝟐𝟐 , 𝒍𝒍 ⇓ 𝒙𝒙𝟐𝟐 ∧ 𝒙𝒙𝟏𝟏 = 𝒙𝒙𝟐𝟐
while(nondet_bool()){x++}return x;
TSGNI(gniEx) also holds:}∀𝒉𝒉𝟏𝟏 , 𝒉𝒉𝟐𝟐 , 𝒍𝒍, 𝒙𝒙𝟏𝟏 . gniEx 𝒉𝒉𝟏𝟏 , 𝒍𝒍 ⇓ 𝒙𝒙𝟏𝟏 ⇒}But how to solve such games between ∀ and ∃? ∃𝒙𝒙𝟐𝟐 . gniEx 𝒉𝒉𝟐𝟐 , 𝒍𝒍 ⇓ 𝒙𝒙𝟐𝟐 ∧ 𝒙𝒙𝟏𝟏 = 𝒙𝒙𝟐𝟐
January 16, 2024

VMCAI'24, London, UK

23

Other Challenging Examples in the Literature[LFCS 2013][PLDI 2019]

January 16, 2024

[CAV 2016][PLDI 2019] Churchill et al. Semantic program alignment for equivalence checking.
[LFCS 2013] Barthe et al. Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification[CAV 2016] Fedyukovich et al. Property Directed Equivalence via Abstract Simulation
VMCAI'24, London, UK

24

Outline
1. Introduction

2. Challenges in Relational Verification

3. Automating Relational Verification
1. Self-Composition (or Product Programs) [CAV 2021]
2. Entailment Checking in 𝝁𝝁𝐂𝐂𝐋𝐋𝐏𝐏 [CAV 2017]
4. Current Limitations and Future Directions[CAV 2021] Unno et al. Constraint-Based Relational Verification.
[CAV 2017] Unno et al. Automating Induction for Solving Horn Clauses.
January 16, 2024

VMCAI'24, London, UK

25

Self-Composition(or Product Programs)
January 16, 2024

VMCAI'24, London, UK

26

Self-Composition (or Product Programs)• Relational verification amounts to synthesis of relational invariants and schedulers• Self-composition refers to a range of techniques aimed at synthesizing alignments
represented symbolically as programs, automata, logical constraints, and games• Syntactic: [CSFW 2004, SAS 2005, PLAS 2006, FM 2011, LFCS 2013, SAS 2016, LPAR 2017]• Semantic: [CAV 2019a, CAV 2019b, PLDI 2019, CAV 2021, CAV 2022][CSFW 2004] Barthe et al. Secure Information Flow by Self-Composition.
[SAS 2005] Terauchi, Aiken. Secure Information Flow as a Safety Problem.
[PLAS 2006] Unno et al. Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference.
[FM 2011] Barthe et al. Relational Verification Using Product Programs.
[LFCS 2013] Barthe et al. Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification[SAS 2016] Angelis et al. Relational Verification Through Horn Clause Transformation.
[LPAR 2017] Mordvinov, Fedyukovich. Synchronizing Constrained Horn Clauses.
[CAV 2019a] Farzan, Vandika. Automated Hypersafety Verification.
[CAV 2019b] Shemer et al. Property Directed Self Composition.
[PLDI 2019] Churchill et al. Semantic program alignment for equivalence checking.
[CAV 2021] Unno et al. Constraint-Based Relational Verification.
[CAV 2022] Beutner, Finkbeiner. Software Verification of Hyperproperties Beyond k-Safety.
January 16, 2024

VMCAI'24, London, UK

27

Our Approach to Semantic Self-Composition [CAV 2021]• Soundly and completely encode the simultaneous synthesis problem of
relational invariants and fair & semantic schedulers needed for relationalverification (𝑘𝑘-safety, co-termination, and GNI) asa constraint solving problem of the class, we call pfwCSP that extends CHCs with
1. head-disjunction (used to express scheduler fairness constraints),

2. well-foundedness constraints (used for synthesizing co-termination witnesses),
3. functionality constraints (used for synthesizing winning strategies for GNI)

• Generalize semantic self-composition for 𝑘𝑘-safety [CAV 2019] to GNI and co-termination• For solving pfwCSP, provide a constraint solver PCSat based on
the template-based CEGIS and an unsat-core based template refinement
January 16, 2024

[CAV 2019] Shemer et al. Property Directed Self Composition.
[CAV 2021] Unno et al. Constraint-Based Relational Verification.

VMCAI'24, London, UK

28

Semantic Self-Composition for TI-NI

Can choose which program to execute depending on the states• Find a semantic scheduler 𝑆𝑆𝑆𝑆ℎ and a safe invariant of the parallel executions of 2
copies of the program under 𝑆𝑆𝑐𝑐ℎFound scheduler 𝑆𝑆𝑆𝑆ℎ dictates:
doubleSquare(bool h,int x) {int z, y=0;
ℓ1 : if(h) {z=2*x} else {z=x}ℓ2 : while(z>0) { z--; y=y+x }ℓ3 : if(!h) { y=2*y }return y; }𝑦𝑦1 = 2 ⋅ 𝑦𝑦2 − 𝑥𝑥2𝑦𝑦1 = 2 ⋅ 𝑦𝑦2

both copies move if 𝑧𝑧1 = 2 ⋅ 𝑧𝑧2 ,1st copy moves if 𝑧𝑧1 = 2 ⋅ 𝑧𝑧2 + 1

Found invariant expressible in LIA:

𝑦𝑦1 = 2 ⋅ 𝑦𝑦2 ∧ 𝑧𝑧1 = 2 ⋅ 𝑧𝑧2 ∨ ⋯ ∧ℎ1 ∧ ¬ℎ2∧∧ 𝑥𝑥1 = 𝑥𝑥2
𝑦𝑦1 = 2 ⋅ 𝑦𝑦2 − 𝑥𝑥2 ∧ 𝑧𝑧1 = 2 ⋅ 𝑧𝑧2 + 1∨ ℎ1 ∧ ℎ2 ∧ ⋯ ∨ ¬ℎ1 ∧ ℎ2 ∧ ⋯ ∨ ¬ℎ1 ∧ ¬ℎ2 ∧ ⋯𝑦𝑦1 = 2 ⋅ 𝑦𝑦2 − 𝑥𝑥2

Executions ℎ1 , 𝑥𝑥1 , 𝑦𝑦1 , 𝑧𝑧1 and ℎ2 , 𝑥𝑥2 , 𝑦𝑦2 , 𝑧𝑧2 under 𝑆𝑆𝑆𝑆ℎ:𝑦𝑦1 = 2 ⋅ 𝑦𝑦2
ℓ
ℓ2
ℓ2
ℓ2
ℓ2
ℓ2 ⊤, 2,6,1 →ℓ1 ⊤, 2,0, ? →⊤, 2,0,4 →⊤, 2,2,3 →⊤, 2,4,2 →⊤, 2,8,0 →3 ⊤, 2,8,0

𝑦𝑦1 = 𝑦𝑦2
ℓ1

𝑦𝑦1 = 2 ⋅ 𝑦𝑦2⊥, 2,0, ? →ℓ2 ⊥, 2,0,2 →ℓ2 ⊥, 2,2,1 →ℓ2 ⊥, 2,4,0 →ℓ3 ⊥, 2,8,0January 16, 2024

VMCAI'24, London, UK

𝑦𝑦1 = 𝑦𝑦229

Prog. & Spec.

pfwCSP

Constraint Generation

represents a relational invariant
preserved by a semantic scheduler
Input:
doubleSquare(bool h, int x) {int z, y=0;

SAT or UNSAT

Constraint Solving

the relational invariant is
inductive and implies TI-NI

Output 𝓒𝓒 (with 𝒉𝒉𝟏𝟏 = ⊤ ∧ 𝒉𝒉𝟐𝟐 = ⊥ fixed):••
non-Horn clause that
if(h) { z=2*x }goesbeyondCHCs !
else{ z=x}
while(z>0)
•
{
z--;
y=y+x
}
represent the semantic

𝑥𝑥1 = 𝑥𝑥2 ∧ 𝑦𝑦1 = 𝑦𝑦2 = 0,∧ 𝑧𝑧1 the= 2 scheduler⋅ 𝑥𝑥1 ∧ 𝑧𝑧2 = is𝑥𝑥2fair: at least one
programmust be𝑉𝑉1 , 𝑉𝑉2 ∧ 𝑆𝑆𝑆𝑆ℎ𝐼𝐼 𝑥𝑥1 , 𝑦𝑦1′ , 𝑧𝑧1′ , 𝑉𝑉2 ⟸ 𝐼𝐼unfinished1 𝑉𝑉1 , 𝑉𝑉2
𝑧𝑧1 > 0 ∧ 𝑧𝑧1′ = 𝑧𝑧1scheduled− 1 ∧ 𝑦𝑦1′ =if𝑦𝑦1there+ 𝑥𝑥1is∨ any∧,…,′ the soundness)(necessary
𝑧𝑧1 ≤ 0 ∧𝑧𝑧1′ = 𝑧𝑧1 ∧ 𝑦𝑦for=𝑦𝑦11
𝑦𝑦1 = 2 ⋅ 𝑦𝑦2 ⟸ 𝐼𝐼 𝑉𝑉1 , 𝑉𝑉2 ∧ 𝑧𝑧1 ≤ 0 ∧ 𝑧𝑧2 ≤ 0,
𝑆𝑆𝑆𝑆ℎ1 𝑉𝑉1 , 𝑉𝑉2 ∨ 𝑆𝑆𝑆𝑆ℎ2 𝑉𝑉1 , 𝑉𝑉2 ∨ 𝑆𝑆𝑆𝑆ℎ1,2 𝑉𝑉1 , 𝑉𝑉2

𝐼𝐼 𝑉𝑉1 , 𝑉𝑉2 ⟸•if(!h) { y=2*yscheduler:
if 𝑆𝑆𝑆𝑆ℎ1} holds,⟸ 𝐼𝐼 𝑉𝑉1 , 𝑉𝑉2 ∧ 𝑧𝑧1 > 0 ∨ 𝑧𝑧2 > 0 ,1st copy
returny;is scheduled• 𝑧𝑧1 > 0 ⟸ 𝐼𝐼 𝑉𝑉1 , 𝑉𝑉2 ∧ 𝑆𝑆𝑆𝑆ℎ1 𝑉𝑉1 , 𝑉𝑉2 ∧ 𝑧𝑧2 > 0,}
• 𝑧𝑧2 > 0 ⟸ 𝐼𝐼 𝑉𝑉1 , 𝑉𝑉2 ∧ 𝑆𝑆𝑆𝑆ℎ2 𝑉𝑉1 , 𝑉𝑉2 ∧ 𝑧𝑧1 > 0,
where 𝑉𝑉1 = 𝑥𝑥1 , 𝑦𝑦1 , 𝑧𝑧1 and 𝑉𝑉2 = 𝑥𝑥2 , 𝑦𝑦2 , 𝑧𝑧2

January 16, 2024

VMCAI'24, London, UK

30

Semantic Self-Composition for Asymmetric CoTermination• Find a fair semantic scheduler 𝑆𝑆𝑆𝑆𝑆, a relational invariant, and a well-founded
relation under 𝑆𝑆𝑐𝑐𝑐
prog1(int x, int y) { while(x>0) { x=x–y; } }prog2(int x, int y) { while(x>0) { x=x–2*y; } }Found scheduler 𝑆𝑆𝑆𝑆ℎ dictates:

both programs move if 𝑥𝑥1 > 0 ∧ 𝑥𝑥2 > 0,
prog1 moves if 𝑥𝑥1 > 0 ∧ 𝑥𝑥2 ≤ 0
𝑥𝑥1 = 𝑥𝑥2
∧ 𝑦𝑦1 = 𝑦𝑦2

Found well-founded relation says:
if 𝑥𝑥1 > 0 ∧ 𝑥𝑥2 ≤ 0, then prog1 repeatedly decreases 𝒙𝒙𝟏𝟏
but 𝒙𝒙𝟏𝟏 is lower bounded by 0

Executions 𝑥𝑥1 , 𝑦𝑦1 and 𝑥𝑥2 , 𝑦𝑦2 with 𝑆𝑆𝑆𝑆ℎ :4,1 → 3,1 → 2,1 → 1,1 → 0,1
4,1 → 2,1 → 0,1

January 16, 2024

prog2

terminated

VMCAI'24, London, UK

prog1

terminatedFound relational invariant implies:𝑥𝑥1 > 0 ∧ 𝑥𝑥2 ≤ 0 ⇒ 𝑦𝑦1 ≥ 1
31

Prog. & Spec.

pfwCSP

Constraint Generation

represents a relational invariant
preserved by a semantic scheduler
Output 𝓒𝓒:
Input:

prog1(x, y) {while(x>0){ x=x–y }
}

•
•

•
•

represents a wellprog2(x,y) {founded relation
while(x>0)
witnessing the •terminationof prog1{ x=x-2*y} •relative to the •} termination of prog2

January 16, 2024

SAT or UNSAT

the relational invariant is
Constraint Solving
inductive
and,function
along with therepresents
a totalrelation,usedwell-founded
to select a bound𝑏𝑏 forimplies
Co-Terminationeachstate 𝑉𝑉𝐼𝐼 0, 𝑏𝑏, 𝑉𝑉 ⟸ 𝐹𝐹𝜆𝜆 𝑉𝑉, 𝑏𝑏 ∧ 𝑥𝑥1 =the𝑥𝑥2 ∧scheduler
𝑦𝑦1 = 𝑦𝑦2 , is fair: all
unfinishedmust
𝐼𝐼 𝑑𝑑 ′ , 𝑏𝑏, 𝑥𝑥1′ , 𝑦𝑦1 , 𝑥𝑥2 , 𝑦𝑦2 ⟸ 𝐼𝐼 𝑑𝑑,
𝑏𝑏, 𝑉𝑉 ∧ 𝑆𝑆𝑆𝑆ℎprograms
1 𝑉𝑉 ∧
eventually𝑥𝑥1 > 0 ∧ 𝑥𝑥1′ = 𝑥𝑥1 − 𝑦𝑦1 ∨ 𝑥𝑥be0 ∧ 𝑥𝑥1′ = 𝑥𝑥1scheduled∧
1 ≤𝑥𝑥1 > 0 ∧ 𝑥𝑥2 > 0 ⇒ 𝑑𝑑 ′ =(necessary
𝑑𝑑 + 1 ,…, for soundness)
𝑅𝑅⇓ 𝑉𝑉1 , 𝑥𝑥1 − 𝑦𝑦1 , 𝑦𝑦1 ⟸ 𝐼𝐼 𝑑𝑑, 𝑏𝑏, 𝑉𝑉1 , 𝑉𝑉2 ∧ 𝑥𝑥1 > 0 ∧ 𝑥𝑥2 ≤ 0,
𝑆𝑆𝑆𝑆ℎ1 𝑑𝑑, 𝑏𝑏, 𝑉𝑉 ∨ 𝑆𝑆𝑆𝑆ℎ2 𝑑𝑑, 𝑏𝑏, 𝑉𝑉 ∨ 𝑆𝑆𝑆𝑆ℎ1,2 𝑑𝑑, 𝑏𝑏, 𝑉𝑉⟸ 𝐼𝐼 𝑑𝑑, 𝑏𝑏, 𝑉𝑉 ∧ 𝑥𝑥1 > 0 ∨ 𝑥𝑥2 > 0 ,𝑥𝑥1 > 0 ⟸ 𝐼𝐼 𝑑𝑑, 𝑏𝑏, 𝑉𝑉 ∧ 𝑆𝑆𝑆𝑆ℎ1 𝑑𝑑, 𝑏𝑏, 𝑉𝑉 ∧ 𝑥𝑥2 > 0,𝑥𝑥2 > 0 ⟸ 𝐼𝐼 𝑑𝑑, 𝑏𝑏, 𝑉𝑉 ∧ 𝑆𝑆𝑆𝑆ℎ2 𝑑𝑑, 𝑏𝑏, 𝑉𝑉 ∧ 𝑥𝑥1 > 0,
𝑑𝑑 ∈ −𝑏𝑏, 𝑏𝑏 ∧ 𝑏𝑏 ≥ 0 ⟸ 𝐼𝐼 𝑑𝑑, 𝑏𝑏, 𝑉𝑉1 , 𝑉𝑉2 ∧ 𝑥𝑥1 > 0 ∧ 𝑥𝑥2 > 0
where 𝑉𝑉 = 𝑥𝑥1 , 𝑦𝑦1 ,𝑥𝑥2 , 𝑦𝑦2
the difference 𝑑𝑑 between the numbers of steps
UKtaken VMCAI'24,
by the London,
two iswithin the bound 𝑏𝑏

32

Semantic Self-Composition for (TI-/TS-)GNI• Find a fair semantic scheduler, a relational invariant, a well-founded relation,and strategies for the non-deterministic choices of the angelic side
• Augment the encodings for TI-NI and Co-Term with• predicate variables that represent the strategies:
total functions from states to choices of the angelic side

• prophecy variables that represent the final outputs of the demonic side(necessary for the completeness)• Please refer to [CAV 2021] for details and examples[CAV 2021] Unno et al. Constraint-Based Relational Verification.
January 16, 2024

VMCAI'24, London, UK

33

Implementation and Evaluation• Evaluated our solver PCSat for solving pfwCSP
on 20 relational verification problems:• 15 solved fully automatically, 5 required small hints

January 16, 2024

VMCAI'24, London, UK

34

The CoAR Verification & Synthesis Tool Chain(https://github.com/hiroshi-unno/coar)• Intermediate languages: (cf. CHCs, SyGuS, SemGuS, …)• pfwnCSP: predicate Constraint Satisfaction Problem with functionality, well-foundedness,& non-emptiness constrains [AAAI20, CAV21dt, CAV21rel, POPL23opt…]• 𝝁𝝁CLP: Constraint Logic Program with arbitrarily nested inductive & co-inductive
predicates (≈ fixpoint logic modulo theories) [POPL23mod, …]• Backends:• PCSat : pfwnCSP constraint solver/optimizer [AAAI20, CAV21dt, CAV21rel, POPL23opt, …]• MuVal : 𝝁𝝁CLP solver based on pfwnCSP solving [CAV21dt, POPL23mod, …]• MuCyc : 𝝁𝝁CLP solver based on cyclic-proof search [CAV17, POPL22, …]• Frontends:• Constraint generator for C [SAS19]• Constraint generator for LTS [CAV21dt, …] (LLVM IR to LTS translator available)• RCaml : constraint generator for OCaml [FLOPS08, PPDP09, POPL13, SAS15, POPL18, LICS18, CAV18, POPL23aem, POPL24, …]
January 16, 2024

VMCAI'24, London, UK

35

Discussion• Semantic self-composition has a high theoretical potential and promisingexperimental results have actually been obtained• Current limitations• Relational verifiers based on semantic self-composition exhibit increased searchcosts and reduced efficiency as the capability of representable schedulers grows• Future directions• Leverage various existing syntactic and semantic abstraction, search pruning, andsymmetry breaking techniques to accelerate the search

January 16, 2024

VMCAI'24, London, UK

36

Entailment Checking in 𝝁𝝁𝐂𝐂𝐋𝐋𝐏𝐏
January 16, 2024

VMCAI'24, London, UK

37

Program Refinement as Generalized Model Checking• Program refinement verification ⊨ 𝑝𝑝 ≤ 𝑞𝑞 generalizes ordinary model checking 𝑝𝑝 ⊨ 𝜙𝜙
• A specification of 𝒑𝒑 is given as a program 𝒒𝒒 instead of a logical formula 𝜙𝜙• 𝑞𝑞 can encode the given 𝜙𝜙 (if the programming language is expressive enough)• 𝑞𝑞 can be a reference implementation (cf. seL4 Project) oran abstract model represented as a highly non-deterministic program• This motivates me to investigate entailment checking problems 𝜓𝜓1 ⊨ 𝜓𝜓2 ina first-order fixpoint logic modulo theories we call 𝜇𝜇CLP [CAV 2017, LICS 2018, POPL 2023]• Relational verification boils down to entailment checking in 𝝁𝝁𝝁𝝁𝝁𝝁𝝁𝝁[CAV 2017] Unno et al. Automating Induction for Solving Horn Clauses.
[LICS 2018] Nanjo et al. A Fixpoint Logic and Dependent Effects for Temporal Property Verification.
[POPL 2023] Unno et al. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification.

January 16, 2024

VMCAI'24, London, UK

38

Example: Functional Program & Relational Spec.
(* recursive function to compute “x × y” *)let rec mult x y =if y = 0 then 0 else x + mult x (y - 1)(* tail recursive function to compute “x × y + a” *)let rec mult_acc x y a =if y = 0 then a else mult_acc x (y - 1) (a + x)(* functional equivalence of mult and mult_acc *)let main x y a = assert (mult x y + a = mult_acc x y a)
January 16, 2024

VMCAI'24, London, UK

39

CHCs Constraint Generation
based on Dependent Refinement Types [PPDP 2009]let rec mult x y =if y = 0 then 0
else x + mult x (y - 1)
let rec mult_acc x y a =if y = 0 then aelse mult_acc x (y - 1) (a + x)

let main x y a =assert (mult x y + a= mult_acc x y a)

[PPDP 2009] Unno, Kobayashi.
Dependent Type Inferencewith Interpolants.
January 16, 2024

VMCAI'24, London, UK

40

CHC Solving via Entailment Checking in 𝝁𝝁CLP

The CHCs on the right is satisfiable if and only if
the following entailment holds in 𝝁𝝁𝐂𝐂𝐂𝐂𝐂𝐂
where

𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 , 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2 ⊨ 𝑠𝑠1 + 𝑎𝑎 = 𝑠𝑠2

𝑦𝑦 = 0 ∨𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑧𝑧 =𝜇𝜇𝑦𝑦 ≠ 0 ∧ 𝑃𝑃 𝑥𝑥, 𝑦𝑦 − 1, 𝑟𝑟 ∧ 𝑧𝑧 = 𝑥𝑥 + 𝑟𝑟
𝑦𝑦 = 0 ∧ 𝑟𝑟 = 𝑎𝑎 ∨𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑟𝑟 =𝜇𝜇𝑦𝑦 ≠ 0 ∧ 𝑄𝑄 𝑥𝑥, 𝑦𝑦 − 1, 𝑎𝑎 + 𝑥𝑥, 𝑟𝑟
January 16, 2024

VMCAI'24, London, UK

41

𝝁𝝁CLP: An Extension of CLP with Quantifiers andArbitrarily-Nested (Co-)Inductive Predicates• Can be seen as a first-order fixpoint logic modulo background theories 𝑇𝑇(formulas) 𝜙𝜙 ∷= ⊥ ⊤ 𝐴𝐴 𝑡𝑡⃗(terms) 𝑡𝑡 ∷= 𝑥𝑥 | 𝑓𝑓 𝑡𝑡⃗¬𝜙𝜙 𝜙𝜙1 ∧ 𝜙𝜙2 | 𝜙𝜙1 ∨ 𝜙𝜙2 ∀𝑥𝑥. 𝜙𝜙 ∃𝑥𝑥. 𝜙𝜙 | 𝑝𝑝(𝑡𝑡⃗)(predicates) 𝑝𝑝 ∷= 𝑋𝑋 𝝁𝝁𝝁𝝁. 𝝀𝝀𝒙𝒙. 𝝓𝝓 𝝂𝝂𝝂𝝂. 𝝀𝝀𝒙𝒙. 𝝓𝝓• 𝐴𝐴 ranges over predicate symbols and 𝑓𝑓 ranges over function symbols in 𝑇𝑇,• 𝑥𝑥 ranges over term variables and 𝑋𝑋 ranges over predicate variables,• Predicates occur only positively in 𝝁𝝁𝝁𝝁. 𝝀𝝀𝒙𝒙. 𝝓𝝓 and 𝝂𝝂𝝂𝝂. 𝝀𝝀𝒙𝒙. 𝝓𝝓 for monotonicity• Least fixpoints 𝝁𝝁𝝁𝝁. 𝝀𝝀𝒙𝒙. 𝝓𝝓 represent inductive predicates, andgreatest fixpoints 𝝂𝝂𝝂𝝂. 𝝀𝝀𝒙𝒙. 𝝓𝝓 represent co-inductive predicates• We also use equational form: 𝑋𝑋 𝑥𝑥⃗ =𝜇𝜇 𝜙𝜙 and 𝑋𝑋 𝑥𝑥⃗ =𝜈𝜈 𝜙𝜙• Examples (integer arithmetic as 𝑇𝑇):
 𝜇𝜇𝜇𝜇. 𝜆𝜆𝑥𝑥. 𝑥𝑥 = 0 ∨ 𝑋𝑋 𝑥𝑥 − 1 𝑥𝑥 ⇔ 𝑥𝑥 = 0 ∨ 𝑥𝑥 = 1 ∨ 𝑥𝑥 = 2 ∨ ⋯ ⇔ ∃𝑧𝑧 ≥ 0. 𝑥𝑥 = 𝑧𝑧
∧ 𝑥𝑥 +
1 ≥ 0 ∧ 𝑥𝑥 + 2 ≥ 0 ∧ ⋯ ⇔ ∀𝑧𝑧 ≥ 0. 𝑥𝑥 +42𝑧𝑧 ≥ 0 𝜈𝜈𝜈𝜈.January
𝜆𝜆𝜆𝜆.16,𝑥𝑥2024≥ 0 ∧ 𝑋𝑋 𝑥𝑥 + 1 𝑥𝑥 ⇔ 𝑥𝑥 ≥ 0VMCAI'24,
London, UK

Entailment Checking via Inductive Theorem Proving
𝑃𝑃 𝑥𝑥, 0,0 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑥𝑥 + 𝑟𝑟 ⇐ 𝑃𝑃 𝑥𝑥, 𝑦𝑦 − 1, 𝑟𝑟 ∧ 𝑦𝑦 ≠ 0
𝑄𝑄 𝑥𝑥, 0, 𝑎𝑎, 𝑎𝑎 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑟𝑟 ⇐ 𝑄𝑄 𝑥𝑥, 𝑦𝑦 − 1, 𝑎𝑎 + 𝑥𝑥, 𝑟𝑟 ∧ 𝑦𝑦 ≠ 0
𝑠𝑠1 + 𝑎𝑎 = 𝑠𝑠2 ⇐ 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ∧ 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2
Prove this by
induction onderivation of
𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1
January 16, 2024

𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ∧ 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2 ⊨ 𝑠𝑠1 + 𝑎𝑎 = 𝑠𝑠2
VMCAI'24, London, UK

43

Principle of Induction on Derivation∀𝐷𝐷. 𝜓𝜓 𝐷𝐷 if and only if∀𝐷𝐷. ∀𝐷𝐷 ′ . 𝐷𝐷′ ≺ 𝐷𝐷 ⇒ 𝜓𝜓 𝐷𝐷′ ⇒ 𝜓𝜓 𝐷𝐷
where 𝐷𝐷′ ≺ 𝐷𝐷 represents that
𝐷𝐷′ is a strict sub-derivation of 𝐷𝐷

January 16, 2024

𝐷𝐷 =

𝐷𝐷1
𝐽𝐽3

𝐽𝐽2

𝐷𝐷2

𝐽𝐽1

𝐷𝐷3

𝐷𝐷4
𝐽𝐽4

VMCAI'24, London, UK

Assume 𝜓𝜓 𝐷𝐷1 , 𝜓𝜓 𝐷𝐷2 ,𝜓𝜓 𝐷𝐷3 , 𝜓𝜓 𝐷𝐷4 ,
⋮
⋮
⋮
𝜓𝜓
, 𝜓𝜓
, 𝜓𝜓
𝐽𝐽2
𝐽𝐽3
𝐽𝐽4
and prove 𝜓𝜓 𝐷𝐷
44

CHC Solving:

InductionTheorem
hypotheses
and lemmas
Inductive
Proving:

Judgment∅; 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 , 𝑄𝑄 𝑥𝑥, 𝑦𝑦, 𝑎𝑎, 𝑠𝑠2 ⊢ 𝑠𝑠1 + 𝑎𝑎 = 𝑠𝑠2
Premises

January 16, 2024

VMCAI'24, London, UK

45

Add an induction hypothesis:Guard to avoid unsound application∀𝑥𝑥 ′ , 𝑦𝑦 ′ , 𝑠𝑠1′ , 𝑎𝑎′ , 𝑠𝑠2′ . 𝐷𝐷 𝑃𝑃 𝑥𝑥 ′ , 𝑦𝑦 ′ , 𝑠𝑠1′ ≺ 𝐷𝐷 𝑃𝑃 𝑥𝑥, 𝑦𝑦, 𝑠𝑠1 ∧𝛾𝛾 =𝑃𝑃 𝑥𝑥′, 𝑦𝑦′, 𝑠𝑠1 ′ ∧ 𝑄𝑄 𝑥𝑥 ′ , 𝑦𝑦 ′ , 𝑎𝑎′ , 𝑠𝑠2′ ⇒ 𝑠𝑠1 ′ + 𝑎𝑎′ = 𝑠𝑠2 ′InductJanuary 16, 2024

Unfold Case analysis on the last rule used

VMCAI'24, London, UK

46

Case analysis on the last rule used
UnfoldJanuary 16, 2024

VMCAI'24, London, UK

47

January 16, 2024

VMCAI'24, London, UK

48

Validity checking
Valid

January 16, 2024

VMCAI'24, London, UK

49

January 16, 2024

VMCAI'24, London, UK

50

ValidJanuary 16, 2024

VMCAI'24, London, UK

51

January 16, 2024

VMCAI'24, London, UK

52

January 16, 2024

VMCAI'24, London, UK

53

Unfold

January 16, 2024

Case analysis on the last rule used

VMCAI'24, London, UK

54

January 16, 2024

VMCAI'24, London, UK

55

ValidJanuary 16, 2024

VMCAI'24, London, UK

56

January 16, 2024

VMCAI'24, London, UK

57

′ ′ ′
′ ′ ′
,
𝑎𝑎
,
𝑠𝑠
.
𝐷𝐷
𝑃𝑃
𝑥𝑥
,𝑃𝑃𝑦𝑦 𝑥𝑥,, 𝑠𝑠𝑦𝑦,1 𝑠𝑠1 ≺∧𝐷𝐷𝑃𝑃 𝑃𝑃∧ ∧∀𝑥𝑥
𝐷𝐷 𝑃𝑃′ , 𝑦𝑦
𝑥𝑥,′𝑦𝑦, 𝑠𝑠−
1,
𝑠𝑠
−
𝑥𝑥
≺
𝐷𝐷
𝑥𝑥, 𝑦𝑦𝑥𝑥,−𝑦𝑦,1,𝑠𝑠𝑠𝑠11 − 𝑥𝑥
1
1 2
𝜎𝜎 𝛾𝛾𝛾𝛾 ==𝑄𝑄 𝑦𝑦′,
𝑥𝑥, 𝑦𝑦𝑠𝑠1−′ 1,∧𝑎𝑎𝑄𝑄
+ 𝑥𝑥,
+ 𝑎𝑎′
𝑥𝑥) =
= 𝑠𝑠𝑠𝑠22 ′𝑥𝑥 ′𝑠𝑠,2𝑦𝑦 ′⇒, 𝑎𝑎′ 𝑠𝑠, 1𝑠𝑠2′− 𝑥𝑥⇒+𝑠𝑠1(𝑎𝑎′ +𝑃𝑃 𝑥𝑥′,
IndHyp Apply induction hypothesis

January 16, 2024

VMCAI'24, London, UK

58

ValidJanuary 16, 2024

VMCAI'24, London, UK

QED

59

Properties of the Inductive Proof System for CHCs
Solving• Soundness: If the goal is proved, the original CHCs have a solution (which may not be
expressible in the background theory)• Relative Completeness: If the original CHCs have a solution expressible in the
background theory, the goal is provable

January 16, 2024

VMCAI'24, London, UK

60

Automating Induction• Use the following rule application strategy:• Repeatedly apply INDHYP until no new premises are added• Apply VALID whenever a new premise is added• Select some 𝑃𝑃 𝑡𝑡̃ and apply INDUCT and UNFOLD• Close a proof branch by VALID that uses

• SMT solvers: provide efficient and powerful reasoning about data structures (e.g.,
integers, reals, algebraic data structures) but predicates are abstracted as
uninterpreted functions• CHC solvers: provide bit costly but powerful reasoning about inductive
predicates
January 16, 2024

VMCAI'24, London, UK

61

A Prototype Entailment Checker MuCyc
http://lfp.dip.jp/rcaml/• Use Z3 and SPACER respectively as the backend SMT and CHC solvers• Integrated with a dependent refinement type based CHC generation tool RCaml for OCaml• Currently support entailments in• The fragment corresponding to CHCs: 𝑃𝑃1 𝑥𝑥1 , … , 𝑃𝑃𝑛𝑛 𝑥𝑥𝑛𝑛 ⊨ 𝜙𝜙 and• 𝑃𝑃1 𝑥𝑥1 , … , 𝑃𝑃𝑛𝑛 𝑥𝑥𝑛𝑛 ⊨ 𝑄𝑄 𝑦𝑦⃗ , which is useful for program refinement verification and proving
lemmas to prove entailments in the above fragment (cf. commutativity proof of mult)• Can prove and then exploit lemmas which are:• User-supplied,• Heuristically conjectured from the given constraints, or• Automatically generated by an abstract interpreter• Can generate a counterexample (if any)
January 16, 2024

VMCAI'24, London, UK

62

Experiments on IsaPlanner Benchmark Set• 85 (mostly) relational verification problems of
total functions on inductively defined data structures

Inductive Theorem Prover
RCaml
Zeno
Support automatic
HipSpec
lemma discovery &CVC4goal generalization
ACL2s
IsaPlanner
Dafny
January 16, 2024

#Successfully Proved
68
82 [Sonnex+ ’12]
80 [Claessen+ ’13]
80 [Reynolds+ ’15]
74 (according to [Sonnex+ ’12])
47 (according to [Sonnex+ ’12])45 (according to [Sonnex+ ’12])

VMCAI'24, London, UK

63

Experiments on Benchmark Programs with
Advanced Language Features & Side-Effects• 30 (mostly) relational verification problems for:• Complex integer functions: Ackermann, McCarthy91• Nonlinear real functions: dyn_sys• Higher-order functions: fold_left, fold_right, repeat, find, ...
• Exceptions: find

• Non-terminating functions: mult, sum, …
• Non-deterministic functions: randpos• Imperative procedures: mult_Ccode

January 16, 2024

VMCAI'24, London, UK

64

• 28 (2 required lemmas) successfully proved by MuCyc• 3 proved by CHC constraint solver 𝝁𝝁Z PDR• 2 proved by inductive theorem prover CVC4 (if inductive
predicates are encoded using uninterpreted functions)January 16, 2024

VMCAI'24, London, UK

65

Discussion• The integration of SMT solving, CHC solving, and inductive theorem proving
resulted in an automated relational verifier across programs in various paradigms
with advanced language features and side-effects• Current limitations• Limited support for automatic lemma discovery and goal generalization• Does not support the full fragment of 𝝁𝝁CLP• Future directions• Generalize the recently observed connection of (co)inductive theorem proving toinvariant and ranking function synthesis [LICS 2018, POPL 2023] and software model
checking [POPL 2022] to the full fragment of 𝜇𝜇CLP
January 16, 2024

[LICS 2018] Nanjo et al. A Fixpoint Logic and Dependent Effects for Temporal Property Verification.
[POPL 2022] Tsukada, Unno. Software Model-Checking as Cyclic-Proof Search.
[POPL 2023] Unno et al. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification.
VMCAI'24, London, UK

66

Outline
1. Introduction

2. Challenges in Relational Verification

3. Automating Relational Verification
1. Self-Composition (or Product Programs) [CAV 2021]
2. Entailment Checking in 𝝁𝝁𝐂𝐂𝐋𝐋𝐏𝐏 [CAV 2017]
4. Current Limitations and Future Directions[CAV 2021] Unno et al. Constraint-Based Relational Verification.
[CAV 2017] Unno et al. Automating Induction for Solving Horn Clauses.
January 16, 2024

VMCAI'24, London, UK

67

Current Limitations of Both Approaches• It often becomes impossible to establish program refinement and equivalence, when
there is movement of statements across loops or recursions• E.g., loop-invariant code motion, loop interchange, loop fusion, …

• Using commutativity or idempotency at the right times may help establish
program refinement or equivalence, but more research is needed to automate it• Although not automated, the proof system for entailment in 𝝁𝝁CLP can prove commutativity
and idempotency and use them as lemmas to prove other entailments that involve reordering

January 16, 2024

VMCAI'24, London, UK

68

Ongoing and Future Work• Develop a general theory and algorithms for aligning reordered executions• Improve the efficiency of semantic self-composition by incorporating abstraction,
search pruning, and symmetry breaking techniques• Automate relational entailments checking in the full class of 𝜇𝜇CLP• Automate program verification of:• Temporal relational properties expressed in hyperlogics (HyperLTL, HyperCTL*, …)• Probabilistic relational properties, motivated fromsecurity, privacy, cryptography, and machine learning

January 16, 2024

VMCAI'24, London, UK

69

Conclusion• Relational verification amounts to synthesis of relational invariants and schedulers• Emerging semantic self-composition techniques enable precise alignment but
require further development to be refined into an efficient solver• An alternative approach based on entailment checking in 𝝁𝝁CLP, a first-orderfixpoint logic, shows promise, though it requires more automation through the
adoption of software model checking and theorem proving techniques to fully realize
the potential of this approach• In both automated approaches, aligning reordered executions remains a challenge

January 16, 2024

VMCAI'24, London, UK

70

Acknowledgements• This talk is based in part on the following two papers

1. Hiroshi Unno, Tachio Terauchi, Eric Koskinen:
Constraint-Based Relational Verification. CAV (1) 2021: 742-766

2. Hiroshi Unno, Sho Torii, Hiroki Sakamoto:
Automating Induction for Solving Horn Clauses. CAV (2) 2017: 571-591• I would like to thank my research collaborators Tachio and Eric as well as my former
students Sho and Hiroki.

January 16, 2024

VMCAI'24, London, UK

71

Questions?

January 16, 2024

VMCAI'24, London, UK

72