Relational F* for State Separating Cryptographic Proofs

Introduction

This page documents a project started in April 2019 by Markulf Kohlweiss, Konrad Kohbrok, Tahina Ramananandro and Nikhil Swamy to use relational F* (TODO: Which paper to cite for relational F*?) to conduct cryptographic proofs written in the State-Separating Proof (SSP) framework introduced in [1].

State-Separating proofs

The state-separating proof (SSP) framework was introduced in [1] and is meant to help writing modular, code-based cryptographic proofs. To reason about oracles and the state they operate on, SSPs use Packages that contains a set of oracles and their shared state. Packages provide oracles, such that other packages or the adversary (who can also be seen as a package) can call them. We can thus, for example, instantiate a traditional security definition based in indistinguishability as the adversary's inability to distinguish between two packages up to some epsilon. In that example, the indistinguishability bit would be 0 in one package and 1 in the other. We call this indistinguishability up to some epsilon "epsilon-equivalence". Similarly, we can model a reduction as a package that is composed with (i.e. calls the oracles provided by) packages representing individual security assumptions.

Much like traditional cryptographic proofs, SSPs require proving that a given reduction (composed with a number of assumptions) simulates the original security game correctly for the adversary. This simulation correctness can be established by proving that the composed reduction is perfectly equivalent to the original security game.

After establishing simulation correctness, we can then use the package algebra provided by [1] to make game hops, for example to idealize a given assumption. Each game hop gives us epsilon-equivalence between two (composed) packages.

For a complete proof, we thus need (a) perfect equivalence between security game and composed reduction (for both the real and the ideal game), as well as a number of game hops that give us an epsilon-equivalence between the reduction equivalent to the real game and the reduction equivalent to the ideal game. We thus ultimately have an epsilon-equivalence between real- and ideal game, concluding the proof.

Stating and proving program equivalences in F*

We aim to formalize and mechanize the state-separating proofs for packages within F*.

We see several potential benefits of doing this:

• Working in F*'s dependently typed logic, we have the expressive power to speak about non-trivial equivalences at higher order

• F*'s support for effects allow us to reason about equivalences among effectful programs, where effects (especially state) are pervasive in the state-separating proofs methodology

• F*'s support for a combination of SMT and tactics may allow us to attain a good degree of automation for these proofs

• Given extensive prior work in F* on libraries that provide efficient, verified, low-level implementations of cryptographic primitives, we hope to be able to apply, through several steps of abstractions, our methodology for cryptographic security proofs to those low-level implementations themselves.

Towards this end, we have started to design a library in which to state equivalences, including epsilon equivalences, among values, functions, modules, and functors.

At the core of our library is a specification style based on relational types. For instances, one specification style we adopt is based on setoids (see Barthe et al. for an introduction), which equip a type with an equivalence relation---technically, we work with partial setoids which equip types with partial equivalence relation or PER, a symmetric, transitive relation that is not necessarily reflexive.

The following module defines our library of Setoids: https://github.com/FStarLang/FStar/blob/nik_lib/examples/rel/Setoids.fst

Using that library, we can state and prove several simple equivalences, automatically. For example, the code below proves that the identity function fun x -> x is relationally parametric, i.e., given any relation arel on the input type a, given x0 and x1 related by arel, id x0 and id x1 are also related by arel.

let id #a (arel:rel a) : (arel ^--> arel) = fun x -> x

Unpeeling the syntax a bit, given two relations arel: rel a and brel: rel b, the type arel ^--> brel is the type of functions f : a -> b that additionally satisfy the following property:

forall (x0 x1:a). arel x0 x1 ==> brel (f x0) (f x1)

That is, arel ^--> brel functions are those that take arel-related arguments to brel-related results.

One can also prove simple information-flow style properties by relational typing.

For instance, we can define the lo relation to be equality while the hi relation to be trivial---meaning that when relating two runs of a program, those inputs and outputs that are related by lo contain no secrets and can flow to/from the adversary, while values related by hi may contain secrets.

let lo a : rel a = fun x y -> x == y
let hi a : rel a = fun x y -> True

Using our relational function types, we can give information flow types to some simple programs:

let f1 : (lo int ^--> lo int) = fun x -> x + 45
let f2 : (hi int ^--> hi int) = fun x -> x + 45

Note, the same program can have more than one type (i.e., it may satisfy more than one relation), as in the case of f1 and f2. However, the same term given a type that claims it takes secret inputs and returns public outputs is rejected.

[@(expect_failure [19])]
let f3 : (hi int ^--> lo int) = fun x -> x + 45

Other programs that correctly hide their secret inputs from the adversary are easily accepted.

let f3 : (hi int ^--> lo int) = fun x -> x - x

Aside from these basic equivalences, one can also define relational variants of modules and functors.

Modules in F* (as in ML) are outside the language of terms and do not enjoy the same kinds of abstraction facilities. F* itself lacks any built-in support for functors in its module language.

However, to state equivalences among modules and functors, we encode modules and functors within F*'s term language. Specifically, we

• Encode modules as dependent maps from labels (the names of the symbols provided by a module) to values at a given relational type: the relation associated with a module is the pointwise conjunction of the relation of each of its operations
• Encode functors as relational-preserving maps from modules to modules
• Enable functors at higher-order, i.e., functors that transform functors to functors are also permitted

Within this regime, we are able to encode the packages of the state-separating proofs methodology as functors, and to prove the algebraic laws of package composition as equivalences among functor compositions. E.g., See https://github.com/FStarLang/FStar/blob/nik_lib/examples/rel/Setoids.fst#L443

We also make use of relational variants of monadic encodings of effects, e.g., the code here shows the definition of a relational variant of a state+exception monad. https://github.com/FStarLang/FStar/blob/nik_lib/examples/rel/Setoids.Example.fst#L16 Specifically, the type eff srel arel shown below is the type of computations that transform srel-related initial states to arel-related optional results and srel-related final states.

let eff (#s:Type) (#a:Type) (srel:erel s) (arel:erel a) =
  srel ^--> ((option_rel arel) ** srel)

Cryptographic Notions of Equivalence in F*

[TODO: Introduce signatures, modules and composition.] [TODO: Introduce epsilons and the eq type.]

[TODO: References. Most importantly a pointer to the code.] [1]: https://eprint.iacr.org/2018/306