Guarantees and limits

A library like this is only worth using if it is precise about where it stops. This page states the guarantees, the things that look like guarantees but are best effort, and the things that are outside its reach entirely.

Why the heap is the problem

A key in an OCaml bytes is not in one place. The minor collector promotes a surviving block by copying it into the major heap and leaving the original bytes behind in the minor heap; Gc.compact moves major-heap blocks the same way. Neither erases the source. By the time you call Bytes.fill you are erasing the newest copy, not the ones the runtime left in its wake.

A Secret.t is a small custom block in the heap that owns a payload allocated in C memory. The handle may be copied and moved freely; the payload never is. There is exactly one place to erase, and the library erases it with a primitive the C compiler is not allowed to optimise away.

What is guaranteed

The payload is never copied by the GC.

It lives outside the heap for the whole life of the value. Promotion and compaction move the handle, not the bytes.

It is zeroized before its memory can be reused.

On destroy, on finalization of the handle, and on wipe_all at normal exit. The zeroization uses memset_explicit, explicit_bzero, explicit_memset, memset_s or SecureZeroMemory, whichever the platform probe finds, falling back to a volatile function pointer behind a barrier. The choice is compiled into its own translation unit so that only link-time optimisation could see across the call, and (Secret.capabilities ()).zeroize_primitive names it.

Comparison is constant time.

equal and equal_string compare the contents in C in time proportional to the length and independent of the values. Lengths are compared first with an ordinary branch: the length is not treated as secret. There is deliberately no compare and no hash.

The contents cannot leak by accident.

Polymorphic compare and Marshal raise Invalid_argument; Hashtbl.hash ignores the payload; pp prints <secret:32B>. Secret bytes reach OCaml values only through documented scratch-buffer callbacks and functions whose names contain expose, unsafe or view.

Use after destruction raises.

Every accessor through the owner raises Secret.Destroyed instead of returning stale bytes. destroy is idempotent, and length and status keep working. Unsafe views have their own lifetime rules below.

What is not guaranteed

None of the following is a bug in the library. They are the boundary of what any userspace library can do.

• Copies a cryptographic primitive spills to the C stack or to registers.
• Key-equivalent data that a library builds in the OCaml heap from a string key — an expanded AES schedule, for example. A zero-copy view removes the raw-key copy, not the schedule. This is measured in the leak census.
• Copies the kernel makes: the page cache for a file you read, socket buffers, a hibernation image.
• Copies you make yourself through expose, unsafe_to_string, or a view you pass to something that copies.
• Zeroization when the process dies without running handlers.
• Page locking and core-dump exclusion, which are best effort and reported rather than assumed — see status.
• Historical copies of a scratch buffer left by major-heap compaction. Wiping the current buffer cannot reach an older moved-from copy.
• Race safety for mutation, destruction, process-wide wiping, or blocking I/O. Callers must synchronize these operations.
• Anything against a root user, ptrace, a cold-boot attack, or a compromised kernel or hypervisor.

Where the wipe happens, and where it does not

Every row above the last two is asserted by test_atexit, test_gc or test_fork, mostly by running a child process and inspecting how it died. The two that cannot be asserted are the two that do not happen.

wipe_all is registered with Stdlib.at_exit when the module is initialised, which is before any handler registered by code that uses it. Handlers therefore run first and still see live secrets.

An explicit wipe_all requires a quiescent process: join or stop worker domains and finish blocking Secret_unix I/O first. Concurrent reads of a live secret are supported, but all mutation, destruction, and process-wide wiping require caller synchronization. Concurrent repeated calls to destroy are the exception and remain safe.

Two tiers

Both tiers may pool released unviewed payload blocks by size class and reuse them only after zeroization. Any allocation that has produced an unscoped view is zeroized and permanently parked instead: it is never reused or unmapped. This prevents cross-secret disclosure at the cost of process-lifetime, potentially unbounded memory retention. Unviewed blocks above the pool's size limit go back to the OS.

~hardened:true is a request. Where the platform has no mmap — Windows, or a freestanding target — the allocation falls back to the default tier and status.page_backed is false.

Nothing is silent

Every hardening feature reports its outcome per value. Secret.status never raises and works after destroy.

Reporting is the default, but it is not the only option. require_hardening takes a list of `Page_backed, `Guard_pages, `Canary, `Locked, `No_core_dump and `Wipe_on_fork, and destroys the secret before raising Hardening_unavailable with the first requirement it could not meet. A key that did not get the protection it asked for never reaches the caller.

Secret.capabilities () answers the same questions for the build and the platform as a whole, before any secret exists. It also reports the page size and the name of the zeroization primitive that was compiled in.

View lifetimes

A view is an ordinary OCaml string or bytes whose block header was written in front of the secret memory — a representation the runtime already supports and uses for static data. That is what lets an unmodified string-based API, including a C stub using String_val, read secret memory without a copy.

The rules that come with it:

• Destruction zeroizes unscoped-view storage and permanently parks it, so a stale view can never observe another secret. A retained mutable view can still modify its own parked storage.
• Store an unscoped view only next to its owner, so the owner stays reachable for as long as the view does. Every unscoped view causes permanent memory retention after destruction.
• A scoped view must not escape its callback. The bigstring view is revoked when the callback returns: its length becomes 0 and further access raises Invalid_argument. Sub-views made with Bigarray.Array1.sub inside the callback cannot be revoked.
• A view is exempt from none of the copying hazards of an ordinary string. String.sub, ^, compare and Marshal all copy.

Prefer scoped views. Their owner remains reachable throughout the callback, including when the callback raises or forces collection. A scoped view that escapes the callback is still a programming error: its unmarked storage may later be released or reused.

View access must obey the same concurrency contract: concurrent reads are supported, while mutation or destruction requires caller synchronization. No scoped or unscoped view may be in use during wipe_all.

On OCaml 4.14 the runtime classifies out-of-heap blocks through the page table, so polymorphic compare, =, Hashtbl.hash and Marshal treat a view as a foreign pointer: comparison is by address and marshalling fails. String.equal, every String and Bytes function, and C stubs using String_val behave identically on 4.14 and supported 5.0–5.5 releases. Use Secret.equal for contents, which is constant time on every supported compiler.

Fork

A forked child inherits copies of every secret, and memory locks are never inherited. The policy is explicit.

Platform matrix

Features are probed by a compile-and-link test at build time. A probe that cannot run reports the feature as unavailable and the C code takes a portable path, so a missing feature is never a build failure.

On a freestanding target — solo5, and so MirageOS — the payload, its zeroization and constant-time equality remain, and everything below them in the table is gone: no OS entropy, no page-backed tier, no fork policy. secret_platform.h forces that profile from the target compiler's own macros, so a build cannot switch on an OS feature that is not there.

Where no OS entropy source exists, Secret.random raises Entropy_unavailable until a generator is installed with Secret.set_entropy_source; the callback fills a scratch buffer that is wiped afterwards. A feature being compiled in does not mean it will succeed at run time — mlock is bounded by RLIMIT_MEMLOCK on every platform. That is what status is for.

The numbers behind the timing and leak claims are on the benchmarks page.