# 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 systemsare 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 systemswhich incrementally combine many different components for expressive relational analysis.## Implementation and examples

https://github.com/ezgicicek/BiRelCost

## 1. Introduction

Relational propertiesof 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 effectsare 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-directednessRelRef Core+new kind of annotations to resolve it+equality modulo SMT-constraints instead of n-s-d subtypingLemmaIf ∆; Φa |= τ ⊑ τ′ in RelRef then there exists e ∈ RelRef Core s.t. ∆; Φa ; · ⊢ e ∽ e :c τ → τ’.Soundnessandcompletenessof the bidirectional system are proven wrt RelRef Core.## 4. RelRefU

+programs of possibly dissimilar syntactic structureSoundnessandcompletenesswrtRelRefU Core.## 5. RelCost

+relational effectsRelCostCore## 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