Vörðr is a formally verified container orchestration system under active development. This document describes our current security status and implementation roadmap.
| Component | Status | Language | Notes |
|---|---|---|---|
| Idris2 Formal Proofs | ✅ Complete | Idris2 | Container lifecycle, reversibility proofs |
| Type-Safe Runtime | ✅ Complete | Rust | Memory safety, no unsafe blocks |
| eBPF Monitoring (Userspace) | ✅ Complete | Rust (Aya) | Event handling, syscall filtering, anomaly detection |
| Reversible Operations | ✅ Complete | Elixir | GenStateMachine with rollback |
| Ada/SPARK Trust (Stub) | Ada/SPARK | Source exists, using C stub | |
| SHA-256 Hashing | ✅ Complete | Rust | Manifest verification |
| Component | Priority | Timeline | Impact |
|---|---|---|---|
| ML-DSA-87 Verification | CRITICAL | Q3 2026 | Cannot verify PQ-signed containers |
| Idris2 Runtime Integration | HIGH | Q2 2026 | Formal proofs not enforced at runtime |
| eBPF Kernel Programs | HIGH | Q3 2026 | No kernel-level syscall monitoring |
| Ada/SPARK Compilation | MEDIUM | Q2 2026 | Using C stubs, no formal verification active |
Current Limitation: Vörðr can only verify containers signed with Ed25519. Once Cerro Torre completes ML-DSA-87 implementation (Phase 1, Q3 2026), Vörðr will integrate post-quantum verification.
| Version | Supported | Notes |
|---|---|---|
main branch |
✅ Yes | Latest development (v0.1.0-alpha) |
| v0.1.0-alpha | ✅ Yes | First release (70% complete) |
| Earlier versions | ❌ No | Pre-production |
- Navigate to Report a Vulnerability
- Complete the form with as much detail as possible
- Submit — we'll receive a private notification
| jonathan.jewell@open.ac.uk | |
| Subject Line | [SECURITY] Vörðr: <brief description> |
⚠️ Important: Do not report security vulnerabilities through public GitLab issues or merge requests.
| Stage | Timeframe | Description |
|---|---|---|
| Initial Response | 48 hours | We acknowledge receipt and confirm we're investigating |
| Triage | 7 days | We assess severity, confirm the vulnerability, and estimate timeline |
| Status Update | Every 7 days | Regular updates on remediation progress |
| Resolution | 90 days | Target for fix development and release |
| Disclosure | 90 days | Public disclosure after fix is available (coordinated with you) |
As a container verification and orchestration system, Vörðr has specific security requirements:
- Current: SHA-256 manifest verification only
- Planned: ML-DSA-87 signature verification (awaits Cerro Torre library, Q3 2026)
- All cryptographic code will be in Ada/SPARK with formal proofs when compiled
- Threshold signatures planned for multi-stakeholder approval
- Current: eBPF userspace framework complete (Aya probes, event handling)
- Missing: Kernel-side eBPF programs not implemented yet (0%)
- eBPF code runs in kernel context — will be reviewed with extra scrutiny
- Privileged operations require explicit capability grants
- All eBPF programs are verified by the kernel's eBPF verifier
- Idris2 Proofs Complete: Container lifecycle, reversibility, SBOM verification
- Integration Pending: Proofs are machine-checked but not wired into Rust runtime yet
- Counterexamples are automatically generated for failed proofs
- Proof integration planned for Q2 2026
- Rust: Cargo.lock with hash-pinned dependencies
- Elixir: mix.lock with version pinning
- Idris2: .ipkg with explicit package versions
- SLSA Level 3 compliance target (when releases begin)
- Sigstore attestations planned for all releases
- Current: Manifest hash verification (SHA-256)
- Roadmap:
- Ed25519 signature verification (Q2 2026)
- ML-DSA-87 signature verification (Q3 2026, depends on Cerro Torre)
- SBOM vulnerability scanning (Q3 2026)
- Transparency log proof verification (Q4 2026)
-
No ML-DSA-87 Verification
- Cannot verify post-quantum signed containers
- Awaits Cerro Torre crypto library completion
- Mitigation: Only accept Ed25519-signed containers for now
- Fix: Q3 2026 (integrate Cerro Torre library)
-
Idris2 Proofs Not Enforced
- Formal proofs exist but not integrated into runtime
- Type-level guarantees not checked during container execution
- Mitigation: Rust type system provides memory safety
- Fix: Q2 2026 (wire Idris2 proofs to Rust runtime)
-
No eBPF Kernel Programs
- Userspace monitoring framework complete
- Kernel-side syscall filtering not implemented
- Impact: Cannot monitor syscalls at kernel level yet
- Fix: Q3 2026 (implement eBPF kernel programs)
-
Ada/SPARK Using C Stubs
- Ada source code exists but not compiled
- Using C stubs for threshold signatures and Gatekeeper
- Impact: No formal verification of trust decisions
- Fix: Q2 2026 (compile Ada/SPARK, remove C stubs)
-
No Database for Policy Storage
- Svalinn-project spec requires Virtuoso VOS for semantic policies
- Currently no policy persistence
- Options:
- PostgreSQL for MVP (1 week)
- Virtuoso VOS for spec compliance (3-4 weeks)
- Fix: Q3 2026
-
No WCAG 2.3 AAA Accessibility
- If building browser UI (MCP adapter), must meet WCAG 2.3 AAA
- Currently no UI, so not urgent
- Fix: Q4 2026 (if UI is built)
When deploying Vörðr in production:
- Only run containers from trusted registries
- Enable strict verification mode (reject on verification failure)
- Use Cerro Torre
.ctpbundles for cryptographic guarantees - Monitor verification failures in logs
- Enable eBPF monitoring for all containers (when kernel programs are implemented)
- Set syscall policies based on least-privilege principle
- Alert on anomalous behavior (unexpected syscalls, file access)
- Review eBPF probe logs regularly
- When Idris2 integration completes, enable runtime proof checking
- Review counterexamples for failed lifecycle transitions
- Use type-safe APIs (avoid FFI escape hatches)
- Run in isolated Kubernetes namespace or separate VM
- Use SELinux or AppArmor confinement
- Limit capabilities (CAP_SYS_ADMIN for eBPF only)
- Forward logs to SIEM
Components:
- Wire Idris2 proofs into Rust runtime
- Compile Ada/SPARK trust components (remove C stubs)
- Enable SPARK proofs for threshold signatures and Gatekeeper
- Runtime proof checking for container lifecycle
Estimated Effort: 4-6 weeks Impact: Formally verified trust decisions
Components:
- Integrate Cerro Torre crypto library
- Implement ML-DSA-87 signature verification
- Implement Ed25519 signature verification
- Support hybrid signatures (Ed25519 + ML-DSA-87)
- Transparency log proof verification
Estimated Effort: 3-4 weeks (depends on Cerro Torre completion) Impact: Post-quantum container verification
Components:
- Implement eBPF kernel programs (syscall, network, file access probes)
- Integrate with userspace monitoring framework
- Policy-based syscall filtering
- Real-time anomaly detection at kernel level
Estimated Effort: 4-5 weeks Impact: Deep runtime security monitoring
Components:
- PostgreSQL integration for policy storage (MVP)
- Virtuoso VOS integration for semantic policies (spec compliance)
- Policy versioning and rollback
- SPARQL 1.2 queries for policy retrieval
Estimated Effort: 3-4 weeks (PostgreSQL) or 6-8 weeks (Virtuoso VOS) Impact: Persistent policy enforcement
We follow coordinated disclosure (responsible disclosure):
- You report the vulnerability privately
- We acknowledge and begin investigation (48 hours)
- We develop a fix and prepare a release
- We coordinate disclosure timing with you
- We publish security advisory and fix simultaneously
- You may publish your research after disclosure
- We will not take legal action against researchers who follow this policy
- We will work with you to understand and resolve the issue
- We will credit you in the security advisory (unless you prefer anonymity)
- We will notify you before public disclosure
- Report vulnerabilities promptly after discovery
- Give us reasonable time to address the issue (90 days)
- Do not access, modify, or delete data beyond proof-of-concept
- Do not share vulnerability details until coordinated disclosure
| Purpose | Contact |
|---|---|
| Security issues | Report via GitLab or jonathan.jewell@open.ac.uk |
| Security questions | GitLab Issues (public, non-sensitive only) |
| General questions | See README.adoc for contact information |
- ARCHITECTURE.adoc - System architecture and formal verification approach
- API.adoc - MCP API security considerations
- Cerro Torre MISSING-SECURITY-COMPONENTS.adoc - Ecosystem security audit
- Palimpsest Covenant - Values and ethics
Thank you for helping keep Vörðr and its users safe. 🛡️
Last updated: 2026-01-28 · Policy version: 1.0.0 · v0.1.0-alpha Status (70% complete)