diff --git a/speckdl/SPEC.v2-dp-primitives.md b/speckdl/SPEC.v2-dp-primitives.md index 8f417b1..f3f009f 100644 --- a/speckdl/SPEC.v2-dp-primitives.md +++ b/speckdl/SPEC.v2-dp-primitives.md @@ -1,7 +1,7 @@ # SpeckDL Language Specification v0.2-DP > The specification-first language for auditable software. -> **This version adds Dark Provenance primitives (`provenance`, `review`, `derives`, `satisfies`, `author`, `source`), SpeckBOM (`bom` + import pinning), and CycloneDX v1.6 as the SpeckBOM output format.** +> **This version adds Dark Provenance primitives (`provenance`, `review`, `derives`, `satisfies`, `author`, `source`), SpeckBOM (`bom` + import pinning), and dual-output BOM format (CycloneDX v1.6 + SPDX 3.0.1).** > Part of the [Speckl](https://os.scoble.me/forgejo/sscoble/speckl) project. MIT License. --- @@ -431,26 +431,39 @@ The provenance graph is serialized as JSON-LD and stored alongside the compiled } ``` -### 4.5 Compilation Manifest (SpeckBOM Output — CycloneDX) +### 4.5 Compilation Manifest (SpeckBOM Output) -At compile time, the compiler produces a **SpeckBOM** — a valid [CycloneDX](https://cyclonedx.org/) v1.6 document with `bomType: specBOM` and `speckl:` property extensions. This extends an existing OWASP/ECMA-424 standard rather than defining a bespoke format, ensuring compatibility with the full CycloneDX tooling ecosystem (Dependency-Track, OWASP integration, etc.). +At compile time, the compiler produces a **SpeckBOM** — a specification-level bill of materials. The Speckl compiler supports **two output formats**: -#### Why CycloneDX - -CycloneDX is the natural base for SpeckBOM because: - -| Concern | CycloneDX Feature | SpeckBOM Mapping | +| Format | Standard | Best for | |---|---|---| -| Component inventory | `components[]` | Imported Specks as components | -| Dependency graph | `dependencies[]` | Import/derives/satisfies edges | -| Toolchain provenance | `metadata.tools[]` | Compiler, solver, runtime | -| Content integrity | `hashes[]` on components | Source and artifact hashes | -| Attestations | CycloneDX Attestations (CDXA) | Review status (`manual`/`auto`/`hybrid`) | -| Citations | `annotations[]` | Author, source, provenance metadata | -| Cross-BOM linking | BOM-Link | Chaining SpeckBOMs across spec imports | -| Extensibility | `properties[]` with namespace | `speckl:` properties for domain-specific fields | +| **CycloneDX v1.6 JSON** | OWASP / ECMA-424 | Security tooling (Dependency-Track, OWASP ecosystem), BOM-type extensibility | +| **SPDX 3.0.1 JSON-LD** | ISO 5962:2023 | Regulated industries (DO-178C, IEC 62304), audit compliance, semantic web tooling | -Neither CycloneDX nor SPDX currently defines a **specification-level BOM type**. SpeckBOM (`specBOM`) fills this gap: it captures *what specification a system satisfies*, *what verification evidence exists*, and *what intent drove each decision* — concerns that software-level BOMs don't address. +Both formats capture the same information. The choice depends on downstream tooling and regulatory context. Neither CycloneDX nor SPDX currently defines a **specification-level BOM type** — SpeckBOM (`specBOM`) fills this gap. + +#### Why Both Standards + +| Concern | CycloneDX v1.6 | SPDX 3.0.1 | +|---|---|---| +| Component inventory | `components[]` | `Package` + `SoftwareArtifact` | +| Dependency graph | `dependencies[]` | `Relationship` (dependsOn, prerequisite) | +| Toolchain provenance | `metadata.tools[]` | `Build` profile (from SLSA integration) | +| Content integrity | `hashes[]` on components | `hash` + `verificationCode` on Packages | +| Attestations | CycloneDX Attestations (CDXA) | `Element` + `Relationship` (attest) | +| Citations/annotations | `annotations[]` | `Annotation` class | +| Cross-BOM linking | BOM-Link | `ExternalDocumentRef` + `SpdxDocument` | +| Extensibility | `properties[]` with namespace | `Extension` + `Property` | +| Licensing | `licenses[]` (SPDX expressions) | Native (SPDX is the license standard) | +| Normative status | OWASP community standard, ECMA-424 | ISO 5962:2023 (international standard) | +| BOM type taxonomy | SBOM, HBOM, MBOM, OBOM, AI-BOM, CBOM | Software-focused, profiles for AI, security, build | +| Provenance model | Properties + annotations | Native PROV-O alignment (JSON-LD) | + +CycloneDX offers a richer BOM type taxonomy (making `specBOM` a natural addition) and a simpler extension model. SPDX offers native JSON-LD, ISO standard status, and tighter PROV-O alignment — critical for regulated environments where auditors expect ISO-normative formats. + +#### CycloneDX Output Format + +The compiler emits a valid CycloneDX v1.6 JSON document with `bomType: specBOM` and `speckl:` property extensions: #### Output Format @@ -551,12 +564,12 @@ The manifest includes: - **Verification results** — SAT/UNSAT for each verify clause - **Reproducibility flag** — `true` only if all toolchain versions match declarations and all imports hash-verify -This manifest is the **audit-ready output**. An auditor can: +An auditor can: 1. Verify the spec hash matches the source file 2. Verify all dependency hashes match their imports 3. Verify toolchain versions match the declared ones 4. Re-run compilation and verify artifact hashes match -5. Load the SpeckBOM into any CycloneDX-compatible tool (Dependency-Track, OWASP ecosystem) for dependency analysis, vulnerability tracking, and compliance reporting +5. Load the SpeckBOM into any CycloneDX-compatible tool (Dependency-Track, OWASP ecosystem) #### CycloneDX Field Mapping @@ -576,15 +589,117 @@ This manifest is the **audit-ready output**. An auditor can: | Verification results (SAT/UNSAT) | `metadata.component.properties[]` | `speckl:verificationResult` | | Reproducibility status | `metadata.component.properties[]` | `speckl:reproducible` | -#### Path to Standardization +#### SPDX 3.0.1 Output Format -SpeckBOM currently extends CycloneDX with a `specBOM` bomType and `speckl:` property namespace. The path to formal adoption: +The compiler also emits a valid SPDX 3.0.1 JSON-LD document using the SPDX `Sbom` class with `speckl:` extension properties. This format aligns with ISO 5962:2023 and is preferred for regulated environments: -1. **Now**: Speckl emits valid CycloneDX v1.6 with `speckl:` extensions — works with all existing tooling -2. **Near-term**: Submit a community proposal to CycloneDX for `specBOM` as a recognized BOM type (alongside SBOM, HBOM, MBOM, OBOM, AI-BOM, CBOM) -3. **Long-term**: If adopted, Speckl becomes the reference implementation for specification-level BOMs in an OWASP standard +```json +{ + "@context": [ + "https://spdx.github.io/spdx-spec/v3.0.1/context.jsonld", + { + "speckl": "https://os.scoble.me/speckl/ns#" + } + ], + "@id": "urn:uuid:f81d4fae-7dec-11d0-a765-00a0c91e6bf6", + "@type": ["spdx:Sbom", "speckl:SpecBOM"], + "spdx:element": [ + { + "@id": "speckl:DrugDosageCalculator-1.0.0", + "@type": "spdx:Software", + "spdx:name": "DrugDosageCalculator", + "spdx:softwareVersion": "1.0.0", + "spdx:packageVersion": "1.0.0", + "spdx:downloadLocation": "pkg:speckl/DrugDosageCalculator@1.0.0", + "spdx:hash": { "@type": "spdx:Hash", "spdx:algorithm": "sha256", "spdx:hashValue": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" }, + "spdx:licenseConcluded": "MIT", + "speckl:verificationResult": "SAT", + "speckl:reproducible": true, + "spdx:builtBy": [ + { "@type": "spdx:Build", "spdx:buildType": "speckl:compile", "speckl:toolVersion": "0.2.0" }, + { "@type": "spdx:Build", "spdx:buildType": "speckl:solve", "speckl:toolVersion": "4.12.5" }, + { "@type": "spdx:Build", "spdx:buildType": "speckl:runtime", "speckl:toolVersion": "1.0.0" } + ] + }, + { + "@id": "speckl:RetryHandler-1.2.0", + "@type": "spdx:Software", + "spdx:name": "RetryHandler", + "spdx:softwareVersion": "1.2.0", + "spdx:downloadLocation": "pkg:speckl/RetryHandler@1.2.0", + "spdx:hash": { "@type": "spdx:Hash", "spdx:algorithm": "sha256", "spdx:hashValue": "a1b2c3..." }, + "speckl:integrity": "verified", + "speckl:derivesFrom": "speckl:FaultHandler-2.0.0", + "speckl:satisfies": "REQ-ASYNC-001" + } + ], + "spdx:relationship": [ + { + "@type": "spdx:Relationship", + "spdx:from": "speckl:DrugDosageCalculator-1.0.0", + "spdx:relationshipType": "spdx:dependsOn", + "spdx:to": ["speckl:RetryHandler-1.2.0"] + }, + { + "@type": "spdx:Relationship", + "spdx:from": "speckl:DrugDosageCalculator-1.0.0", + "spdx:relationshipType": "speckl:satisfies", + "spdx:to": ["req:FDA-21-CFR-820-30"] + }, + { + "@type": "spdx:Relationship", + "spdx:from": "speckl:DrugDosageCalculator-1.0.0", + "spdx:relationshipType": "spdx:wasAttributedTo", + "spdx:to": ["agent:sarah-chen"] + } + ], + "spdx:annotation": [ + { + "@type": "spdx:Annotation", + "spdx:annotationType": "REVIEW", + "spdx:statement": "Manual review required before deployment", + "speckl:reviewType": "manual", + "speckl:reviewStatus": "pending" + } + ] +} +``` -This is the same path SPDX used for AI-BOM — extend the standard rather than fork it. +#### SPDX Field Mapping + +| SpeckDL Primitive | SPDX 3.0.1 Location | Field | +|---|---|---| +| `bom { compiler }`, `bom { solver }`, `bom { runtime }` | `spdx:Build` (in `builtBy`) | Tool name + version | +| `bom { license }` | `spdx:licenseConcluded` | SPDX expression (native) | +| `bom { hash }` | `spdx:hash` | SHA-256 | +| `import "X" hash H version V` | `spdx:Software` element | Package with version + hash | +| `derives from X` | `spdx:Relationship` (derivesFrom) | Standard SPDX relationship | +| `satisfies X clause Y` | `speckl:satisfies` property | Extension on element | +| `author: Name ` | `spdx:Relationship` (wasAttributedTo) | Agent element | +| `source: kind ref X` | `spdx:Relationship` (wasInformedBy) | Activity element | +| `provenance { regulation: X }` | `spdx:Relationship` + element | Regulation node | +| `review: manual` | `spdx:Annotation` (REVIEW) | Standard annotation | +| Compilation artifacts (Z3, DST, WASM) | `spdx:SoftwareArtifact` elements | With hashes | +| Verification results (SAT/UNSAT) | `speckl:verificationResult` | Extension property | +| Reproducibility status | `speckl:reproducible` | Extension property | + +#### Compiler Output + +The `speckl-compile` tool produces both formats by default: + +``` +$ speckl compile drug-dosage.speck --output-dir out/ + + out/ + ├── drug-dosage.prov.jsonld # Provenance graph (PROV-O / JSON-LD) + ├── drug-dosage.specbom.cdx.json # SpeckBOM (CycloneDX v1.6) + ├── drug-dosage.specbom.spdx.json # SpeckBOM (SPDX 3.0.1 JSON-LD) + ├── drug-dosage.z3.smt2 # Z3 assertions + ├── drug-dosage.dst.json # Decision Structure Tree + └── drug-dosage.wasm # WASM module +``` + +Use `--bom-format cdx|spdx|both` to select output format. Default is `both`. --- @@ -933,7 +1048,7 @@ The provenance graph (§4.4) is serialized as JSON-LD using PROV-O vocabulary. T ### B.2 SpeckBOM — CycloneDX v1.6 -The compilation manifest (§4.5) is serialized as CycloneDX v1.6 JSON with `bomType: specBOM` and `speckl:` property extensions. This is the **composition BOM** layer — what a spec depends on, what tools built it, and what it produced. +The compilation manifest (§4.5) supports CycloneDX v1.6 JSON with `bomType: specBOM` and `speckl:` property extensions. Preferred for security tooling and OWASP ecosystem integration. | SpeckDL Primitive | CycloneDX Location | Field | |---|---|---| @@ -953,21 +1068,44 @@ The compilation manifest (§4.5) is serialized as CycloneDX v1.6 JSON with `bomT | Verification results (SAT/UNSAT) | `metadata.component.properties[]` | `speckl:verificationResult` | | Reproducibility status | `metadata.component.properties[]` | `speckl:reproducible` | -### B.3 Two-Layer Architecture +### B.3 SpeckBOM — SPDX 3.0.1 -Speckl produces **two complementary outputs**: +The compilation manifest (§4.5) also supports SPDX 3.0.1 JSON-LD using the `Sbom` class with `speckl:` extension properties. Preferred for regulated environments (DO-178C, IEC 62304) where ISO 5962:2023 compliance is required. + +| SpeckDL Primitive | SPDX Location | Field | +|---|---|---| +| `bom { compiler }`, `bom { solver }`, `bom { runtime }` | `spdx:Build` (in `builtBy`) | Tool name + version | +| `bom { license }` | `spdx:licenseConcluded` | SPDX expression (native) | +| `bom { hash }` | `spdx:hash` | SHA-256 | +| `import "X" hash H version V` | `spdx:Software` element | Package with version + hash | +| `derives from X` | `spdx:Relationship` (derivesFrom) | Standard SPDX relationship | +| `satisfies X clause Y` | `speckl:satisfies` property | Extension on element | +| `author: Name ` | `spdx:Relationship` (wasAttributedTo) | Agent element | +| `source: kind ref X` | `spdx:Relationship` (wasInformedBy) | Activity element | +| `provenance { regulation: X }` | `spdx:Relationship` + element | Regulation node | +| `review: manual` | `spdx:Annotation` (REVIEW) | Standard annotation | +| `review: auto` | No additional annotation | N/A | +| `review: hybrid` | `spdx:Annotation` (REVIEW) | `speckl:reviewType: hybrid` | +| Compilation artifacts (Z3, DST, WASM) | `spdx:SoftwareArtifact` elements | With hashes | +| Verification results (SAT/UNSAT) | `speckl:verificationResult` | Extension property | +| Reproducibility status | `speckl:reproducible` | Extension property | + +### B.4 Two-Layer Architecture + +Speckl produces **three complementary outputs**: | Layer | Format | Concern | Standard | |---|---|---|---| | **Intent provenance** | JSON-LD / PROV-O | Who, why, what drove this specification | W3C PROV-O | -| **Composition BOM** | CycloneDX v1.6 JSON | What this spec depends on, builds with, produces | OWASP CycloneDX (ECMA-424) | +| **Composition BOM (CycloneDX)** | CycloneDX v1.6 JSON | What this spec depends on, builds with, produces | OWASP CycloneDX (ECMA-424) | +| **Composition BOM (SPDX)** | SPDX 3.0.1 JSON-LD | Same composition data, ISO-normative format | ISO 5962:2023 | These layers are orthogonal: - The provenance graph answers *"Why does this constraint exist?"* (regulatory, design decision, conversation) - The SpeckBOM answers *"What is this spec made of, and can I reproduce it?"* (dependencies, toolchain, artifacts) -Together they form the complete audit trail: **intent** (PROV-O) + **composition** (CycloneDX) = **full accountability**. +Together they form the complete audit trail: **intent** (PROV-O) + **composition** (CycloneDX or SPDX) = **full accountability**. --- -*This is a v0.2-DP specification. Dark Provenance and SpeckBOM primitives are optional but recommended for safety-critical and regulated systems. The SpeckBOM compilation output extends CycloneDX v1.6 (OWASP/ECMA-424). Feedback welcome via the [Speckl repository](https://os.scoble.me/forgejo/sscoble/speckl).* \ No newline at end of file +*This is a v0.2-DP specification. Dark Provenance and SpeckBOM primitives are optional but recommended for safety-critical and regulated systems. SpeckBOM compilation output supports both CycloneDX v1.6 (OWASP/ECMA-424) and SPDX 3.0.1 (ISO 5962:2023). Feedback welcome via the [Speckl repository](https://os.scoble.me/forgejo/sscoble/speckl).* \ No newline at end of file