Sicherheit

Der größte Teil der Sicherheit von Hilde kommt aus der Sprache selbst: Jede Ressource wird genau einmal verwendet (lineare Typen), jede Funktion nennt ihren Vertrag, jeder Index wird geprüft, und schlechte Eingaben werden abgelehnt, statt einen Absturz auszulösen. Diese Seite beschreibt, was die Standardbibliothek darüber hinaus bietet und wo ihre Grenzen liegen.

„unsafe“ nur in den Bindings

Die Sprache selbst braucht keinen unsafe-Code. Ein Modul ist nur dann unsafe, wenn sein Rumpf pragma Unsafe_Module; enthält. Nur ein solches Modul darf eine C-Funktion einbinden (pragma Foreign_Import), C mit @embed einfügen oder Hilde.Memory importieren, das eingebaute Modul für rohen Speicher. Der Compiler prüft das (H2028, H2038).

• In Hilde sind die unsafe-Module zum einen die dünnen Bindings an C-Bibliotheken unter Bindings.* (36 Module), zum anderen die aus Spezifikationen erzeugten C-Deklarationen (11 Module). Ein Programm kann kein Bindings.*-Modul importieren (H2045), sondern verwendet das sichere Standard.*-Modul darüber. Die Prüfläufe gleichen die Liste der unsafe-Module mit dem Quelltext ab.
• Auch der eingebaute Kern des Compilers ist unsafe: Hilde.Pervasive, das Prelude, enthält die Arithmetik als eingebettetes C, Hilde.Memory verwaltet rohen Speicher, und Hilde.Array prüft jeden Index, bevor es auf Speicher zugreift.
• In MIRCO gibt es genau acht unsafe-Module, alle unter Bindings (DuckDB, HDF5, LAPACK, libm, netCDF, Number, pocketfft, Ziggurat). Wolly, RAMBO, ROXIE und lea haben überhaupt kein unsafe-Modul.
• hilde compile --forbid-unsafe-modules verbietet unsafe-Module auf der Kommandozeile einer Anwendung. hilde guard zeigt die Angriffsfläche eines Programms: seine unsafe-Module, C-Bibliotheken, fremden Funktionen und Einbettungen, und welche davon das Programm tatsächlich erreicht.

Sandbox

Standard.Sandbox beschränkt den laufenden Prozess auf das, was eine Richtlinie erlaubt. Eine Richtlinie nennt Zusagen mit den Begriffen von pledge und Pfade mit den Rechtebuchstaben von unveil. Der Bericht der Sandbox nennt genau die Mechanismen, die tatsächlich gegriffen haben. Er hält das Programm nicht an. Was ein nicht eingeschränkter Lauf bedeutet, entscheidet das Programm selbst. Der Code stammt aus der Sandbox, die für den Webserver Hiawatha geschrieben wurde, und wurde für Hilde angepasst.

Unter Android, auf anderen Systemen und innerhalb einer Bibliothek wird nichts angewendet, und der Bericht sagt das auch.

Ein vollständiges Programm: Es sagt Standardausgabe und Lesen zu, gibt das Arbeitsverzeichnis zum Lesen frei, wendet die Richtlinie an und gibt den Bericht aus. Für diese Seite wurde es mit hilde check geprüft, übersetzt und unter Linux ausgeführt:

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

Signaturen: ML-DSA-44 mit Ed25519

Standard.MlDsa bietet ML-DSA nach FIPS 204 in den Stufen 44, 65 und 87. Der Code stammt aus libcrux, in der Fassung, die auch OpenSSH mitbringt, und verhält sich auf jedem System gleich. Standard.CompositeSig ist die zusammengesetzte Signatur aus ML-DSA-44 und Ed25519 nach dem IETF-Entwurf. Sie gilt nur, wenn beide Teilsignaturen stimmen. Wird eines der beiden Verfahren gebrochen, lässt sich damit allein also nichts fälschen. RAMBO signiert seine Tokens mit ML-DSA-44 oder, wenn ein Client das verlangt, mit der zusammengesetzten Signatur.

Vault

Standard.Vault speichert Geheimnisse in einer verschlüsselten .env-Datei, mit XChaCha20-Poly1305 und HMAC-SHA3-512. Der Schlüssel wird aus einem Hauptschlüssel und einem Pepper von genau 32 Byte abgeleitet, der Pepper liegt in einer eigenen Datei. Die Datei wird atomar mit den Rechten 0600 geschrieben, Eigentümer und Gruppe bleiben erhalten, und Schlüssel und Pepper lassen sich wechseln. Das Schlüsselmaterial ist ein linearer Wert und wird beim Schließen gelöscht. Das Format ist mit dem Vault der Go-Bibliothek kompatibel, die als Vorbild diente.

HTML bereinigen

sanitize in Standard.Html lässt nur durch, was eine Richtlinie erlaubt. Skripte, Frames und Formulare werden entfernt, URLs sind nur mit http, https und mailto erlaubt, und die Ausgabe ist immer wohlgeformt. Wolly.Markdown schickt auch sein eigenes HTML noch einmal durch diesen Filter.

Sanitizer für das erzeugte C

Eine andere Art Sanitizer prüft das erzeugte C. hilde test --memory führt die Tests unter AddressSanitizer und UndefinedBehaviorSanitizer aus, --race unter ThreadSanitizer. Die Prüfläufe des Projekts tun das bei jeder Testsuite.

Weiteres in der Standardbibliothek

• Passwörter mit Argon2id im PHC-Format und festen Parametern. Alte bcrypt-Hashes lassen sich prüfen und neu speichern. Hashes können gepfeffert werden.
• TLS über libtls mit Zertifikatsprüfung, die sich nicht abschalten lässt, TLS 1.3 und gegenseitiger Authentifizierung.
• Cookies nach RFC 6265, CSRF-Tokens per HMAC, Sitzungen auf dem Server, Benutzerkonten mit Sperre und begrenzter Zahl von Anmeldeversuchen.
• XML ohne DTDs und damit ohne XXE. Archive prüfen Dateinamen auf .. und absolute Pfade. Parser lehnen ab, statt zu raten.
• Standard.HashMap verwendet SipHash-1-3 mit einem zufälligen Schlüssel gegen Hash-Flooding.
• Standard.SqlCipher für verschlüsselte Datenbanken; der Schlüssel ist ein linearer Wert und wird gelöscht.

Pakete

Pakete und Releases werden mit signify signiert. Wie man sie prüft und wo die öffentlichen Schlüssel liegen, steht auf der Seite Pakete.