Introduction

Domino is a tool for computer-assisted game-hopping and natively supports State-Separating Proofs.

Code is defined in a pseudocode-like language. The tool generates SMT-LIB 2.6 code, which can be used to prove statements about the code. We are mostly interested in proving equal behaviour of two programs (in order to justify a game-hop).

We also want to type-check our code and draw composition graphs as well as generate LaTeX code from it.

Getting Started

Tutorials

Concepts

Domino Project Structure

Directory Layout

The ssp binary operates on an directory containing both *.pkg.ssp package definitions and *.comp.ssp composition definitions. By default it will process all of them.

Proof Techniques

User Interfaces

Command Line Interface (CLI)

Domino CLI is currently the main user interface for parsing, type checking, proof verification, exporting to LaTeX. This section explains the subcommands that CLI provides.

domino prove
domino latex
domino proofsteps

Tip

If you are getting started with a project, it is a good idea to export the project to LaTeX which contains the composition diagrams next to the code of packages as well as the theorems proved in the project with their proof steps. See domino latex for more information.

Tip

domino --version prints the commit hash of the Domino version you are using. Please include its output when reporting issues.

`domino prove`

This is the most useful command that you use most of the time when working with Domino. It parses and type checks the project and then verifies the proofs. There are several options for the command that we explain here.

Important

Run this command at the root of a Domino project, where ssp.toml is located.

`-t` or `--transcript`

This option instructs Domino to store the SMT obligations it passes to its prover backend as a SMT-LIB files under the directory _build/code_eq in the current project. Domino generates a separate .smt2 file for each claim (invariant, same-output, equal-aborts, and user-defined lemmata) in each oracle exposed by each pair of equivalent games, i.e. {left-game-instance-name}-{right-game-instance-name}-{oracle-name}-{claim}.smt2.

Tip

Use this option for debugging as well as learning how Domino verifies your code equivalence game hops under the hood. You may run your favorite SMT solver directly on this file with various debugging options.

`-s <SMTSOLVER>` or `--smtsolver <SMTSOLVER>`

This option instructs Domino to use the given SMT solver backend. Possible values are cvc5, cvc4, and z3. Default solver is CVC5.

Warning

Currently, we have tested our example projects only with cvc5.

`--proof <PROOF>`

This option instructs Domino to only attempt proving the given theorem. Notice that the theorem name defined with the theorem block in the theorem file is considered, not the name of theorem file. For example:

domino prove --proof Simple4WHS

`--proofstep <PROOFSTEP>`

Given that the previous --proof option is provided, user can specify the numeric index of the game hop they wish to verify in the given theorem <PROOF>. Game hops in a gamehop block are indexed from top to bottom starting from zero. For example:

domino prove --proof Simple4WHS --proofstep 0

`--oracle <ORACLE>`

Given that the previous two options --proof and --proofstep are provided and the game hop corresponding to <PROOFSTEP> is an equivalence game hop, the user can specify the name of the oracle they wish to be verified. For example:

domino prove --proof Simple4WHS --proofstep 0 --oracle NewKey

`--parallel <THREADS>`

This option instructs Domino to spawn a thread pool of size <THREADS> + 1 for SMT solving. It defaults to 1, i.e. 2 threads; therefore, parallel solving is on by default.

`domino latex`

This command instructs Domino to export composition diagrams (in TikZ) next to the pseudocode of the packages (with CryptoCode) to LaTeX. Moreover, it states the theorems proved in the project and the game hops for each of them.

The output LaTeX files are stored under the directory _build/latex in the current project. Some files are marked with _lossy in the end of their names. These are intended to contain a more readable version of the pseudocode of packages for cryptographers or anyone who may care less about the syntactic salt of Domino.

Tip

Domino generates two LaTeX files (called Theorem_{Theorem-Name}.tex and Theorem_{Theorem-Name}_lossy.tex) for each theorem in the project. Consider compiling either of these two files if you want to get an overview of the project.

Warning

It might take a few seconds or minutes for the job to finish. Be patient! Read the rest of the section to see why!

`-s <SOLVER>` or `--smtsolver <SOLVER>`

This option instructs Domino to use the given SMT solver for generating composition diagrams. Possible values are cvc4, cvc5, and z3. It defaults to z3.

Tip

While z3 works much faster, especially on large examples it is possible to use cvc5 as well – for example if you currently do not have z3 installed.

Note

How come there is an SMT solver used for LaTeX export?

Eye-catching SSP diagrams can not be generated carelessly. Packages shall not overlap. Calling packages shall lie to the left of the callee packages. Edges shall not cross packages. There should be enough spacing between packages and edges to be aesthetically charming.

These requirements require a careful algorithm to be designed. However, as developers of a formal verification tool, we decided to formally state our requirements and let the solver to find a solution adhering to our specifications. Read more about the constraints passed to the SMT solver here.

`domino proofsteps`

This command outputs a one-line summary (equivalence or reduction to which assumption) of the game hops for each theorem in the project.

Language Reference

Invariants, Lemmata, and Randomness Mapping

Domino allows the user to express their state relations, lemmata, and randomness mappings with SMT-LIB language. Additionally, Domino defines a syntactic sugar to help writing these relations.

Invariants

For each equivalence game hop, Domino expects us to define a function called invariant which takes the states of the left and right sides of the code equivalence.

(define-fun invariant 
    (
        (left-state <GameState_{left-game-instance-name>}_<$<!{int-param-1}!>...<!{int-param-n}!>$>>)
        (right-state <GameState_{right-game-instance-name>}_<$<!{int-param-1}!>...<!{int-param-n}!>$>>)
    )
    Bool
    ; your invariant
)

Notice that the game instance name shall be the same as the name used when instantiating the name in the theorem. Moreover, only integer parameters of the games (in the order of declaration in the composition files) appear in the game state type. For example:

(define-fun invariant
    (
        (left-game <GameState_Left_<$<!n!><!m!>$>>)
        (right-game <GameState_Right_<$<!n!><!m!>$>>)
    )
    Bool
    true
)

Tip

You can find the exact type for your game states in the transcripts generated by Domino CLI. Read about transcripts in CLI options.

Note

Why only integer parameters?

Integer parameters can be used to declare bit string types (Bits(n)) and bit strings are translated to a corresponding Bits_n. That is, unlike other parameters (functions, booleans, etc.) they can be used to modify types and not just code of packages. Therefore, the current implementation creates a new game (and package) state type for each combination of concrete bit string types. For instance, if a game with an integer parameter nis instantiated with literal integer 256 as well as a theorem parameter skeylen, two game states with <!256!> and <!skeylen!> in their names are defined in the transcript.

Warning

It is possible that in future, only integers used for type modifications are used in the game state type names. Therefore, it is always a good idea to check the transcript.

Domino Book