ARCHITECTURE.md
1 # Cerro Torre Architecture 2 3 ## Overview 4 5 Cerro Torre is designed as a pipeline that transforms upstream source packages into verified, signed container images with complete provenance. 6 7 ``` 8 ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ 9 │ Upstream │───►│ Import │───►│ Build │───►│ Export │ 10 │ Source │ │ │ │ │ │ │ 11 └─────────────┘ └─────────────┘ └─────────────┘ └─────────────┘ 12 │ │ │ 13 ▼ ▼ ▼ 14 ┌─────────────────────────────────────────────────┐ 15 │ Provenance Chain │ 16 │ (hashes, signatures, attestations at each step)│ 17 └─────────────────────────────────────────────────┘ 18 ``` 19 20 ## Core Principles 21 22 ### 1. Verification Over Trust 23 24 Every claim is backed by cryptographic evidence: 25 - Upstream sources verified against known hashes 26 - Build outputs verified against expected results 27 - Signatures from identified keys with recorded trust 28 29 ### 2. Formal Verification for Security-Critical Code 30 31 The `src/core/` modules use SPARK annotations: 32 - `cerro_crypto` - All cryptographic operations 33 - `cerro_manifest` - Manifest parsing and validation 34 - `cerro_provenance` - Provenance chain verification 35 36 SPARK proofs guarantee: 37 - No buffer overflows 38 - No integer overflows 39 - No uninitialised memory access 40 - Functional correctness of crypto operations 41 42 ### 3. Separation of Concerns 43 44 ``` 45 ┌─────────────────────────────────────────────────────────────┐ 46 │ CLI Layer │ 47 │ (src/cli/cerro_main) │ 48 ├─────────────────────────────────────────────────────────────┤ 49 │ Orchestration Layer (Non-SPARK Ada) │ 50 │ ┌──────────┐ ┌──────────┐ ┌──────────┐ ┌──────────┐ │ 51 │ │ Importers│ │ Builder │ │ Exporters│ │ Policy │ │ 52 │ └──────────┘ └──────────┘ └──────────┘ └──────────┘ │ 53 ├─────────────────────────────────────────────────────────────┤ 54 │ Core Layer (SPARK Verified) │ 55 │ ┌──────────┐ ┌──────────┐ ┌──────────┐ ┌──────────┐ │ 56 │ │ Crypto │ │ Manifest │ │Provenance│ │ Verify │ │ 57 │ └──────────┘ └──────────┘ └──────────┘ └──────────┘ │ 58 └─────────────────────────────────────────────────────────────┘ 59 ``` 60 61 ## Module Descriptions 62 63 ### Core Layer (`src/core/`) 64 65 **cerro_crypto.ads/adb** 66 - Hash functions (SHA-256, SHA-384, SHA-512, BLAKE3) 67 - Ed25519 signature verification 68 - Constant-time comparison (timing attack prevention) 69 - Hex encoding/decoding 70 71 **cerro_manifest.ads/adb** 72 - Package manifest data types 73 - TOML parsing into Manifest records 74 - Structural validation 75 - Serialisation back to TOML 76 77 **cerro_provenance.ads/adb** 78 - Provenance chain data structures 79 - Upstream hash verification 80 - Patch hash verification 81 - Chain integrity checking 82 83 **cerro_verify.ads/adb** 84 - High-level verification API 85 - Policy-based verification 86 - Combines manifest, provenance, and signature checks 87 88 ### Orchestration Layer 89 90 **src/build/cerro_builder.ads/adb** 91 - Source fetching with hash verification 92 - Patch application 93 - Build command execution 94 - Reproducibility checking 95 96 **src/policy/cerro_selinux.ads/adb** 97 - SELinux policy generation (CIL format) 98 - Permission checking 99 - Policy installation 100 101 ### Importers (`src/importers/`) 102 103 Each importer translates from a distribution's package format to Cerro manifests: 104 105 **debian/** - Debian .dsc files 106 - Parse control file format 107 - Extract source and patches 108 - Map dependencies 109 110 **fedora/** - Fedora SRPMs 111 - Parse RPM .spec files 112 - Koji integration 113 - Handle macros 114 115 **alpine/** - Alpine APKBUILD 116 - Parse shell script format 117 - aports repository support 118 119 ### Exporters (`src/exporters/`) 120 121 Each exporter produces output in a target format: 122 123 **oci/** - OCI Container Images 124 - Rootfs creation 125 - OCI config.json generation 126 - Registry push 127 - SLSA provenance attachment 128 129 **rpm-ostree/** - OSTree Repositories 130 - OSTree commit creation 131 - Static delta generation 132 - rpm-ostree treefile generation 133 134 ## Data Flow 135 136 ### Import Flow 137 138 ``` 139 1. User: cerro import debian:nginx/1.26.0-1 140 2. Importer downloads .dsc from Debian mirror 141 3. Importer parses .dsc, extracts metadata 142 4. Importer downloads orig.tar.gz and debian.tar.gz 143 5. Core verifies hashes against Debian's recorded values 144 6. Importer generates .ctp manifest with full provenance 145 7. Manifest saved to manifests/nginx.ctp 146 ``` 147 148 ### Build Flow 149 150 ``` 151 1. User: cerro build manifests/nginx.ctp 152 2. Builder reads manifest 153 3. Core verifies manifest signatures 154 4. Builder fetches source (re-verifying hashes) 155 5. Builder applies patches in order (verifying each) 156 6. Builder runs build commands in isolated environment 157 7. Builder collects output files and hashes them 158 8. Builder updates manifest with file hashes 159 9. Builder signs manifest with builder key 160 10. Artifacts saved to output directory 161 ``` 162 163 ### Export Flow 164 165 ``` 166 1. User: cerro export --format=oci nginx:1.26.0-1 167 2. Exporter reads manifest 168 3. Core verifies manifest and signatures 169 4. Exporter creates rootfs from file list 170 5. Exporter generates OCI config.json 171 6. Exporter creates OCI image tarball 172 7. Exporter attaches provenance attestation 173 8. Image ready for podman load or registry push 174 ``` 175 176 ## Security Model 177 178 ### Trust Boundaries 179 180 ``` 181 ┌─────────────────────────────────────────────────────────────┐ 182 │ Untrusted Zone │ 183 │ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ │ 184 │ │ Network │ │ Upstream │ │ User │ │ 185 │ │ Traffic │ │ Sources │ │ Input │ │ 186 │ └──────┬──────┘ └──────┬──────┘ └──────┬──────┘ │ 187 └─────────┼────────────────┼────────────────┼─────────────────┘ 188 │ │ │ 189 ▼ ▼ ▼ 190 ┌─────────────────────────────────────────────────────────────┐ 191 │ Verification Boundary │ 192 │ (SPARK-verified code) │ 193 │ All data validated before further processing │ 194 └─────────────────────────────────────────────────────────────┘ 195 │ 196 ▼ 197 ┌─────────────────────────────────────────────────────────────┐ 198 │ Trusted Zone │ 199 │ ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ │ 200 │ │ Verified │ │ Signed │ │ Trusted │ │ 201 │ │ Manifests │ │ Artifacts │ │ Keys │ │ 202 │ └─────────────┘ └─────────────┘ └─────────────┘ │ 203 └─────────────────────────────────────────────────────────────┘ 204 ``` 205 206 ### Key Management 207 208 - **Upstream keys**: Verify source authenticity (GPG keys from GNU, etc.) 209 - **Builder keys**: Attest to reproducible builds 210 - **Maintainer keys**: Approve packages for distribution 211 - **Witness keys**: Sign transparency log entries 212 213 Keys are stored in `keys/` with trust levels in `keys/trust.toml`. 214 215 ## Future Architecture 216 217 ### Federated Transparency Log 218 219 ``` 220 ┌─────────────┐ ┌─────────────┐ ┌─────────────┐ 221 │ Operator A │ │ Operator B │ │ Operator C │ 222 │ Log │◄──►│ Log │◄──►│ Log │ 223 └──────┬──────┘ └──────┬──────┘ └──────┬──────┘ 224 │ │ │ 225 └──────────────────┼──────────────────┘ 226 │ 227 ┌─────▼─────┐ 228 │ Witness │ 229 │ Network │ 230 └───────────┘ 231 ``` 232 233 Each operator maintains their own log. Witnesses cross-verify consistency. Clients can query any operator and verify against witnesses.