| name | defensibility-analysis-shield-synthesis |
| description | Network defensibility analysis using shield synthesis and adversarial game theory. Reinterprets shielded RL from runtime enforcement to design-time structural analysis. Use when: analyzing network topology security, synthesizing safety shields for RL agents, computing defensibility verdicts for cyber-physical systems, designing secure multi-agent architectures, evaluating network architecture defensibility, or combining formal verification with adversarial RL. |
Defensibility Analysis via Shield Synthesis
Core Concept
Shield synthesis reinterpreted as a design-time analytical instrument rather than runtime enforcement. The automata-theoretic machinery (specification compilation, product game construction, attractor computation, winning-region extraction) produces structural insights about a system, not runtime constraints on deployed agents.
Methodology
Step 1: Two-Player Safety Game Construction
def construct_defense_game(network_topology, defender_spec, attacker_spec):
"""
Build constrained two-player safety game for network defense.
- Defender spec defines the unsafe region
- Attacker spec restricts adversary legal actions during attractor computation
"""
product_game = compile_specifications(network_topology, defender_spec, attacker_spec)
winning_region = compute_attractor(product_game, attacker_restricted=True)
return product_game, winning_region
Step 2: Defensibility Verdict
def compute_defensibility(winning_region, network_topology):
"""Compute formal certificate: defensible iff initial_state in winning_region"""
return network_topology.initial_state in winning_region
Step 3: Topology Metrics from Attractor Structure
def compute_defensibility_metrics(winning_region, attractor_structure):
return {
'coverage': len(winning_region) / len(attractor_structure.states),
'critical_nodes': find_attractor_bottlenecks(attractor_structure),
'basin_depths': compute_attractor_depths(attractor_structure)
}
Step 4: Defensibility Fingerprint
def compute_defensibility_fingerprint(formal_metrics, operational_behavior):
"""Combine formal safety with operational behavior from shield-constrained adversarial RL"""
return {
'formal_safety': formal_metrics,
'operational_effectiveness': operational_behavior,
'alignment': compare_formal_vs_operational(formal_metrics, operational_behavior)
}
Key Insights
- Defensibility verdict is the output, not the safe policy
- Small architecture changes cause large operational shifts while formal safety margins remain unchanged
- Formal defensibility and operational effectiveness capture distinct security aspects
- Shield synthesis answers architectural questions about whether, where, and how a system can be defended
When to Use
- Evaluating whether a network topology is formally defensible
- Design-time security analysis before deployment
- Comparing architectural alternatives for security posture
- Synthesizing safety constraints for RL-based network defense
- Multi-agent adversarial simulation for security assessment
- Cyber-physical system security certification
