Security

Most of Hilde's safety comes from the language: a resource is used exactly once (linear types), a function states its contract, an index is checked, and bad input is answered with a refusal, not a crash. This page describes what the standard library adds and where its limits are.

"unsafe" only in the bindings

The language itself needs no unsafe code. A module is unsafe only when its body says pragma Unsafe_Module;, and only such a module may bind a C function (pragma Foreign_Import), paste C with @embed, or import Hilde.Memory, the built-in module of raw memory. The compiler checks this (H2028, H2038).

• The unsafe modules are the thin bindings to C libraries, Bindings.* (36 modules), and the C declarations generated from specifications, Bindings.C.* (11 modules). A programme cannot import a Bindings.* module (H2045); it imports the safe Standard.* module built on it. The build checks hold the list of unsafe modules to the source.
• The compiler's built-in core is unsafe too: Hilde.Pervasive, the prelude, carries arithmetic as embedded C, Hilde.Memory holds raw memory, and Hilde.Array checks every index before it touches memory.
• In MIRCO all eight unsafe modules lie in src/Bindings (DuckDB, HDF5, LAPACK, libm, netCDF, Number, pocketfft, Ziggurat). Wolly, RAMBO, ROXIE and lea have no unsafe module at all.
• hilde compile --forbid-unsafe-modules refuses unsafe modules on an application's command line, and hilde guard reports a programme's attack surface: its unsafe modules, C libraries, foreign functions and embeds, and which of them it reaches.

Sandbox

Standard.Sandbox confines the running process to what a policy allows. A policy names promises in the words of pledge and paths in the permission letters of unveil. Its report names each mechanism that took effect, and no other; nothing in it stops the programme, so what an unconfined run means is the programme's decision. The code was taken over and adapted from the sandbox written for the web server Hiawatha.

On Android, on other systems and in a library nothing is applied, and the report says so.

A complete programme: it promises standard output and reading, allows the working directory for reading, applies the policy and prints the report. It was checked with hilde check, compiled and run on Linux for this page:

import Standard.String (String, asSpan, destroyString);
import Standard.Sandbox (Policy, makePolicy, allowPromises, allowPath, Report, applyPolicy, describeReport);

module body Example.SandboxPolicy is
    function main(): ExitCode is
        let promised: Policy := allowPromises(makePolicy(), "stdio rpath");
        let policy: Policy := allowPath(promised, ".", "r");
        let report: Report := applyPolicy(policy);
        let line: String := describeReport(report);
        printLn(asSpan(&line));
        destroyString(line);
        return ExitSuccess();
    end;
end module body.

hilde check: 1 modules given, 6 checked, no error

sandbox:     no-new-privileges, landlock abi 10, 1 of 1 paths, seccomp

Signatures: ML-DSA-44 with Ed25519

Standard.MlDsa provides ML-DSA of FIPS 204 at the levels 44, 65 and 87, from the C code of libcrux that OpenSSH carries, the same on every system. Standard.CompositeSig is the composite signature ML-DSA-44 with Ed25519 after the IETF draft: it is valid only when both signatures hold, so a break of one method alone forges nothing. RAMBO signs its tokens with ML-DSA-44, or with the composite where a client asks for it.

Vault

Standard.Vault keeps secrets in an encrypted .env file: XChaCha20-Poly1305 and HMAC-SHA3-512, the key made from a key and a pepper of exactly 32 bytes, the pepper kept in a file of its own. The file is written atomically with mode 0600, owner and group are kept, key and pepper can be rotated, and the key material is a linear value, wiped when it is closed. The format is compatible with the vault of the Go library Hilde took as its model.

Sanitizer

sanitize in Standard.Html keeps only what a policy allows: code, frames and forms fall away, URLs are allowed only with http, https and mailto, and the output is always well formed. Wolly.Markdown sends its own HTML through it once more.

Sanitizers of another kind check the generated C: hilde test --memory runs the tests under AddressSanitizer and UndefinedBehaviorSanitizer, --race under ThreadSanitizer, and the build checks run them on every suite.

More in the standard library

• Passwords with Argon2id in the PHC format with fixed parameters; old bcrypt hashes can be checked and stored again; peppered hashes.
• TLS through libtls, with the certificate check that cannot be switched off, TLS 1.3 and mutual TLS.
• Cookies after RFC 6265, CSRF tokens by HMAC, sessions on the server, users with lockout and a limit of attempts.
• XML without DTDs and so without XXE; archives check names against .. and absolute paths; a parser refuses rather than guesses.
• Standard.HashMap with SipHash-1-3 under a random key, against hash flooding.
• Standard.SqlCipher for an encrypted database, its key linear and wiped.

Packages

Packages and releases are signed with signify; how to check them and where the public keys lie is on the packages page.