Methodology Reference: NCT / NACT / NSCT

Overview

PANTHER's Ivy formal verification integrates three complementary compositional testing methodologies:

Methodology	Full Name	Perspective	Environment
NCT	Network-Centric Compositional Testing	Specification compliance	Real network
NACT	Network-Attack Compositional Testing	Attacker behavior	Real network
NSCT	Network-Simulator Centric Compositional Testing	Scale & topology	Simulated network

All three share the same foundational Ivy formal specification language and the 14-layer template architecture, but differ in their testing perspective, entity roles, and execution environment.

---

1. NCT -- Network-Centric Compositional Testing

1.1 Core Concept

NCT tests protocol implementations by having a formal specification play one role in the protocol (client, server, or man-in-the-middle) against an Implementation Under Test (IUT). The formal specification: - Generates test traffic using Z3/SMT symbolic execution - Monitors received packets against specification assertions - Checks that the IUT's behavior complies with the protocol specification

This is "compositional" because the specification is decomposed into modular layers that can be tested independently or composed.

1.2 Role Inversion

A key concept in NCT: the Ivy tester's role is the opposite of what it tests. - Testing a QUIC server -> Ivy acts as a formal client (quic_server_test_ files) - Testing a QUIC client -> Ivy acts as a formal server (quic_client_test_ files) - MIM testing -> Ivy acts as a man-in-the-middle (quic_mim_test_* files)

The oppose_role() function in panther_ivy handles this mapping.

1.3 Specification Structure

Protocol specifications use a layered architecture with monitors (before/after clauses) attached to protocol events:

before clauses (preconditions/guards): - Define what conditions must hold before an event can occur - Act as guards: if the precondition fails, the event is blocked - Example: before sending a packet, the connection must be in the correct state

after clauses (state updates/checks): - Define state updates and checks after an event occurs - Record history information by updating shared variables - Check specification compliance of received data - Example: after receiving a packet, verify it has the correct format and update connection state

_finalize() (end-state verification): - Called when the test completes - Performs heuristic checks on the overall test outcome - Example: verify that some data was actually received, no errors occurred

1.4 Test Specification Example (from QUIC)

Here is the structure of a QUIC server test (quic_server_test.ivy):

#lang ivy1.7

include order
include quic_infer
include file
include ivy_quic_shim_client        # Shim: Ivy acts as client
include quic_locale
include ivy_quic_client_behavior    # Entity behavior for client role

include ivy_quic_client_standard_tp  # Initial transport parameters
include quic_time

after init {
    # Initialize network sockets, TLS, transport parameters
    sock := net.open(endpoint_id.client, client.ep);
    client.set_tls_id(0);
    server.set_tls_id(1);
    var extns := tls_extensions.empty;
    extns := extns.append(make_transport_parameters);
    call tls_api.upper.create(0, false, extns);  # false = not a server
}

# Export actions to be generated by the test mirror
export frame.ack.handle
export frame.stream.handle
export frame.crypto.handle
export frame.path_response.handle
export packet_event
export client_send_event
export tls_recv_event

# Final verification
export action _finalize = {
    require is_no_error;
    require conn_total_data(the_cid) > 0;  # Some data was received
}

Test variants (e.g., quic_server_test_stream.ivy) include the base test and add weight attributes:

#lang ivy1.7
include quic_server_test
attribute frame.crypto.handle.weight = "5"
attribute frame.path_response.handle.weight = "5"

1.5 NCT Workflow

1. Select target protocol and RFC -- identify which protocol to test and which RFC defines it
2. Decompose into 14 formal layers -- map RFC sections to the template layers
3. Write type definitions -- {prot}_types.ivy (foundation layer)
4. Build core stack -- frames -> packets -> protection -> connection
5. Define entity roles -- client, server, MIM instances
6. Write behavioral constraints -- before/after monitors encoding RFC requirements
7. Create test specifications -- role-specific tests with _finalize
8. Verify -- ivy_check for formal properties
9. Compile -- ivyc target=test to produce test binaries
10. Execute against IUT -- run compiled test against implementation

1.6 Directory Structure

protocol-testing/{prot}/
├── {prot}_stack/          # Core protocol model (layers 1-9)
├── {prot}_entities/       # Entity definitions and behavior (layers 10-12)
├── {prot}_shims/          # Implementation bridge (layer 12)
├── {prot}_utils/          # Serialization, utilities (layers 13-14)
├── {prot}_tests/
│   ├── server_tests/      # Tests targeting server IUTs (Ivy acts as client)
│   ├── client_tests/      # Tests targeting client IUTs (Ivy acts as server)
│   └── mim_tests/         # Man-in-the-middle tests
└── {prot}_attacks_stack/  # Optional APT integration

