2021.07.13: Bidirectional Type Checking for Relational Properties
Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg [2019],
Bidirectional Typechecking For Relational Properties
presenter: Lisa
Problem statement
Relational type and effect systems are appealing for simple and precise verification of information flow, differential privacy, and cost analysis. However, they lack a general foundation for implementing them.
In this paper, we develop bidirectional versions of several relational type systems which incrementally combine many different components for expressive relational analysis.
Implementation and examples
https://github.com/ezgicicek/BiRelCost
1. Introduction
Relational properties of programs consider pairs of execution traces.
In information flow control they describe equivalence between the values that are observable at a specific security level.
Relational refinements types – their interpretation is a relation between the values in the two executions.
Relational effects are usually quantitative. In differential privacy – level of indistinguishability between the outputs on two inputs differing in one data element.
2. Relational STLC (relSTLC)
no refinements, no effects, two programs with the same structure
Soundness, If either Γ ⊢ e1 ∽ e2 ↑ τ or Γ ⊢ e1 ∽ e2 ↓ τ, then Γ ⊢ |e1| ∽ |e2| : τ.
Completeness, If Γ ⊢ e1 ∽ e2 : τ , then there are type-annotated e1’ and e2’ such that Γ ⊢ e1′ ∽ e2′ ↑ τ. These annotations can be limited to the top-level and any explicit β-redexes
3. RelRef
+ relational refinement types over lists
+ syntactic equality of two values
=> additional non-syntax-directedness
RelRef Core
+ new kind of annotations to resolve it
+ equality modulo SMT-constraints instead of n-s-d subtyping
Lemma If ∆; Φa |= τ ⊑ τ′ in RelRef then there exists e ∈ RelRef Core s.t. ∆; Φa ; · ⊢ e ∽ e :c τ → τ’.
Soundness and completeness of the bidirectional system are proven wrt RelRef Core.
4. RelRefU
+ programs of possibly dissimilar syntactic structure
Soundness and completeness wrt RelRefU Core.
5. RelCost
+ relational effects
RelCostCore
6. Implementation
Constraint solving with existentials
7. Discussion
Possible extensions
- Γ ⊢ e ∽ e’ : τ ~ τ’ | p
- Mixed inference and checking for two expressions in one relational rule
9. Conclusion
Discussion
Main contribution - the first (extensible) bidirectional system for relational TT
2021.07.13: Bidirectional Type Checking for Relational Properties
Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg [2019],
Bidirectional Typechecking For Relational Properties
presenter: Lisa
Problem statement
Relational type and effect systems are appealing for simple and precise verification of information flow, differential privacy, and cost analysis. However, they lack a general foundation for implementing them.
In this paper, we develop bidirectional versions of several relational type systems which incrementally combine many different components for expressive relational analysis.
Implementation and examples
https://github.com/ezgicicek/BiRelCost
1. Introduction
Relational properties of programs consider pairs of execution traces.
In information flow control they describe equivalence between the values that are observable at a specific security level.
Relational refinements types – their interpretation is a relation between the values in the two executions.
Relational effects are usually quantitative. In differential privacy – level of indistinguishability between the outputs on two inputs differing in one data element.
2. Relational STLC (relSTLC)
no refinements, no effects, two programs with the same structure
Soundness, If either Γ ⊢ e1 ∽ e2 ↑ τ or Γ ⊢ e1 ∽ e2 ↓ τ, then Γ ⊢ |e1| ∽ |e2| : τ.
Completeness, If Γ ⊢ e1 ∽ e2 : τ , then there are type-annotated e1’ and e2’ such that Γ ⊢ e1′ ∽ e2′ ↑ τ. These annotations can be limited to the top-level and any explicit β-redexes
3. RelRef
+ relational refinement types over lists
+ syntactic equality of two values
=> additional non-syntax-directedness
RelRef Core
+ new kind of annotations to resolve it
+ equality modulo SMT-constraints instead of n-s-d subtyping
Lemma If ∆; Φa |= τ ⊑ τ′ in RelRef then there exists e ∈ RelRef Core s.t. ∆; Φa ; · ⊢ e ∽ e :c τ → τ’.
Soundness and completeness of the bidirectional system are proven wrt RelRef Core.
4. RelRefU
+ programs of possibly dissimilar syntactic structure
Soundness and completeness wrt RelRefU Core.
5. RelCost
+ relational effects
RelCostCore
6. Implementation
Constraint solving with existentials
7. Discussion
Possible extensions
8. Related Work
9. Conclusion
Discussion
Main contribution - the first (extensible) bidirectional system for relational TT