Envoy Formal Verifier

A formally verified tool written in Dafny for analyzing and verifying Envoy proxy configurations. This tool translates Envoy route configurations into SMT-LIB logic to mathematically prove properties about routing behavior.

Features

• Equivalence Checking (check-eq): Formally verify if two different Envoy configurations are semantically equivalent (i.e., route all possible packets to the same clusters).
• Route Query (query): Determine exactly which cluster a specific request path will be routed to for a given configuration.
• Redundancy Detection (verify-redundancy): Detect "dead code" or shadowed routes in your configuration that can never be reached.
• Formal Assurance: Built with Dafny, utilizing strong pre-conditions and post-conditions to guarantee the correctness of the parser and SMT generation logic.

Prerequisites

• Dafny (v4.x)
• Go (1.18+)
• Z3 SMT Solver (required for running the analysis logic)

Build Instructions

To verify the Dafny code and compile it into a standalone Go executable:

./scripts/build_go.sh

This will create an executable binary envoy-verifier in the project root.

Usage

1. Route Query

Find out where a packet goes.

./envoy-verifier query <config_file> <path>

Example:

./envoy-verifier query test_config.yaml /api/v1/user
# Output: Action: "cluster_api_service"

2. Equivalence Checking

Check if two configuration files behave exactly the same.

./envoy-verifier check-eq <config1.yaml> <config2.yaml>

Example:

./envoy-verifier check-eq config_v1.yaml config_v2.yaml
# Output: RESULT: EQUIVALENT (or NOT EQUIVALENT with counter-example)

3. Redundancy Verification

Check for unreachable routes (shadowed by earlier rules).

./envoy-verifier verify-redundancy <config_file>

Example:

./envoy-verifier verify-redundancy test_redundant.json
# Output: Redundant Route Found: Listener ..., VH ..., Route #1 (Config ID: 123)

4. Analyze (Dump SMT)

Dump the generated SMT-LIB logic for manual inspection or use with other solvers.

./envoy-verifier analyze <config_file>

Project Structure

• src/Program.dfy: Main entry point and CLI logic.
• src/EnvoyToSmt.dfy: Core logic for parsing JSON/YAML Envoy configs and translating them to SMT. Includes a verified JSON tokenizer and parser.
• src/Analysis.dfy: Implementation of verification algorithms (Equivalence, Redundancy, Query).
• test_config.yaml: Sample valid configuration for testing.

Verification Guarantees

This tool includes formally verified specifications:

• Parser Safety: Validates that the JSON parser always makes progress and handles malformed input safely.
• SMT Validity: Guarantees that generated SMT formulas are well-formed (non-empty, correct headers).
• Tokenizer Correctness: Proves bound and non-empty properties for all generated tokens.