Genrate Safe DAML Code Tools

**Goal**: Build a "DAML-Safe by Construction" Development Platform that enforces runtime security through multi-gate validation, leveraging DAML compiler's mathematical proofs and canonical security policy.

**Priority**: High  
**Estimated Effort**: 4-5 weeks  
**Dependencies**: [MCP Resources Infrastructure](https://github.com/ChainSafe/canton-mcp-server/issues/2) (Complete)

---

## Core Philosophy: Runtime Security Enforcement

**This is NOT a build-time tool. This is a production security platform that runs on every code generation request.**

### The Security Flow

```
User Request: "Generate transfer pattern"
    ↓
LLM Code Generation
    ↓
Gate 1: DAML Compiler Safety ← RUNS IN PRODUCTION
    ├─ PASS → Gate 2
    └─ FAIL → BLOCK (show user why + safe alternatives)
    ↓
Gate 2: Safety Annotations ← RUNS IN PRODUCTION
    ├─ PASS → Gate 3
    └─ FAIL → BLOCK (show user why + annotation requirements)
    ↓
Gate 3: Formal Verification ← RUNS IN PRODUCTION
    ├─ PASS → Gate 4
    └─ FAIL → BLOCK (show user why + composition issues)
    ↓
Gate 4: Production Readiness ← RUNS IN PRODUCTION
    ├─ PASS → Show code to user ✅
    └─ FAIL → BLOCK (show user why + testing requirements)
```

**Critical Understanding**: Each gate is production security infrastructure, not a test suite.

---

## Canonical Resources as Security Policy

### What Canonical Resources ARE:
- ✅ **Runtime security policy** - defines what's safe/unsafe
- ✅ **Living threat model** - anti-patterns are discovered vulnerabilities
- ✅ **User-facing documentation** - shown when code is blocked
- ✅ **LLM training data** - teaches the model what's safe
- ✅ **Audit evidence** - proves why code was blocked/allowed

### What Canonical Resources ARE NOT:
- ❌ Test fixtures
- ❌ Example code
- ❌ Documentation only
- ❌ Static reference material

### Resource Types:

#### Safe Patterns (`resources/patterns/`)
```yaml
# simple-transfer-v1.0.yaml
daml_template: |
  template SafeTransfer
    with
      currentOwner: Party
    where
      signatory currentOwner  # ← Gate 1 ALLOWS this
```

**Purpose**: Define certified-safe patterns that have passed all gates.

#### Anti-Patterns (`resources/anti-patterns/`)
```yaml
# missing-signatory-v1.0.yaml
problematic_code: |
  template UnsafeTransfer
    with
      owner: Party
    where
      # Missing signatory!  # ← Gate 1 BLOCKS this
```

**Purpose**: Define known vulnerabilities that gates MUST block. If a gate allows an anti-pattern, **that's a security vulnerability in the gate itself**.

### Policy Evolution:
1. Security researcher discovers new vulnerability
2. Add `anti-patterns/new-vulnerability-v1.0.yaml`
3. Tests verify gate now blocks it
4. **Gate immediately starts blocking in production**

---

## DAML Compiler Safety Advantages

### Built-in Safety Guarantees
- **Authorization Model**: DAML compiler enforces authorization by design
- **Type Safety**: All DAML code is type-safe by construction
- **Consistency**: Compiler ensures ledger consistency
- **Atomicity**: All operations are atomic by design

### Haskell Formal Verification
- **Dependent Types**: GHC extensions support dependent types
- **Liquid Haskell**: Formal verification tool for Haskell
- **QuickCheck**: Property-based testing with proof generation
- **Agda/Idris Integration**: Interface with proof assistants

---

## Safety Gates Architecture

### Gate 1: DAML Compiler Safety ✅ **COMPLETE**
**Runtime Enforcement**: Runs on every code generation request

**What it does:**
- Compiles pattern with DAML compiler
- Extracts authorization model (signatories, observers, controllers)
- Verifies type safety through compilation
- Blocks if compilation fails
- Generates safety certificate if passed

**Why it blocks:**
- Pattern doesn't compile
- Authorization errors (missing signatory, invalid controller)
- Type safety violations
- Syntax errors

**Production behavior:**
```python
result = await safety_checker.check_pattern_safety(generated_code)
if not result.passed:
    return {
        "blocked": True,
        "reason": result.blocked_reason,
        "anti_patterns": find_matching_anti_patterns(generated_code),
        "safe_alternatives": find_safe_alternatives(user_request)
    }
```

### Gate 2: Safety Annotations
**Runtime Enforcement**: Runs on every code generation request

**What it does:**
- Validates safety annotations in DAML templates
- Generates safety certificates from annotations
- Validates pattern combinations for composition safety
- Blocks if annotations missing/invalid

**Why it blocks:**
- Missing required safety annotations
- Invalid annotation syntax
- Unsafe pattern combinations detected
- Annotation contradicts compiler analysis

### Gate 3: Formal Verification
**Runtime Enforcement**: Runs on every code generation request

**What it does:**
- Formally verifies safety properties
- Validates composition safety for pattern combinations
- Verifies business context constraints
- Blocks if formal verification fails

**Why it blocks:**
- Safety properties cannot be proven
- Composition creates unsafe combinations
- Business context validation fails
- Formal verification timeout

### Gate 4: Production Readiness
**Runtime Enforcement**: Runs on every code generation request

**What it does:**
- Validates comprehensive test coverage
- Checks complete audit trail presence
- Verifies production testing results
- Blocks if production readiness criteria not met

**Why it blocks:**
- Insufficient test coverage
- Missing audit trail entries
- Production testing not completed
- Safety certificate expired

---

## Test Strategy: Gate Validation

**Tests validate that gates correctly enforce security policy. They are NOT traditional unit tests.**

### Test Categories:

#### 1. Security Policy Tests
```python
@pytest.mark.security
@pytest.mark.parametrize("anti_pattern_name", get_all_anti_pattern_names())
async def test_gate_blocks_anti_pattern(anti_pattern_name):
    """
    SECURITY REQUIREMENT: Gate must block this anti-pattern.
    Failure = production security vulnerability.
    """
    anti_pattern = load_anti_pattern(anti_pattern_name)
    result = await safety_checker.check_pattern_safety(
        anti_pattern.content["problematic_code"]
    )
    
    assert result.passed is False, \
        f"SECURITY VIOLATION: {anti_pattern_name} was NOT blocked!"
```

#### 2. Regression Tests
```python
@pytest.mark.regression
@pytest.mark.parametrize("pattern_name", get_all_safe_pattern_names())
async def test_gate_allows_safe_pattern(pattern_name):
    """
    REGRESSION: Gate must allow canonical safe patterns.
    Failure = gate too strict, blocks valid code.
    """
    pattern = load_pattern(pattern_name)
    result = await safety_checker.check_pattern_safety(
        pattern.content["daml_template"]
    )
    
    assert result.passed is True, \
        f"REGRESSION: Safe pattern '{pattern_name}' incorrectly blocked!"
```

#### 3. Compliance Tests
```python
@pytest.mark.compliance
async def test_all_gates_maintain_audit_trail():
    """
    COMPLIANCE: All gate decisions must be auditable.
    Failure = regulatory compliance violation.
    """
    result = await safety_checker.check_pattern_safety(code)
    
    assert result.audit_id is not None
    audit_entry = await audit_trail.get_entry(result.audit_id)
    assert audit_entry.code_hash == hash(code)
    assert audit_entry.decision in ["blocked", "allowed"]
```

**Key Point**: If a test fails, it means:
- A security vulnerability was introduced (anti-pattern allowed)
- A regression occurred (safe pattern blocked)
- Compliance requirement violated (no audit trail)

---

## Stories

### ✅ Story 3.1: DAML Compiler Safety Integration **[COMPLETE]**

**Status**: ✅ Production-ready  
**Completed**: 2025-10-28  
**Branch**: `feature/story-3-1-daml-compiler-safety`

**What was built:**
- ✅ DAML compiler subprocess integration
- ✅ Authorization model extraction (signatories, observers, controllers)
- ✅ Type safety verification through compilation
- ✅ Error parsing for DAML 2.9 & 2.10+ formats
- ✅ Safety certificate generation
- ✅ JSON-based audit trail system
- ✅ Complete test suite (71/72 tests passing)

**Production artifacts:**
```python
# Runtime enforcement (runs on every request)
from canton_mcp_server.daml import SafetyChecker

safety_checker = SafetyChecker()
result = await safety_checker.check_pattern_safety(generated_code)

if result.passed:
    # Code passed Gate 1 - proceed to Gate 2
    return {"code": generated_code, "certificate": result.safety_certificate}
else:
    # Code blocked - show user why
    return {
        "blocked": True,
        "reason": result.blocked_reason,
        "errors": result.compilation_result.errors
    }
```

**Files created:**
- `src/canton_mcp_server/daml/__init__.py` (48 lines)
- `src/canton_mcp_server/daml/types.py` (266 lines)
- `src/canton_mcp_server/daml/daml_compiler_integration.py` (461 lines)
- `src/canton_mcp_server/daml/authorization_validator.py` (230 lines)
- `src/canton_mcp_server/daml/type_safety_verifier.py` (160 lines)
- `src/canton_mcp_server/daml/safety_checker.py` (255 lines)
- `src/canton_mcp_server/daml/audit_trail.py` (220 lines)
- `tests/daml/*` (6 test files, 1,355 lines)

**Total**: 21 files, 3,473 lines

**Limitations (by design):**
- Gate 1 validates through DAML compilation only
- Does NOT yet check against canonical anti-patterns
- Does NOT yet suggest safe alternatives
- Story 3.1.5 will add policy-based blocking

---

### Story 3.1.1: Canonical Policy Integration for Gate 1

**Runtime Enforcement**: Enhances Gate 1 with canonical pattern matching

**Acceptance Criteria:**
- [ ] Gate 1 loads canonical anti-patterns from `resources/anti-patterns/`
- [ ] Gate 1 checks generated code against all anti-patterns
- [ ] Gate 1 blocks code matching any anti-pattern (even if it compiles)
- [ ] Gate 1 shows matching anti-pattern to user when blocking
- [ ] Gate 1 suggests safe alternatives from `resources/patterns/`
- [ ] Gate 1 maintains audit trail of policy-based blocks
- [ ] Tests validate Gate 1 blocks all canonical anti-patterns

**Why this is needed:**
Code can compile successfully but still match known anti-patterns:

```python
# This COMPILES but is unsafe (matches anti-pattern: excessive-authority)
template DangerousContract
  with
    admin: Party
    users: [Party]
  where
    signatory admin, users  # All parties are signatories - authority explosion!
    
    choice AdminOverride : ()
      controller admin
      do return ()  # Admin can do anything without user consent
```

**Production Behavior:**
```python
# Enhanced Gate 1 with policy checking
result = await safety_checker.check_pattern_safety(
    generated_code,
    check_anti_patterns=True  # NEW: Check canonical policy
)

if result.compilation_failed:
    block(reason="DAML compilation failed", errors=result.errors)

# NEW: Check against canonical anti-patterns
if result.matches_anti_pattern:
    anti_pattern = result.matched_anti_pattern
    return {
        "blocked": True,
        "reason": "Code matches known anti-pattern",
        "anti_pattern": {
            "name": anti_pattern.name,
            "description": anti_pattern.description,
            "problematic_code": anti_pattern.content["problematic_code"],
            "why_problematic": anti_pattern.content["why_problematic"]
        },
        "safe_alternatives": load_safe_patterns(user_context)
    }
```

**Tasks:**
- [ ] Integrate ResourceLoader into SafetyChecker
- [ ] Implement anti-pattern matching logic (code similarity)
- [ ] Add safe alternative suggestion engine
- [ ] Update SafetyCheckResult to include matched anti-patterns
- [ ] Add policy-based blocking to audit trail
- [ ] Write policy enforcement tests (parametrized with all anti-patterns)
- [ ] Document policy-based blocking behavior

**Files to Modify:**
- `src/canton_mcp_server/daml/safety_checker.py` - Add canonical policy checking
- `src/canton_mcp_server/daml/types.py` - Add anti-pattern match results

**Files to Create:**
- `src/canton_mcp_server/daml/pattern_matcher.py` - Code similarity matching
- `src/canton_mcp_server/daml/alternative_suggester.py` - Safe pattern suggestions
- `tests/daml/test_policy_enforcement.py` - Policy-based blocking tests

**Test Strategy:**
```python
@pytest.mark.security
@pytest.mark.parametrize("anti_pattern_name", get_all_anti_pattern_names())
async def test_gate1_blocks_canonical_anti_pattern(anti_pattern_name):
    """
    SECURITY: Gate 1 must block ALL canonical anti-patterns.
    This validates the policy enforcement layer.
    """
    anti_pattern = load_anti_pattern(anti_pattern_name)
    
    # Even if it compiles, it should be blocked
    result = await safety_checker.check_pattern_safety(
        anti_pattern.content["problematic_code"],
        check_anti_patterns=True
    )
    
    assert result.passed is False, \
        f"SECURITY VIOLATION: Anti-pattern '{anti_pattern_name}' was NOT blocked!"
    assert result.matched_anti_pattern is not None
    assert result.matched_anti_pattern.name == anti_pattern_name
```

**Estimate**: 2-3 days

---

### Story 3.2: Safety Annotation System

**Runtime Enforcement**: Runs on every code generation request (Gate 2)

**Acceptance Criteria:**
- [ ] Gate 2 runs in production on every code generation request
- [ ] Gate 2 blocks code missing required safety annotations
- [ ] Gate 2 validates safety annotations against canonical policy
- [ ] Gate 2 generates safety certificates for annotated patterns
- [ ] Gate 2 maintains complete audit trail of annotation decisions
- [ ] Gate 2 prevents unsafe pattern combinations
- [ ] Tests validate Gate 2 correctly enforces annotation policy

**Production Behavior:**
```python
# User generates code → LLM → Gate 1 (passed) → Gate 2
result = await annotation_gate.check_annotations(code, gate1_certificate)

if not result.passed:
    return {
        "blocked": True,
        "gate": "annotation",
        "reason": "Missing required safety annotations",
        "required_annotations": result.missing_annotations,
        "examples": load_annotated_patterns()
    }
```

**Tasks:**
- [ ] Design runtime annotation enforcement architecture
- [ ] Implement annotation parser (runs per-request)
- [ ] Create annotation validator (enforces canonical policy)
- [ ] Add safety certificate generation for annotated code
- [ ] Implement annotation audit trails
- [ ] Add pattern combination validation
- [ ] Write gate validation tests (not unit tests)
- [ ] Document annotation enforcement behavior

**Files to Create:**
- `src/canton_mcp_server/annotations/annotation_gate.py` - Runtime gate
- `src/canton_mcp_server/annotations/annotation_parser.py` - Per-request parser
- `src/canton_mcp_server/annotations/annotation_policy.py` - Policy enforcer
- `src/canton_mcp_server/annotations/certificate_generator.py` - Certificate generation

**Test Strategy:**
```python
@pytest.mark.security
def test_gate2_blocks_missing_annotations():
    """Gate 2 must block code missing required annotations"""
    code = generate_code_without_annotations()
    result = await annotation_gate.check(code)
    assert result.passed is False

@pytest.mark.regression  
def test_gate2_allows_properly_annotated_code():
    """Gate 2 must allow properly annotated safe patterns"""
    pattern = load_safe_pattern("simple-transfer")
    result = await annotation_gate.check(pattern.daml_template)
    assert result.passed is True
```

**Estimate**: 4-5 days

---

### Story 3.3: DAML-Safe Code Generation Engine

**Runtime Enforcement**: Wraps LLM code generation with gate enforcement

**Acceptance Criteria:**
- [ ] Generator runs all gates on every code generation request
- [ ] Generator blocks code that fails any gate
- [ ] Generator provides safe alternatives when blocking
- [ ] Generator maintains complete audit trail
- [ ] Generator shows users which gate blocked and why
- [ ] Tests validate generator correctly enforces multi-gate policy

**Production Flow:**
```python
# User request → Generator → Gates → Block/Allow
async def generate_safe_daml_code(user_request: str):
    # 1. LLM generation
    generated_code = await llm.generate(user_request)
    
    # 2. Gate 1: DAML Compiler Safety
    gate1_result = await safety_checker.check_pattern_safety(generated_code)
    if not gate1_result.passed:
        return block_with_alternatives(gate=1, result=gate1_result)
    
    # 3. Gate 2: Safety Annotations
    gate2_result = await annotation_gate.check(generated_code)
    if not gate2_result.passed:
        return block_with_alternatives(gate=2, result=gate2_result)
    
    # All gates passed!
    return {
        "code": generated_code,
        "certificates": [gate1_result.certificate, gate2_result.certificate],
        "audit_ids": [gate1_result.audit_id, gate2_result.audit_id]
    }
```

**Tasks:**
- [ ] Design multi-gate enforcement architecture
- [ ] Implement gate orchestration (runs all gates sequentially)
- [ ] Create safe alternative suggestion engine
- [ ] Add generation audit trails (tracks which gate blocked)
- [ ] Implement user-facing error messages per gate
- [ ] Write multi-gate validation tests
- [ ] Document generation security guarantees

**Files to Create:**
- `src/canton_mcp_server/generation/safe_generator.py` - Multi-gate orchestrator
- `src/canton_mcp_server/generation/gate_orchestrator.py` - Gate execution engine
- `src/canton_mcp_server/generation/alternative_suggester.py` - Safe alternatives
- `src/canton_mcp_server/generation/user_feedback.py` - Block messages

**Estimate**: 5-6 days

---

### Story 3.4: DAML Authorization Safety

**Runtime Enforcement**: Enhanced Gate 1 with deeper authorization analysis

**Acceptance Criteria:**
- [ ] Gate 1 validates signatory declarations in runtime
- [ ] Gate 1 verifies controller-authorization relationships per request
- [ ] Gate 1 handles multi-party scenarios through DAML compilation
- [ ] Gate 1 provides authorization-specific safety certificates
- [ ] Gate 1 blocks authorization patterns that don't compile safely
- [ ] Tests validate Gate 1 correctly enforces authorization policy

**Production Enhancement:**
```python
# Enhanced Gate 1 with authorization depth
result = await safety_checker.check_pattern_safety(
    code,
    authorization_strict=True  # Deep authorization analysis
)

if not result.authorization_model:
    return {
        "blocked": True,
        "reason": "Could not extract authorization model",
        "anti_pattern": "missing-signatory"
    }

if not result.authorization_valid:
    return {
        "blocked": True,
        "reason": result.authorization_errors,
        "correct_alternative": load_pattern("well-authorized-create")
    }
```

**Estimate**: 4-5 days

---

### Story 3.5: DAML Business Logic Safety

**Runtime Enforcement**: Enhanced Gate 1 with business logic validation

**Acceptance Criteria:**
- [ ] Gate 1 validates asset conservation through DAML compilation
- [ ] Gate 1 verifies state transitions using DAML's atomicity model
- [ ] Gate 1 ensures business logic safety via DAML's type system
- [ ] Gate 1 provides business-logic-specific safety certificates
- [ ] Tests validate Gate 1 correctly enforces business logic safety

**Estimate**: 3-4 days

---

### Story 3.6: DAML-Safe Tool Integration

**Runtime Enforcement**: All MCP tools use gate system

**Acceptance Criteria:**
- [ ] All tools run gates on generated code before showing to user
- [ ] All tools provide gate-specific error messages
- [ ] All tools maintain audit trails of gate decisions
- [ ] All tools show safe alternatives when blocking
- [ ] Tests validate tools correctly integrate with gates

**Files to Modify:**
- `src/canton_mcp_server/tools/validate_daml_business_logic.py` - Use gates
- `src/canton_mcp_server/tools/debug_authorization_failure.py` - Use Gate 1
- `src/canton_mcp_server/tools/suggest_authorization_pattern.py` - Use certified patterns

**Estimate**: 3-4 days

---

### Story 3.7: MCP Tool Integration

**Runtime Enforcement**: New tools for gate management

**Acceptance Criteria:**
- [ ] New tools expose gate enforcement to users
- [ ] New tools show gate status and certificates
- [ ] New tools maintain audit trails
- [ ] Tests validate new tools correctly use gates

**Files to Create:**
- `src/canton_mcp_server/tools/generate_safe_daml_code.py` - Multi-gate generation
- `src/canton_mcp_server/tools/get_safety_certificate.py` - Certificate retrieval
- `src/canton_mcp_server/tools/validate_against_gates.py` - Manual gate check

**Estimate**: 4-5 days

---

## Safety Principles

### 1. Runtime Security Enforcement
- **All gates run in production** on every code generation request
- **Block before user sees code** if any gate fails
- **Audit every decision** for compliance and analysis
- **Show users why** code was blocked with safe alternatives

### 2. Canonical Policy as Security Boundary
- **Anti-patterns define threats** - gates MUST block these
- **Safe patterns define certified code** - gates MUST allow these
- **Policy evolves with threats** - new anti-patterns → immediate enforcement
- **Tests validate enforcement** - not just implementation correctness

### 3. DAML-Safe by Construction
- **Leverage DAML compiler's proofs** - don't reinvent safety
- **Use DAML's authorization model** - it's mathematically proven
- **Rely on type safety guarantees** - compiler does the hard work
- **Block compilation failures** - if DAML won't compile it, we won't show it

### 4. Defense in Depth
- **Multiple gates** - fail at earliest possible gate
- **Independent validation** - each gate checks different properties
- **Composition safety** - gates validate pattern combinations
- **Complete audit trails** - every gate decision is logged

### 5. User-Facing Security
- **Clear error messages** - explain why code was blocked
- **Safe alternatives** - show certified patterns that work
- **Educational feedback** - teach users what's safe/unsafe
- **Transparent enforcement** - users understand the security model

---

## Production Architecture

```
┌─────────────────────────────────────────────────────────────┐
│                      User Request                            │
│              "Generate transfer pattern"                     │
└────────────────────────┬────────────────────────────────────┘
                         │
                         ▼
┌─────────────────────────────────────────────────────────────┐
│                   LLM Code Generation                        │
│          (Claude generates DAML template)                    │
└────────────────────────┬────────────────────────────────────┘
                         │
                         ▼
┌─────────────────────────────────────────────────────────────┐
│   Gate 1: DAML Compiler Safety (Production Enforcement)     │
│   ┌─────────────────────────────────────────────────────┐   │
│   │ • Compile with DAML compiler                        │   │
│   │ • Extract authorization model                       │   │
│   │ • Verify type safety                                │   │
│   │ • Check against anti-patterns                       │   │
│   └─────────────────────────────────────────────────────┘   │
└────────────┬────────────────────────────────┬───────────────┘
             │ PASS                           │ FAIL
             ▼                                ▼
    ┌────────────────┐              ┌─────────────────────┐
    │   Gate 2...    │              │  BLOCK & SHOW:      │
    └────────────────┘              │  • Why blocked      │
                                    │  • Which anti-pattern│
                                    │  • Safe alternatives│
                                    └─────────────────────┘
```

**Key Insight**: This is **production security infrastructure**, not development tooling.


Genrate Safe DAML Code Tools #4

Description

Core Philosophy: Runtime Security Enforcement

The Security Flow

Canonical Resources as Security Policy

What Canonical Resources ARE:

What Canonical Resources ARE NOT:

Resource Types:

Safe Patterns (resources/patterns/)

Anti-Patterns (resources/anti-patterns/)

Policy Evolution:

DAML Compiler Safety Advantages

Built-in Safety Guarantees

Haskell Formal Verification

Safety Gates Architecture

Gate 1: DAML Compiler Safety ✅ COMPLETE

Gate 2: Safety Annotations

Gate 3: Formal Verification

Gate 4: Production Readiness

Test Strategy: Gate Validation

Test Categories:

1. Security Policy Tests

2. Regression Tests

3. Compliance Tests

Stories

✅ Story 3.1: DAML Compiler Safety Integration [COMPLETE]

Story 3.1.1: Canonical Policy Integration for Gate 1

Story 3.2: Safety Annotation System

Story 3.3: DAML-Safe Code Generation Engine

Story 3.4: DAML Authorization Safety

Story 3.5: DAML Business Logic Safety

Story 3.6: DAML-Safe Tool Integration

Story 3.7: MCP Tool Integration

Safety Principles

1. Runtime Security Enforcement

2. Canonical Policy as Security Boundary

3. DAML-Safe by Construction

4. Defense in Depth

5. User-Facing Security

Production Architecture

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Safe Patterns (`resources/patterns/`)

Anti-Patterns (`resources/anti-patterns/`)