Skip to content

Security: ib823/proof

Security

SECURITY.md

Security Policy

Reporting

If you discover a security issue in RIINA™, please report it responsibly.

Security contact: ikmal.baharudin@gmail.com (PGP key on request) — or Telegram: @ib823. A dedicated security@ alias is being established; until it is live, use the contact above and put SECURITY in the subject.

Please do not open a public GitHub issue, PR, or discussion for security reports.

Response & Coordinated Disclosure Timeline

RIINA follows a 90-day coordinated disclosure policy (aligned with the norms used by Google Project Zero / CERT/CC):

  • 72 hours — Acknowledgment of your report.
  • 7 days — Initial assessment and severity classification (see bands below).
  • 30 days — Target for a fix or mitigation (Critical issues prioritized).
  • 90 days — Default public-disclosure deadline. We coordinate the date with you; we may request a short extension for a hard fix, and we may disclose earlier if the issue is already being exploited in the wild. Either party may shorten the window by mutual agreement.

EU CRA reporting readiness (Regulation (EU) 2024/2847)

Status: process documented; scope decision pending. Whether RIINA-the-product is itself "placed on the EU market" within CRA scope is an owner/legal determination (tracked as REQ-45 in RIINA_MASTER_PLAN.md). The process below is maintained NOW so that, if scope applies, the Art. 14 clocks can be met from day one. This section is a reporting PROCESS, not a claim of CRA conformity.

From 11 September 2026, Art. 14 requires manufacturers to report to ENISA and the designated national CSIRT, via the single reporting platform:

Trigger Deadline RIINA action
Awareness of an actively exploited vulnerability 24 h early warning Maintainer files the early warning; the SBOMs below identify affected components
Same event 72 h full notification Vulnerability notification incl. severity + corrective measures available so far
Corrective measure available 14 d final report Final report; VEX updated (see below)
Severe incident impacting product security 24 h / 72 h / 1 month Same ladder, incident variant

Machine-readable inputs kept current in this repository:

  • SBOMsbom/riina-proto.cdx.json, sbom/riina-tooling.cdx.json (CycloneDX, deterministic, regenerated by scripts/generate-sbom.sh; both prove zero third-party runtime dependencies, which keeps the component blast-radius of any report to RIINA's own code).
  • VEXsbom/riina.vex.cdx.json (CycloneDX VEX, same script). Records the exploitability status of published vulnerabilities against RIINA components; currently empty of affected entries, which is itself the machine-readable statement "no known exploited vulnerabilities".
  • The compiler-checkable slice of CRA Annex I is enforced as the cra compliance profile (riinac … --profiles cra); its scope note is explicit that passing it is not conformity.

Severity classification

We classify using CVSS v3.1 qualitative bands, applied to residual impact:

Band Example Handling
Critical Miscompile that silently breaks a security guarantee; key/secret recovery Immediate; out-of-band fix if needed
High Soundness hole in the type/effect/IFC checker; CT leak with a practical oracle Prioritized in the 30-day target
Medium DoS on the compiler (crafted input → hang/OOM); FFI-boundary issue in the playground shim Standard window
Low Hardening gaps without a practical exploit Batched into normal releases

The maintainers' own view of the current residual-Medium-and-above risks is published openly in 04_SPECS/security/THREAT_MODEL.md §8 (Open Risks) — we do not hide the gaps.

CVE handling

  • For any issue rated Medium or above that affects a released artifact, we will request a CVE (via GitHub's CNA for this repository, or MITRE directly) and reference it in the advisory and CHANGELOG.md.
  • Advisories are published via GitHub Security Advisories (GHSA) after a fix is available; the GHSA ID and any CVE are cross-linked.
  • Fixes land with a regression test (and, where the affected component has one, an updated Coq/CT anchor) so the issue cannot silently regress.

Scope

In scope: the compiler (riinac, all passes + codegen + verification), the formal proofs (02_FORMAL/), the tooling/crypto (05_TOOLING/, esp. riina-core), the website (website/), and the VS Code extension (riina-vscode/).

Known limitations that are documented, not vulnerabilities (see the threat model): source-level constant-time cannot defeat DMP/GoFetch or transient-execution (Downfall/Inception) leaks on affected hardware — those require deploy-time hardware/OS controls (DIT, microcode, kernel mitigations). Reports demonstrating a practical leak through RIINA-generated code on a mitigated host are in scope and very welcome.

Out of Scope

  • Example programs in 07_EXAMPLES/ (educational, not production).
  • Documentation content (unless it leaks secrets).
  • The downstream toolchain (cc, wasmtime, the OS, the CPU) — each is its own TCB; RIINA's guarantee ends at what it emits (threat model TB-2). Bugs in those projects go to those projects.
  • Findings that require a malicious host OS, physical access, fault injection, or power/EM analysis.

Safe Harbor

We will not pursue legal action against researchers who, in good faith, follow this policy: who access only their own data (or test data), avoid privacy violations and service degradation, and give us a reasonable window to remediate before public disclosure. If in doubt, ask first via the security contact.

Responsible Disclosure (process)

  1. Reporter sends details via the contact above.
  2. We acknowledge receipt within 72 hours.
  3. We work with the reporter to reproduce and assess the issue.
  4. We develop, test, and (where applicable) prove the fix.
  5. We release the fix, request a CVE if Medium+, and credit the reporter (unless anonymity is requested).
  6. We publish a GHSA advisory after the fix is available and coordinate public disclosure (≤ 90 days).

Recognition

We gratefully acknowledge security researchers who report issues responsibly. With your permission, we will credit you in our CHANGELOG.md and security advisories.


RIINA takes security seriously. Our formal-verification approach makes many classes of bug mathematically impossible within the proven fragment — but we remain vigilant about the components that fall outside our proof coverage, and we document those boundaries openly in 04_SPECS/security/THREAT_MODEL.md.

There aren't any published security advisories