1.7 Serena Tools for NCT

Step	Serena Tool	Purpose
Navigate specs	find_symbol, get_symbols_overview	Understand existing spec structure
Read spec code	read_file	Read specific sections of .ivy files
Trace deps	find_referencing_symbols	Find what references a symbol
Search patterns	search_for_pattern	Find patterns across specs
Verify	ivy_check	Check formal properties
Compile	ivy_compile	Build test executables
Inspect model	ivy_model_info	View model types, relations, actions
Create specs	create_text_file	Write new .ivy files
Edit specs	replace_symbol_body	Modify existing symbols

---

2. NACT -- Network-Attack Compositional Testing

2.1 Core Concept

NACT extends NCT to model and test from an attacker's perspective. It uses the APT (Advanced Persistent Threat) lifecycle model to systematically test security properties of protocol implementations. Attack specifications use the same Ivy formal language and before/after monitor pattern as NCT.

2.2 APT 6-Stage Lifecycle

The APT lifecycle is organized into 3 phases with 6 stages plus a cross-cutting concern:

Phase 1: Infiltration 1. Reconnaissance -- Gather information about the target (WHOIS, DNS queries, port scanning, service enumeration, OS fingerprinting, banner grabbing). Defined in attack_reconnaissance.ivy. - Actions: launch_whois_lookup(), launch_dns_query(), endpoint_scanning(src, dst) - Types: passive (OSINT, social engineering) and active (port scanning, network scanning)

1. Infiltration -- Initial access to the target network. Defined in attack_infiltration.ivy.

2. C2 Communication -- Establish command & control channels. Defined in attack_c2_communication.ivy.

Phase 2: Expansion 4. Privilege Escalation -- Gain higher access levels. Defined in attack_privilege_escalation.ivy.

1. Persistence -- Maintain access to the compromised system. Defined in attack_maintain_persistence.ivy.

Phase 3: Extraction 6. Exfiltration -- Extract data from the target. Defined in attack_exflitration.ivy.

Cross-cutting: White Noise -- Distraction attacks to cover the primary attack. Defined in attack_white_noise.ivy.

The lifecycle is composed in attack_life_cycle.ivy:

#ivy lang1.7
include attack_white_noise
# Infiltration
include attack_reconnaissance
include attack_infiltration
include attack_c2_communication
# Expansion
include attack_privilege_escalation
include attack_maintain_persistence
# Extraction
include attack_exfiltration

2.3 APT Directory Structure

protocol-testing/apt/
├── apt_entities/              # Attack entity definitions (attacker, bot, C2, target, MIM)
├── apt_entities_behavior/     # Attack entity behavioral constraints
├── apt_lifecycle/             # 6-stage lifecycle definitions
│   ├── attack_life_cycle.ivy  # Master include file
│   ├── attack_reconnaissance.ivy
│   ├── attack_infiltration.ivy
│   ├── attack_c2_communication.ivy
│   ├── attack_privilege_escalation.ivy
│   ├── attack_maintain_persistence.ivy
│   ├── attack_exflitration.ivy
│   ├── attack_white_noise.ivy
│   ├── apt_attack_connection.ivy
│   ├── apt_datagram.ivy
│   ├── apt_packet.ivy
│   └── (protocol-specific bindings:)
│   ├── quic_apt_lifecycle/    # QUIC-specific attack bindings
│   ├── minip_apt_lifecycle/   # MiniP-specific attack bindings
│   ├── udp_apt_lifecycle/     # UDP-specific attack bindings
│   └── stream_data_apt_lifecycle/
├── apt_network/               # Attack network infrastructure models
├── apt_protocols/             # Protocol-specific APT integration
│   └── {prot}/                # Per-protocol attack model overlays
├── apt_shims/                 # Attack implementation bridges
├── apt_stack/                 # Attack protocol stack layers
├── apt_tests/                 # Attack test specifications
│   ├── server_attacks/        # Tests attacking server IUTs
│   ├── client_attacks/        # Tests attacking client IUTs
│   └── mim_attacks/           # Man-in-the-middle attack tests
├── apt_utils/                 # Attack utilities
└── test/                      # Test infrastructure

2.4 Protocol-Specific Bindings

Each supported protocol has attack bindings that connect the generic APT lifecycle to protocol-specific actions: - QUIC: quic_apt_lifecycle/ -- maps reconnaissance to QUIC endpoint scanning, infiltration to connection manipulation, etc. - MiniP: minip_apt_lifecycle/ -- simplified protocol attack bindings - UDP: udp_apt_lifecycle/ -- basic datagram-level attack bindings - Stream Data: stream_data_apt_lifecycle/ -- stream-oriented attack bindings

