SECURITY.md

<!--
Copyright (c) 2026 Ahmad Ali Parr. All rights reserved.
SPDX-License-Identifier: LicenseRef-Proprietary
Public source visibility does not grant an open-source license. See LICENSE.
-->

# Security policy

## Supported scope

| Version | Scope |
| --- | --- |
| v1.0.x | Maintainer triage for the verification scaffold and build/proof workflow |
| Unreleased runtime designs | Design review; no supported deployed interpreter |

The repository is public and source-visible. v1 contains interfaces, a proof/control model, and an
allocation counter. It is not a sandbox for executing untrusted Unlambda code.
Passing typechecks and the counter's SPARK proofs do not establish security of
an interpreter, an FFI adapter, or a production deployment.

## Report privately

Email the repository owner at **ahmedparr93@gmail.com** with subject
`[unlambda-idris-spark] Security report`. This is the contact published on the
[maintainer's GitHub profile](https://github.com/AHMADALIPARR). If GitHub private
vulnerability reporting is enabled later, the repository's Security tab may
also provide a private report form. Do not assume that form is currently enabled.

Include the affected commit/version, relevant toolchain versions, a minimal
reproduction, expected impact, and suggested remediation if available. Do not
include credentials, personal data, or live customer input. Avoid publishing
an exploit or opening an ordinary issue containing sensitive details while
the report is being investigated.

The maintainer reviews reports and coordinates fixes and disclosure. No fixed
response SLA or paid bounty program is currently promised.

## What to report

- Build or agent-hook execution that can expose secrets or run unintended commands.
- A proof gate that reports success despite missing, suppressed, or unproved checks.
- Unsafe future handle lookup, generation reuse, or incorrect memory exhaustion.
- Release asset/source mismatch, compromised dependencies, or false evidence claims.
- A defect in the checked model or contracts that invalidates a documented result.

## Build and proof boundaries

CI actions and compiler sources are pinned; the GNATprove archive is checksum
verified. Evidence is tied to source commits. Credentials and local
`agent_hooks.sh` must not be committed. Generated proof modules require the same
review and typechecking as handwritten modules. Third-party compilers, provers,
and runtime libraries remain part of the trusted toolchain.