# Reachability Slice Schema

_Last updated: 2025-12-22. Owner: Scanner Guild._

This document defines the **Reachability Slice** schema - a minimal, attestable proof unit that answers whether a vulnerable symbol is reachable from application entrypoints.

---

## 1. Overview

A **slice** is a focused subgraph extracted from a full reachability graph, containing only the nodes and edges relevant to answering a specific reachability query (for example, "Is CVE-2024-1234's vulnerable function reachable?").

### Key Properties

| Property | Description |
|----------|-------------|
| **Minimal** | Contains only nodes/edges on paths between entrypoints and targets |
| **Attestable** | DSSE-signed with a dedicated slice predicate |
| **Reproducible** | Same inputs -> same bytes (deterministic) |
| **Content-addressed** | Retrieved by BLAKE3 digest |

---

## 2. Predicate Type & Schema

- Predicate type: `stellaops.dev/predicates/reachability-slice@v1`
- JSON schema: `https://stellaops.dev/schemas/stellaops-slice.v1.schema.json`
- DSSE payload type: `application/vnd.stellaops.slice.v1+json`

---

## 3. Schema Structure

### 3.1 ReachabilitySlice

```csharp
public sealed record ReachabilitySlice
{
    [JsonPropertyName("_type")]
    public string Type { get; init; } = "stellaops.dev/predicates/reachability-slice@v1";

    [JsonPropertyName("inputs")]
    public required SliceInputs Inputs { get; init; }

    [JsonPropertyName("query")]
    public required SliceQuery Query { get; init; }

    [JsonPropertyName("subgraph")]
    public required SliceSubgraph Subgraph { get; init; }

    [JsonPropertyName("verdict")]
    public required SliceVerdict Verdict { get; init; }

    [JsonPropertyName("manifest")]
    public required ScanManifest Manifest { get; init; }
}
```

### 3.2 SliceInputs

```csharp
public sealed record SliceInputs
{
    public required string GraphDigest { get; init; }
    public ImmutableArray<string> BinaryDigests { get; init; }
    public string? SbomDigest { get; init; }
    public ImmutableArray<string> LayerDigests { get; init; }
}
```

### 3.3 SliceQuery

```csharp
public sealed record SliceQuery
{
    public string? CveId { get; init; }
    public ImmutableArray<string> TargetSymbols { get; init; }
    public ImmutableArray<string> Entrypoints { get; init; }
    public string? PolicyHash { get; init; }
}
```

### 3.4 SliceSubgraph, Nodes, Edges

```csharp
public sealed record SliceSubgraph
{
    public ImmutableArray<SliceNode> Nodes { get; init; }
    public ImmutableArray<SliceEdge> Edges { get; init; }
}

public sealed record SliceNode
{
    public required string Id { get; init; }
    public required string Symbol { get; init; }
    public required SliceNodeKind Kind { get; init; } // entrypoint | intermediate | target | unknown
    public string? File { get; init; }
    public int? Line { get; init; }
    public string? Purl { get; init; }
    public IReadOnlyDictionary<string, string>? Attributes { get; init; }
}

public sealed record SliceEdge
{
    public required string From { get; init; }
    public required string To { get; init; }
    public SliceEdgeKind Kind { get; init; } // direct | plt | iat | dynamic | unknown
    public double Confidence { get; init; }
    public string? Evidence { get; init; }
    public SliceGateInfo? Gate { get; init; }
    public ObservedEdgeMetadata? Observed { get; init; }
}
```

### 3.5 SliceVerdict

```csharp
public sealed record SliceVerdict
{
    public required SliceVerdictStatus Status { get; init; }
    public required double Confidence { get; init; }
    public ImmutableArray<string> Reasons { get; init; }
    public ImmutableArray<string> PathWitnesses { get; init; }
    public int UnknownCount { get; init; }
    public ImmutableArray<GatedPath> GatedPaths { get; init; }
}
```

`SliceVerdictStatus` values (snake_case):
- `reachable`
- `unreachable`
- `unknown`
- `gated`
- `observed_reachable`

### 3.6 ScanManifest

`ScanManifest` is imported from `StellaOps.Scanner.Core` and includes required fields for reproducibility:

