Cerro Torre

Provenance-verified container packaging with cryptographic supply chain guarantees.

Cerro Torre is a SPARK/Ada-verified toolchain for packaging container images into cryptographically signed .ctp bundles. It provides complete provenance chain from source to deployment, integrating with Svalinn (gateway) and Vörðr (runtime) for verified container operations.

The name references Patagonia’s most technically demanding peak. Cerro Torre stands for doing things properly: fair means, complete transparency, no shortcuts.

Why Cerro Torre?

The container base image landscape offers:

• Alpine: Minimal and excellent, but limited supply chain transparency

• Wolfi: Strong security focus, but governed by a VC-backed company

Cerro Torre offers a third path:

| Principle | What It Means | |-----------|---------------| | Formally Verified | Core tooling written in Ada/SPARK with machine-checked proofs | | Democratically Governed | Multi-stakeholder cooperative, no corporate parent | | Radically Transparent | Complete cryptographic provenance for every package | | Format Agnostic | Import from Debian, Fedora, Alpine — not locked to any upstream | | Ethically Committed | The Palimpsest Covenant articulates our values |

Architecture

┌─────────────────────────────────────────────────────────────────┐
│                         IMPORTERS                                │
│  ┌─────────┐  ┌─────────┐  ┌─────────┐  ┌─────────┐            │
│  │ Debian  │  │ Fedora  │  │ Alpine  │  │  Nix    │   ...      │
│  │  .dsc   │  │  SRPM   │  │APKBUILD │  │  .drv   │            │
│  └────┬────┘  └────┬────┘  └────┬────┘  └────┬────┘            │
│       │            │            │            │                  │
│       └────────────┴─────┬──────┴────────────┘                  │
│                          ▼                                      │
│  ┌───────────────────────────────────────────────────────────┐  │
│  │              CERRO TORRE MANIFEST (.ctp)                  │  │
│  │         Declarative · Turing-Incomplete · Verifiable      │  │
│  └─────────────────────────┬─────────────────────────────────┘  │
│                            ▼                                    │
│  ┌───────────────────────────────────────────────────────────┐  │
│  │              SPARK-VERIFIED BUILD CORE                    │  │
│  │  Cryptographic Ops · Manifest Parsing · Provenance Chain  │  │
│  └─────────────────────────┬─────────────────────────────────┘  │
│                            ▼                                    │
│  ┌───────────────────────────────────────────────────────────┐  │
│  │                    ATTESTATIONS                           │  │
│  │  in-toto · SBOM · Federated Transparency Logs            │  │
│  └─────────────────────────┬─────────────────────────────────┘  │
│                            ▼                                    │
│                        EXPORTERS                                │
│  ┌─────────┐  ┌─────────┐  ┌─────────┐  ┌─────────┐            │
│  │   OCI   │  │ OSTree  │  │  .deb   │  │  .rpm   │            │
│  │ Images  │  │ Commits │  │ Compat  │  │ Compat  │            │
│  └─────────┘  └─────────┘  └─────────┘  └─────────┘            │
└─────────────────────────────────────────────────────────────────┘

The Manifest Format

Cerro Torre packages are defined in .ctp manifest files — a declarative, Turing-incomplete format designed for formal verification. Package definitions cannot contain arbitrary computation, making them analysable and provable.

See [spec/manifest-format.md](spec/manifest-format.md) for the full specification.

Import Sources

Primary: Debian — Chosen for governance alignment. Debian is genuinely community-governed with constitutional documents, elected leadership, and no corporate owner. Building on democratic foundations matters for a democratically-governed project.

Secondary: Fedora — For packages where Fedora’s version is better maintained, and for SELinux reference policies.

Extensible: The importer architecture allows community contribution of additional sources (Alpine, Nix, Arch, etc.).

Security

• SELinux Enforcing: First-class SELinux support with auto-generated per-container policies

• Threshold Signing: k-of-n keyholders required for releases; no single point of trust

• Federated Transparency: Multiple independent log operators; threshold agreement required

• Reproducible Builds: Any party can rebuild and verify packages

Licensing

Cerro Torre tooling is dual-licensed under your choice of:

• Palimpsest-MPL-1.0 License — Maximum permissiveness

• AGPL-3.0-or-later — Copyleft with network provisions

The Palimpsest Covenant travels alongside as a values commitment (not a legal requirement). Community members are encouraged to adopt it.

Packages retain their upstream licenses.

Governance

Cerro Torre is owned by a multi-stakeholder cooperative with:

• Maintainer Members: Active package/infrastructure maintainers (one person, one vote on technical decisions)

• User Members: Organisations and individuals using Cerro Torre in production (vote on strategic direction)

• Asset Lock: If dissolved, assets go to another cooperative or charity, never to private interests

• Fork Protection: Forking is explicitly encouraged; the cooperative exists to be useful, not to control

See [governance/](governance/) for full documentation.

Project Structure

