Panther Ivy Tester¤

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.

Requirements and Dependencies¤

The plugin requires:

• Ivy: The Ivy formal verification framework
• Python: Python 3.10 or higher
• Protocol Model: Formal specification of the protocol in Ivy language
• Build Tools: C++ compiler and related development tools

See the Installation Website for detailed setup instructions.

Docker-based deployment installs all necessary dependencies automatically.

Overview: Integration with Microsoft's Ivy formal verification tool for protocol verification and specification-based testing. Panther-Ivy provides compositional specification-based testing where formal protocol models generate test traffic and verify implementation compliance.

Complete Workflow Architecture:

Configuration Options¤

The Panther Ivy Tester accepts the following configuration parameters:

services:
  panther_ivy:
    name: "quic_verifier"
    implementation:
      name: "panther_ivy"
      type: "tester"
    protocol:
      name: "quic"
      version: "rfc9000"
      role: "tester"
    config:
      test: "quic_server_test_stream"  # Ivy test name
      build_mode: ""                   # Z3 build mode (see Build Modes)
      timeout: 120                     # Timeout in seconds
      iterations_per_test: 1           # Number of iterations per test
      internal_iterations_per_test: 300  # Solver loop iterations
      use_system_models: false         # Use APT system models
      z3_source: "local"               # Z3 source: "local" or "pip"
      log_level_events: "DEBUG"        # Event logging level
      log_level_binary: "DEBUG"        # Binary logging level

Build Modes¤

PANTHER-Ivy supports multiple build modes for different optimization and debugging needs while preserving backward compatibility with Shadow Network Simulator.

Available Build Modes¤

Configuration Examples¤

Original Method (Shadow Compatible):

services:
  panther_ivy:
    config:
      build_mode: ""  # or omit entirely

Debug Mode:

services:
  panther_ivy:
    config:
      build_mode: "debug-asan"

High Performance Mode:

services:
  panther_ivy:
    config:
      build_mode: "release-static-pgo"

Environment Variable Override¤

You can also set the build mode via environment variable:

export BUILD_MODE="rel-lto"

Shadow Network Simulator Compatibility¤

The original method (empty build_mode) is preserved exactly as before to ensure Shadow Network Simulator continues to work without changes. This uses: - Plain make with default C++11 standard - Shared libz3.so library - Legacy mk_make.py build system - No additional compilation flags

Supported Protocols¤

The Panther Ivy Tester has formal models for the following protocols:

QUIC¤

Ivy Protocol Models:

The Panther-Ivy system uses formal Ivy models that define:

# Example: QUIC Packet Structure
object packet = {
    object quic_packet = {
        variant this of packet = struct {
            ptype : quic_packet_type,
            pversion : version,
            dst_cid : cid,
            src_cid : cid,
            token : stream_data,
            seq_num : pkt_num,
            payload : quic_frame.arr
        }
    }
}

# Example: Packet Event
action packet_event(src:ip.endpoint, dst:ip.endpoint, pkt:packet.quic_packet) = {}

Protocol Layers Architecture:

┌─────────────────────────────────────┐
│         Application Layer           │  <- quic_application.ivy
├─────────────────────────────────────┤
│         Security Layer              │  <- quic_security.ivy
├─────────────────────────────────────┤
│         Frame Layer                 │  <- quic_frame.ivy
├─────────────────────────────────────┤
│         Packet Layer                │  <- quic_packet.ivy
├─────────────────────────────────────┤
│         Protection Layer            │  <- quic_protection.ivy
├─────────────────────────────────────┤
│         Datagram Layer (UDP)        │  <- Network interface
└─────────────────────────────────────┘

Integration with Implementations:

The system uses shim layers to interface with real protocol implementations:

# ivy_quic_shim.ivy - Interface between Ivy model and implementation
implement quic_net.recv(host:endpoint_id, s: quic_net.socket, src:ip.endpoint, pkts:net_prot.arr) {
    if host = endpoint_id.server {
        call server.behavior(host,s,src,pkts);
    } else if host = endpoint_id.client {
        call client.behavior(host,s,src,pkts);
    }
}

Test Result Analysis:

Test outputs include: - Trace files: Detailed execution traces showing packet exchanges - Invariant violations: When protocol properties are violated - Counterexamples: Specific sequences that expose bugs - Coverage reports: Which parts of the protocol were exercised - Performance metrics: Timing and resource usage

Available Test Categories:

Usage Examples¤

QUIC Protocol Verification¤

Example Test Execution:

# Experiment configuration excerpt
services:
  picoquic_server:
    implementation:
      name: "picoquic"
      type: "iut"
    protocol:
      name: "quic"
      role: "server"

  ivy_client:
    implementation:
      name: "panther_ivy"
      type: "testers"
      test: "quic_server_test_stream"
    protocol:
      name: "quic"
      role: "client"
      target: "picoquic_server"

This configuration creates a test where: 1. Picoquic runs as a QUIC server 2. Ivy acts as a formal client tester 3. The quic_server_test_stream test generates client traffic to test the server's stream handling 4. Results verify server compliance with QUIC specifications

Installation (old)¤

Linux¤

On Debian-based Linux ditributions such as Ubuntu, download and install the file panther-ms-ivy_X.X_YYYY.deb where X.X is the IVy version and YYYY is the machine architecture. Use your system’s package manager to install this package, or the following commands:

$ sudo dpkg -i panther-ms-ivy_X.X_YYYY.deb
$ sudo apt-get install -f

Windows¤

The Windows binary distribution is in the form of a zip archive. Download the file ivy.X.Y-.Windows-z86.zip, where X.X is the IVy version (this will work on both 32-bit and 64 bit Intel Windows). Use Windows Explorer to extract this archive in the directory C:\. This should give you a directory C:\ivy. To use IVy in a command window, first execute this command:

> C:\ivy\scripts\activate

Command Generation¤

The PantherIvy plugin uses a structured approach to command generation, ensuring proper escaping of special characters and reliable execution:

Structured Command Arguments¤

Commands are built as lists of arguments rather than concatenated strings. This allows for proper escaping of each argument:

# Example from generate_run_command
command_args = []
command_args.extend(["seed=", str(params_dict["seed"])])
command_args.extend(["server_addr=", params_dict["server_addr"]])
command_args.extend([">", "/app/logs/testers.log"])

Environment Variables¤

Environment variables are stored in dictionaries:

env_vars = {
    "IVY_LOG_LEVEL": log_level,
    "TEST_NAME": test_name,
    "PATH": "/usr/local/bin:/usr/bin"
}

Handling Edge Cases¤

The command generation system correctly handles edge cases such as:

• Paths with spaces: /path with spaces/file.txt
• Special characters: "Hello & Goodbye"
• Redirections: command > output.txt 2> error.log
• Environment variables with special values: KEY=value:with:colon;and;semicolons

Template Rendering¤

Command templates are rendered with proper escaping using Jinja2 filters:

rendered = template.render(
    command_args=command_args,  # List of properly escaped arguments
    env_vars=env_vars,          # Dictionary of environment variables
    extra_fields=extra_fields   # Any additional template-specific values
)

Important Note¤

Do not modify the template files directly. Instead, customize command generation by changing how data is passed to the templates. This ensures consistent behavior and proper character escaping.