- `scanId`
- `createdAtUtc`
- `artifactDigest`
- `scannerVersion`
- `workerVersion`
- `concelierSnapshotHash`
- `excititorSnapshotHash`
- `latticePolicyHash`
- `deterministic`
- `seed` (base64-encoded 32-byte seed)
- `knobs` (string map)

`artifactPurl` is optional.

---

## 4. Verdict Computation Rules

```
reachable   := path_exists AND min(path_confidence) > 0.7 AND unknown_edges == 0
unreachable := NOT path_exists AND unknown_edges == 0
unknown     := otherwise
```

`gated` and `observed_reachable` are reserved for feature-gate and runtime-observed paths (see Sprint 3830 and 3840).

---

## 5. Example Slice

```json
{
  "_type": "stellaops.dev/predicates/reachability-slice@v1",
  "inputs": {
    "graphDigest": "blake3:a1b2c3d4e5f6789012345678901234567890123456789012345678901234abcd",
    "binaryDigests": ["sha256:deadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"],
    "sbomDigest": "sha256:cafebabecafebabecafebabecafebabecafebabecafebabecafebabecafebabe"
  },
  "query": {
    "cveId": "CVE-2024-1234",
    "targetSymbols": ["openssl:EVP_PKEY_decrypt"],
    "entrypoints": ["main", "http_handler"]
  },
  "subgraph": {
    "nodes": [
      {"id": "node:1", "symbol": "main", "kind": "entrypoint", "file": "/app/main.c", "line": 42},
      {"id": "node:2", "symbol": "process_request", "kind": "intermediate", "file": "/app/handler.c", "line": 100},
      {"id": "node:3", "symbol": "decrypt_data", "kind": "intermediate", "file": "/app/crypto.c", "line": 55},
      {"id": "node:4", "symbol": "EVP_PKEY_decrypt", "kind": "target", "purl": "pkg:generic/openssl@3.0.0"}
    ],
    "edges": [
      {"from": "node:1", "to": "node:2", "kind": "direct", "confidence": 1.0},
      {"from": "node:2", "to": "node:3", "kind": "direct", "confidence": 0.95},
      {"from": "node:3", "to": "node:4", "kind": "plt", "confidence": 0.9}
    ]
  },
  "verdict": {
    "status": "reachable",
    "confidence": 0.9,
    "reasons": ["path_exists_high_confidence"],
    "pathWitnesses": ["main -> process_request -> decrypt_data -> EVP_PKEY_decrypt"],
    "unknownCount": 0
  },
  "manifest": {
    "scanId": "scan-1234",
    "createdAtUtc": "2025-12-22T10:00:00Z",
    "artifactDigest": "sha256:00112233445566778899aabbccddeeff00112233445566778899aabbccddeeff",
    "artifactPurl": "pkg:generic/app@1.0.0",
    "scannerVersion": "scanner.native:1.2.0",
    "workerVersion": "scanner.worker:1.2.0",
    "concelierSnapshotHash": "sha256:1111222233334444555566667777888899990000aaaabbbbccccddddeeeeffff",
    "excititorSnapshotHash": "sha256:2222333344445555666677778888999900001111aaaabbbbccccddddeeeeffff",
    "latticePolicyHash": "sha256:3333444455556666777788889999000011112222aaaabbbbccccddddeeeeffff",
    "deterministic": true,
    "seed": "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA=",
    "knobs": { "maxDepth": "20" }
  }
}
```

---

## 6. Determinism Requirements

For reproducible slices:

1. **Node ordering**: Sort by `id` (ordinal).
2. **Edge ordering**: Sort by `from`, then `to`, then `kind`.
3. **Strings**: Trim and de-duplicate lists (`targetSymbols`, `entrypoints`, `reasons`).
4. **Timestamps**: Use UTC ISO-8601 with `Z` suffix.
5. **JSON serialization**: Canonical JSON (sorted keys, no whitespace).

---

## 7. Related Documentation

- [Binary Reachability Schema](./binary-reachability-schema.md)
- [RichGraph Contract](../contracts/richgraph-v1.md)
- [Function-Level Evidence](./function-level-evidence.md)
- [Replay Verification](./replay-verification.md)

---

_Created: 2025-12-22. See Sprint 3810 for implementation details._