2.5 NACT Workflow

1. Define threat model -- Identify which APT stages apply to the target protocol
2. Design attack entities -- Define attacker roles and capabilities in apt_entities/
3. Write attacker behavioral constraints -- FSM and before/after monitors for attack actions
4. Create protocol-specific bindings -- Map generic attack stages to protocol actions
5. Write attack test specifications -- Create test files in apt_tests/
6. Verify attack specs -- ivy_check to ensure attack model consistency
7. Compile attack tests -- ivyc to produce attack test executables
8. Execute against IUT -- Run attack tests against protocol implementations
9. Analyze security properties -- Check whether IUT correctly handles attack scenarios

2.6 Serena Tools for NACT

Same tools as NCT (section 1.7), with additional focus on: - Navigating apt/ directory structure - Understanding attack entity formal models - Tracing protocol-specific bindings

---

3. NSCT -- Network-Simulator Centric Compositional Testing

3.1 Core Concept

NSCT uses the Shadow Network Simulator to run protocol tests in a deterministic, simulated network environment. This enables: - Scale testing: Run many nodes simultaneously in a controlled environment - Topology testing: Define complex network topologies (meshes, hierarchies, partitions) - Deterministic replay: Same simulation produces same results (useful for debugging) - Network condition modeling: Simulate latency, loss, bandwidth constraints

3.2 Shadow NS Integration

PANTHER integrates Shadow NS as an execution environment alternative to Docker Compose: - Docker Compose (NCT/NACT): Real network stack, isolated containers - Shadow NS (NSCT): Simulated network stack, deterministic execution

Configuration uses PANTHER experiment configs with type: shadow_ns in the network_environment section:

tests:
  - name: "NSCT Test"
    network_environment:
      type: shadow_ns
      topology:
        # Shadow NS topology configuration
    services:
      server:
        implementation:
          name: picoquic
          type: iut
        protocol:
          name: quic
          version: rfc9000
          role: server

3.3 When to Use NSCT vs NCT

Criterion	NCT (Real Network)	NSCT (Simulated)
Fidelity	High (real OS stack)	Medium (simulated stack)
Scale	Limited (container resources)	High (many simulated nodes)
Determinism	Non-deterministic	Deterministic
Topology control	Basic (Docker networks)	Full (arbitrary topologies)
Network conditions	Limited manipulation	Full control
Debugging	Harder (non-deterministic)	Easier (deterministic replay)
Performance testing	Realistic	Simulated

3.4 NSCT Workflow

1. Define network topology -- Specify nodes, links, latencies, bandwidths
2. Configure simulation parameters -- Duration, seed, logging level
3. Set up protocol implementations -- Map IUTs to simulated nodes
4. Define formal specifications -- Same Ivy specs as NCT (reuse)
5. Run simulation-based verification -- Execute via PANTHER with shadow_ns environment
6. Analyze results -- Examine simulation logs and verification output

3.5 Complementarity

The three methodologies are designed to be complementary: - NCT verifies specification compliance in realistic conditions - NACT verifies security properties under adversarial conditions - NSCT verifies behavior at scale and under varied network conditions

A comprehensive testing campaign would use all three: 1. NCT to verify basic protocol compliance 2. NACT to test resilience against attacks 3. NSCT to verify behavior at scale and under adverse network conditions

---

4. The 14-Layer Template (Shared Foundation)

All three methodologies share the same 14-layer formal model template. This template provides a structural pattern for decomposing any network protocol into modular Ivy specifications.

4.1 Core Protocol Stack (Layers 1-9, Always Required)

#	Layer	File Pattern	Purpose
1	Type Definitions	{prot}_types.ivy	Identifiers, bit vectors, enumerations
2	Application	{prot}_application.ivy	Data transfer semantics
3	Security/Handshake	{prot}_security.ivy	Key establishment, handshake
4	Frame/Message	{prot}_frame.ivy	Protocol data unit definitions
5	Packet	{prot}_packet.ivy	Wire-level packet structure
6	Protection	{prot}_protection.ivy	Encryption/decryption
7	Connection/State	{prot}_connection.ivy	Session lifecycle
8	Transport Parameters	{prot}_transport_parameters.ivy	Negotiable parameters
9	Error Handling	{prot}_error_code.ivy	Error taxonomy

4.2 Entity Model (Layers 10-12, Always Required)