cerro-torre/
├── spec/                    # Specifications
│   ├── manifest-format.md   # .ctp format specification
│   ├── provenance-chain.md  # Attestation requirements
│   └── transparency-log.md  # Federated log protocol
├── governance/              # Cooperative documents
│   ├── articles.md          # Bylaws
│   ├── covenant.md          # Palimpsest Covenant
│   └── decisions/           # Decision records
├── src/                     # Ada/SPARK implementation
│   ├── core/                # SPARK-verified (crypto, parsing, verification)
│   ├── importers/           # Debian, Fedora, etc.
│   ├── exporters/           # OCI, OSTree, etc.
│   ├── build/               # Build orchestration
│   └── policy/              # SELinux generation
├── manifests/               # Package manifests (.ctp)
├── keys/                    # Public keys and policies
└── docs/                    # Documentation

Project Status

Phase 0: Foundations — MVP v0.1.0-alpha

Component	Status	Description
Manifest Parser	Complete	.ctp TOML-like format with metadata, provenance, dependencies
Crypto Core	Complete	SHA-256/SHA-512 (FIPS 180-4), Ed25519 signatures (RFC 8032)
Bundle Packing	Complete	ct pack creates tar-based .ctp bundles
Bundle Verification	Complete	ct verify checks hashes, signatures, policy
Trust Store	Complete	Local key management with trust levels
Help System	Complete	ct help, ct explain, ct man with JSON output for CI/CD
Policy Engine	In Progress	Allow/deny rules for deployment
Registry Operations	Planned	ct fetch, ct push for remote registries

Building from Source

Prerequisites

• GNAT (>= 13.0) — Ada compiler

• Alire (recommended) or GPRbuild

Build

# Using Alire (recommended)
alr build

# Or directly with GPRbuild
gprbuild -P cerro_torre.gpr

# Build modes: Development, Release, Proof
gprbuild -P cerro_torre.gpr -XCERRO_BUILD_MODE=Release

The ct binary is placed in bin/.

CLI Commands

# Core commands
ct pack <image> -o <file>                  # Pack OCI image into .ctp bundle
ct verify <bundle.ctp> [--policy <file>]   # Verify bundle
ct explain <bundle>                        # Show verification chain

# Runtime integration
ct run <bundle> [--runtime=svalinn]        # Run via Svalinn/podman/docker
ct unpack <bundle> -o <dir>                # Extract to OCI layout

# Key management
ct keygen [--id <name>]                    # Generate signing keypair
ct key list                                # List trusted keys
ct key import <file.pub>                   # Import public key
ct key trust <id> <level>                  # Set trust level

# Distribution
ct fetch <ref> -o <file>                   # Fetch from registry
ct push <bundle> <dest>                    # Push to registry

# Diagnostics
ct doctor                                  # Check pipeline health
ct diff <old> <new>                        # Compare bundles

# Help
ct help [command]                          # Command help
ct version [--json]                        # Version info
ct man <topic>                             # Man-page style docs

Integration with Svalinn Ecosystem

Component	Role	Integration
Svalinn	Edge gateway	Validates .ctp bundles before deployment
Vörðr	Container runtime	Verifies attestations, executes containers
verified-container-spec	Protocol specification	Defines attestation formats

End-to-End Workflow

# 1. Package an image with Cerro Torre
ct pack docker.io/library/nginx:1.26 -o nginx.ctp

# 2. Verify the bundle
ct verify nginx.ctp --policy strict.json

# 3. Run via Svalinn gateway (which delegates to Vörðr)
ct run nginx.ctp --runtime=svalinn

# Or run directly with Vörðr
vordr run nginx.ctp --verify

Project Structure

cerro-torre/
├── src/
│   ├── core/               # SPARK-verified (crypto, parsing)
│   │   ├── cerro_crypto.adb
│   │   ├── cerro_manifest.adb
│   │   ├── cerro_provenance.adb
│   │   └── cerro_trust_store.adb
│   ├── cli/                # Command-line interface
│   │   ├── cerro_main.adb
│   │   └── cerro_cli.adb
│   ├── build/              # Bundle creation/verification
│   │   ├── cerro_pack.adb
│   │   └── cerro_verify.adb
│   ├── importers/          # Source format importers
│   │   ├── debian/
│   │   ├── fedora/
│   │   └── alpine/
│   ├── exporters/          # Output format exporters
│   │   ├── oci/
│   │   └── rpm-ostree/
│   ├── policy/             # SELinux generation
│   └── runtime/            # Runtime integration
├── spec/                   # Specifications
│   └── manifest-format.md
├── governance/             # Cooperative documents
├── cerro_torre.gpr         # GNAT project file
└── README.adoc

Getting Involved

Read the Palimpsest Covenant first. If those values resonate, see CONTRIBUTING.md.

License

Dual-licensed under:

• Palimpsest-MPL-1.0 License

• AGPL-3.0-or-later

See LICENSE.txt for details.