diff --git a/docs/whitepaper-v2.md b/docs/whitepaper-v2.md index b792aeb..331f405 100644 --- a/docs/whitepaper-v2.md +++ b/docs/whitepaper-v2.md @@ -923,9 +923,149 @@ The Raft example is particularly significant because it bridges SpeckDL's academ The natural progression — Two-Phase Commit (learning), Paxos (theoretical bedrock), Raft (production consensus), then TigerBeetle (production financial ledger) — forms a complete curriculum for understanding and verifying distributed systems specifications. -## 6. Compliance and Supply Chain +## 6. Compliance and Supply Chain Security -*[Section 6: NIST SA-11 alignment, SBOM automation, regulatory use cases]* +Section 4 described Speckl's provenance-by-construction model. This section examines how that model maps to real-world compliance frameworks and regulatory requirements — and why automated evidence generation matters now more than ever. + +### 6.1 The Compliance Landscape in 2026 + +Software supply chain security has moved from best practice to regulatory requirement. The landscape includes: + +**United States:** +- **Executive Order 14028** (2021): Requires SBOMs for all software procured by the federal government. NIST SSDF (SP 800-218) defines secure development practices including SA-11 (Developer Testing and Evaluation). +- **CISA Secure Software Development Attestation** (2024-2026): Software vendors selling to the US government must attest to following NIST SSDF practices. Form requires artifact evidence. +- **FDA Premarket Cybersecurity Guidance** (2025): Medical device software requires SBOMs and evidence of secure development lifecycle. +- **FedRAMP Authorization**: Cloud service providers must demonstrate SA-11 compliance and provide supply chain documentation. + +**European Union:** +- **Cyber Resilience Act** (2027 enforcement begins): Requires CE marking for products with digital elements. SBOMs mandated. Vulnerability disclosure processes required. Non-compliance penalties: up to €15M or 2.5% of global turnover. +- **NIS2 Directive** (2024): Expands critical infrastructure security requirements including supply chain risk management. +- **DORA** (Digital Operational Resilience Act, 2025): Financial institutions must test and document ICT systems including third-party software. + +**International:** +- **ISO/IEC 27001:2022** Annex A.8.25: Secure development lifecycle controls. +- **SLSA** (Supply-chain Levels for Software Artifacts): Google-originated framework, now OpenSSF. Level 3 requires non-falsifiable provenance. + +### 6.2 NIST SA-11: Human-in-the-Loop for Automated Outputs + +NIST SP 800-53 SA-11 is the control most directly addressed by Speckl. SA-11 requires organizations to perform "developer testing and evaluation" — and critically, the SA-11 enhancement controls address automated code generation: + +**SA-11(2) — Static and Dynamic Analysis**: Requires analysis of "developer-generated, machine-generated, and system-generated code" using static analysis tools. Speckl's compiler generates code deterministically from a spec — the spec serves as the static analysis artifact because it declares exactly what the code should do. + +**SA-11(4) — Manual Code Reviews**: Requires manual inspection of code for defects and security issues. Speckl enables this by providing a human-readable, concise specification alongside every generated artifact. Reviewers inspect the spec (a few hundred lines) and verify that the generated code (potentially thousands of lines) faithfully implements it. + +**SA-11(6) — Attack Surface Reviews**: Requires analysis of attack surfaces introduced by the system. Speckl's state machine model makes attack surfaces explicit: every action, every state transition, and every guard condition is declared in the spec. Security reviewers can identify missing guards or overly permissive state transitions without reading generated code. + +**SA-11(7) — Verify Scope of Testing/Evalution**: Requires confirmation that testing covers all components. Speckl's compilation model guarantees that every action in the spec produces corresponding code. There is no code without a spec — completeness is structural, not aspirational. + +### 6.3 The Evidence Problem + +Organizations face a structural challenge with compliance: **evidence production is manual, expensive, and disconnected from development.** + +A typical compliance response looks like this: +1. Security team sends a questionnaire to engineering +2. Engineering team members respond from memory or grep through repositories +3. Responses are compiled into a document, reviewed, and submitted +4. The process repeats quarterly or annually +5. Evidence is stale the moment it's produced because the code has already changed + +This is fundamentally a **documentation-as-afterthought** model. Speckl inverts it to **documentation-as-compilation-target.** + +When a Speckl project compiles, it produces: +- **The spec itself**: human-readable documentation of design intent +- **PROV-O audit trail**: machine-readable chain of custody showing what was compiled, when, by whom +- **CycloneDX SBOM**: standardized bill of materials listing all declared types and their relationships +- **SPDX metadata**: formal records of copyright, license, supplier, and originator + +These artifacts are not manually produced. They are compiler outputs — which means they are always up to date because they are regenerated on every build. A compliance auditor can verify that the spec `v0.4` produced the SBOM `sha256:abc...` and that both match the deployed artifact. + +### 6.4 Compliance Automation with Speckl + +Here is a concrete compliance workflow: + +**Step 1: Spec is the source of truth.** A SpeckDL specification describes the system's state, actions, guards, and invariants. This spec lives in version control alongside the generated code. + +**Step 2: Compilation produces evidence.** Every build generates: +- `{spec}.prov-o.ttl` — W3C PROV-O provenance graph +- `{spec}.cyclonedx.json` — OWASP CycloneDX SBOM v1.4 +- `{spec}.spdx.json` — SPDX 2.3 license and supplier metadata +- `{spec}.ts` — Generated TypeScript (human-reviewable) +- `{spec}.wat` — Generated WAT (verifiable via wabt) + +**Step 3: Evidence is self-consistent.** All three provenance artifacts derive from the same parse tree. They can't disagree with each other — consistency is guaranteed by construction. An auditor can trace any SBOM entry back to a specific line in the spec. + +**Step 4: Evidence is verifiable.** The PROV-O graph records a chain of derivation: `source.speck → parse → AST → artifact`. The WASM module can be validated through wabt's `wat2wasm`. The TypeScript can be checked with `tsc --noEmit`. Each artifact has an independent verification path. + +**Step 5: Evidence is cumulative.** Each commit in version control carries its own set of generated artifacts. An auditor can trace how the system evolved — and verify that at no point was a spec change made without corresponding artifact regeneration. + +### 6.5 The Judgement Transport Model + +The term "judgement transport" captures Speckl's compliance philosophy: + +> Speckl does not replace human judgement with automation. It transports human judgement from the specification to every artifact that depends on it. + +In traditional development: +- A human makes a design decision +- A human writes code implementing that decision +- A human reviews the code to verify it matches the decision +- A human writes documentation describing the decision +- At audit time, a different human tries to reconstruct the original decision from the code, commits, and docs + +In Speckl development: +- A human makes a design decision and writes it as a SpeckDL spec +- The compiler generates code that implements exactly that decision +- The compiler generates documentation, SBOMs, and provenance from the same decision +- At audit time, the auditor reads the spec and verifies that the generated artifacts derive from it + +The judgement is made once. The evidence is generated automatically. The audit chain is verifiable. This is judgement transport. + +### 6.6 Real-World Use Cases + +**Medical Device Software (FDA)** +A startup building an insulin pump controller needs to demonstrate to FDA reviewers that the software was developed following a secure development lifecycle, that all third-party components are documented, and that safety-critical logic is verifiable. Writing the logic as a SpeckDL spec means the spec itself is evidence of design intent, the SBOM documents all dependencies, and the provenance trail shows every change. + +**Government Contractor (CISA Attestation)** +A contractor building a case management system for a federal agency must attest to NIST SSDF compliance. Instead of a one-time document produced for the RFP response, the contractor maintains the system spec in SpeckDL. The attestation is supported by a continuously regenerated artifact trail showing SA-11(2),(4),(6),(7) control coverage. + +**Financial Services (DORA)** +A fintech company deploying to EU customers must demonstrate ICT risk management including third-party software transparency. The Speckl-generated CycloneDX SBOM provides a machine-readable inventory. The SPDX records document licensing obligations. The PROV-O trail demonstrates that the deployed software derives from a reviewed specification. + +**Open Source Project (SLSA Level 3+)** +An open source project targeting SLSA Level 3 compliance needs non-falsifiable provenance — evidence that the built artifact came from the claimed source. Speckl's PROV-O generation provides this: the provenance graph records the exact source file, parse tree, and generation parameters that produced each artifact. + +### 6.7 What Speckl Does Not Do + +It is equally important to be clear about boundaries. Speckl is not: + +- **A static analysis tool.** Speckl generates TypeScript — you run your existing tools (ESLint, Sonar, Snyk) on the output. +- **A vulnerability scanner.** Speckl's SBOM helps you know what you have, but it doesn't check CVEs. Integrate with Grype, Trivy, or Dependabot. +- **A model checker.** Speckl does not exhaustively verify state space properties like TLC does for TLA+. Invariant checking is runtime, not compile-time. +- **A formal verification system.** Speckl guarantees that generated artifacts match the spec. It does not guarantee that the spec is correct. That remains a human responsibility — and always should be. +- **A replacement for security review.** Speckl makes review more efficient by providing a concise specification. It does not eliminate the need for human security expertise. + +Speckl's compliance role is specific and focused: **it automates the production and maintenance of compliance evidence, and it provides a human-reviewable specification that anchors all generated artifacts.** + +### 6.8 The Cost Equation + +Compliance-as-afterthought has a measurable cost. Industry data: + +- **SOC 2 Type II audit:** $30,000-$100,000 for initial certification, $20,000-$50,000 annually +- **FedRAMP authorization:** $500,000-$2,000,000 for initial, $100,000-$500,000 annually +- **Manual SBOM generation:** 2-5 engineering days per artifact per release cycle +- **Compliance questionnaire response time:** 40-80 engineering hours per audit cycle + +Speckl shifts these costs from ongoing manual effort to upfront specification investment: + +| Compliance Activity | Without Speckl | With Speckl | +|---------------------|---------------|-------------| +| SBOM generation | Manual per release | Automatic on every build | +| Evidence collection | 40-80h per audit | 0h — artifacts always current | +| Design documentation | Separate from code, drifts | Spec is documentation, always matches | +| Dependency inventory | Runtime discovery | Declared in spec, emitted as SBOM | +| Provable chain of custody | Not typically provided | PROV-O graph generated per build | +| Auditor Q&A | Engineering time per question | Auditor reads spec + generated artifacts | + +The upfront cost: spec authoring. The recurring savings: all evidence production. For organizations undergoing multiple compliance assessments annually, the ROI is measured in engineering weeks per year. ## 7. Related Work @@ -937,4 +1077,4 @@ The natural progression — Two-Phase Commit (learning), Paxos (theoretical bedr --- -*Whitepaper v2 draft. Sections 1-3 complete; 4-8 forthcoming.* +*Whitepaper v2 draft. Sections 1-6 complete; 7-8 forthcoming.*