#	Layer	File Pattern	Purpose
10	Entity Definitions	ivy_{prot}_{role}.ivy	Network participant instances
11	Entity Behavior	ivy_{prot}_{role}_behavior.ivy	FSM and constraints
12	Shims	{prot}_shim.ivy	Implementation bridge

4.3 Infrastructure (Layers 13-14, Mostly Reusable)

#	Layer	File Pattern	Purpose
13	Serialization/Deserialization	{prot}_ser.ivy, {prot}_deser.ivy	Wire format encoding
14	Utilities	byte_stream.ivy, file.ivy, time.ivy, random_value.ivy, locale.ivy	Common utilities

4.4 Optional Layers

• Security Sub-Protocol (tls_stack/ or dtls_stack/)
• FSM Modules ({prot}_fsm/)
• Recovery & Congestion ({prot}_recovery/ or {prot}_congestion/)
• Extensions ({prot}_extensions/)
• Attacks Stack ({prot}_attacks_stack/)
• Stream/Flow Management ({prot}_stream.ivy)

4.5 Genuinely Reusable Components

Only these components are identical across protocols: - byte_stream.ivy -- byte stream manipulation - file.ivy -- file I/O - random_value.ivy -- random value generation - The shim pattern (not implementation) -- same bridge architecture - The _finalize() pattern -- same end-state verification approach - The before/after monitor pattern -- same specification approach

4.6 Decision Matrix

Protocol Property	Template Impact
Connection-oriented?	TCP layer, simplified packet structure
Built-in reliability?	Add recovery/congestion modules
Multiplexed streams?	Add stream management + per-stream FSM
Integrated security?	Add TLS/DTLS stack + protection layer
Peer-to-peer?	Symmetric entities (Speaker/Peer)
Pub/Sub pattern?	Add broker entity + topic/subscription
Extension mechanism?	Add extensions module
Stateless?	Simplify connection/state management
Tunneling?	Add encapsulation + SA management
Real-time?	Add timing constraints + FEC recovery

---

5. Serena Tool Reference for All Methodologies

5.1 Ivy-Specific Tools (from panther-serena)

ivy_check -- Formal verification - Parameters: relative_path (str), isolate (str|None), max_answer_chars (int) - Runs: ivy_check [isolate=X] path.ivy - Checks: isolate assumptions, invariants, safety properties - Returns: JSON {stdout, stderr, return_code}

ivy_compile -- Test compilation - Parameters: relative_path (str), target (str, default "test"), isolate (str|None), max_answer_chars (int) - Runs: ivyc target=X [isolate=Y] path.ivy - Produces: compiled test executable - Returns: JSON {stdout, stderr, return_code}

ivy_model_info -- Model introspection - Parameters: relative_path (str), isolate (str|None), max_answer_chars (int) - Runs: ivy_show [isolate=X] path.ivy - Shows: types, relations, actions, invariants, isolates - Returns: JSON {stdout, stderr, return_code}

5.2 Standard Serena Tools (for code navigation)

Tool	Purpose	When to Use
find_symbol	Find symbol by name path	Navigate to specific functions/modules
get_symbols_overview	List top-level symbols in file	Understand file structure
find_referencing_symbols	Find what references a symbol	Trace dependencies
search_for_pattern	Regex search across files	Find patterns in specs
read_file	Read file contents	View specific .ivy files
create_text_file	Create new file	Write new specs
replace_symbol_body	Replace symbol implementation	Edit existing specs
replace_content	Replace content by regex	Fine-grained edits
list_dir	List directory contents	Explore directory structure
find_file	Find file by name	Locate spec files

---

6. File Naming Conventions

Pattern	Example (QUIC)	Description
{prot}_types.ivy	quic_types.ivy	Type definitions
{prot}_frame.ivy	quic_frame.ivy	Frame/message definitions
{prot}_packet.ivy	quic_packet.ivy	Packet structure
ivy_{prot}_{role}.ivy	ivy_quic_client.ivy	Entity definition
ivy_{prot}_{role}_behavior.ivy	ivy_quic_client_behavior.ivy	Entity behavior
{prot}_shim.ivy	quic_shim.ivy	Implementation bridge
{prot}_server_test.ivy	quic_server_test.ivy	Base server test
{prot}server_test.ivy	quic_server_test_stream.ivy	Test variant
{prot}_ser.ivy / {prot}_deser.ivy	quic_ser.ivy / quic_deser.ivy	Serialization
attack_{stage}.ivy	attack_reconnaissance.ivy	APT lifecycle stage
{prot}_apt_lifecycle/	quic_apt_lifecycle/	Protocol-specific APT bindings