Spec couche 2 — le manifeste et l’octroi (ADR-150)

État (réconcilié le 2026-08-12). Incréments 1 à 5 faits — le mécanisme est complet de bout en bout : les deux artefacts existent, se lisent, se valident, l’invariant qui les relie est du code testé, la signature détachée établit qui présente un artefact, l’émission rend l’invariant inviolable par construction, l’arbitre enchaîne signature → octroi → enveloppe en refusant muettement, la largeur des enveloppes par défaut est tranchée (#657, option B) et la cage est posée depuis les entitlements accordés (#663).

Ce qui reste n’est plus un mécanisme mais une porte : rien ne relie un .airapp sur disque à spec.granted. Le chemin de l’octroi n’est fixé nulle part, et aucun code ne lit un bundle depuis un répertoire — voir §6. C’est le périmètre non écrit d’ADR-010.

1. Ce que cette spec réalise, et ce qu’elle ne réalise pas

ADR-150 tranche quatre choses : que l’octroi existe et soit distinct du manifeste (D1), que les deux soient binaires avec un codec texte pour le développeur (D2), l’ordre d’arbitrage signature → octroi → enveloppe (D3), et le refus muet, tracé (D4).

Cette spec réalise les quatre. Les §2 à §5ter décrivent les artefacts, leur schéma, leurs bornes, leur validation, l’invariant octroi ⊆ manifeste, la signature et l’émission ; §5quater réalise D3 et D4 — le lanceur vérifie la signature, cherche l’octroi, le plafonne par l’enveloppe, et refuse sans rien dire à l’appelant.

Ce qu’elle ne réalise pas : le lanceur ne sait pas d’où vient un bundle. Tout ce qui est décrit ici opère sur des artefacts déjà en mémoire — AppManifest::read(reader) prend un lecteur, pas un chemin. La disposition sur disque d’un .airapp, l’emplacement de l’octroi et l’installation qui l’émet relèvent d’ADR-010 et ne sont écrits nulle part.

2. Les deux artefacts

Schéma : crates/air-config-schema/schema/air-config-bundle.capnp. Lecture et validation : crates/air-bundle/src/lib.rs.

2.1 Pourquoi ils partagent leur vocabulaire

Entitlements — les quatre familles d’ADR-010 : filesystem, réseau, AirCom, périphériques — est le même type des deux côtés. Ce n’est pas une économie de code : c’est ce qui rend l’invariant écrivable. Comparer une demande et un accord exprimés dans deux langages différents exigerait une traduction, et toute traduction a des cas où elle arrondit — du mauvais côté une fois sur deux.

2.2 Fail-closed, jusque dans les défauts du format

Une liste vide n’accorde rien ; un booléen absent vaut faux ; un champ hors borne rejette l’artefact entier au lieu de l’amputer. Le défaut de Cap’n Proto — zéros et pointeurs nuls — est donc ici la position la plus fermée, ce qui rend un artefact tronqué inoffensif plutôt que permissif.

Un cas mérite d’être nommé : il n’existe pas de convention « liste de ports vide ⇒ tous les ports ». Le vide est ce que produit une troncature ; lui donner le sens le plus large ferait d’un accident une élévation de privilèges. « Tous les ports » se dit par un booléen explicite dont le défaut est faux.

3. Les bornes, et leurs valeurs

Aucune n’est laissée ouverte — une borne « à décider plus tard » devient un illimité que personne n’assume.

L’algorithme d’empreinte est figé, pas négocié : un champ « algorithme » côté artefact laisserait un attaquant choisir le plus faible que le lecteur accepte encore. En changer sera un champ neuf que les lecteurs à jour exigeront — un ajout, jamais une négociation.

4. La validation, et ce qu’elle attrape

Les chemins. Un chemin d’exécutable est relatif (sans quoi l’octroi d’une application couvrirait le lancement de /usr/bin/sh) ; un chemin de règle est absolu. Aucun ne tolère .., ., ni composant vide. .. est le cas qui compte : il fait sortir d’une arborescence sans que le texte le montre. Les deux autres sont refusés parce qu’ils donneraient deux écritures pour le même chemin, donc deux chances de se comparer inégal alors qu’ils désignent la même chose.

L’identifiant de bundle. Notation inversée, minuscules, chiffres, . et -, au moins deux composants, aucun vide. Il n’authentifie personne — c’est une clé d’index vers l’octroi — mais il finira dans un nom de fichier, et un identifiant portant / ou .. désignerait alors un autre octroi que le sien.

La confusion de type. Cap’n Proto ne type pas l’AnyPointer de l’enveloppe : rien dans le format n’empêche de lire un octroi pour un manifeste. Ce qui l’empêche est la vérification de domaine de AirConfig::reader::<T> (ManifestDomain, GrantDomain).

C’est une garde, pas une formalité. Si elle tombait, prendre un octroi pour un manifeste ferait lire granted à la place de requested : la demande deviendrait identique à l’accord, et l’invariant serait vrai par construction, donc vide. La divergence actuelle des deux dispositions fait qu’aujourd’hui la lecture échouerait de toute façon — mais c’est une coïncidence qui tient à la forme présente des schémas, et qu’un champ ajouté ferait disparaître sans que personne le remarque. Les tests le disent en ces termes, et le prouvent en désarmant la garde.

5. L’invariant

Un manifeste ne confère rien. Il demande. Seul un octroi valide autorise une exécution — et il n’autorise jamais plus que ce que le manifeste demandait.

Grant::authorizes(manifest, manifest_sha256, developer_key) est le seul endroit où cette phrase devient du code. Trois conditions de sujet, et il faut les trois :

1. même bundle — sinon l’octroi de l’un servirait à l’autre ;
2. même manifeste, à l’octet près — sinon un manifeste réécrit pour demander davantage retrouverait l’octroi rendu à sa version d’avant ;
3. même signataire — les deux premières disent quoi, aucune ne dit qui. Un tiers re-signant le même bundle avec sa propre clé présenterait le même identifiant et la même empreinte, et hériterait d’un accord rendu à quelqu’un d’autre.

Puis Entitlements::covers : chaque droit accordé doit avoir été demandé.

5.1 La comparaison des chemins est une égalité, pas une inclusion

Un octroi sur /var/lib/app n’est pas couvert par une demande sur /var, même si Landlock, lui, appliquerait le second au premier. La raison tient au sens de la vérification : on ne cherche pas si l’accord est applicable, mais si la machine a accordé quelque chose que le développeur n’avait pas écrit. Raisonner par préfixe demanderait de normaliser deux chemins — liens, ., //, encodages — et les divergences entre deux normaliseurs sont la source classique des contournements. L’égalité n’a pas de cas limite.

Conséquence assumée : l’émetteur d’octroi devra recopier les chemins du manifeste tels quels. C’est un travail d’outil, pas de jugement.

5.2 Les ports, eux, se comparent par inclusion

Un port accordé nommément est couvert par le même port demandé ou par un « n’importe quel port » demandé. L’inverse est refusé : accorder « n’importe quel port » quand trois ports étaient demandés est précisément l’élargissement que l’invariant existe pour attraper.

5bis. La signature (incrément 2)

L’étape 1 de l’arbitrage (ADR-150 D3) : établir qui présente un artefact. Sans elle, les deux étapes suivantes n’ont pas de sujet — chercher un octroi « pour cette identité » avant d’avoir établi l’identité, c’est évaluer un accord contre un inconnu, et c’est directement exploitable : remplacer le binaire, garder l’octroi.

Artefact détaché, binaire, domaine air.signature (BundleSignature). Ed25519.

5bis.1 Ce que la signature couvre : l’artefact complet

Enveloppe AIRCFGv1 comprise, pas le seul message Cap’n Proto qu’elle contient.

La raison est précise : l’enveloppe porte le schemaDomain. Signer le seul payload laisserait ré-envelopper les mêmes octets sous un autre domaine sans invalider la signature — donc présenter un octroi signé là où un manifeste est attendu, avec une signature parfaitement valide. Le checksum FNV de l’enveloppe ne s’y oppose pas : il détecte la corruption, pas l’adversaire.

Par transitivité, signer le manifeste couvre les binaires du bundle, puisque le manifeste porte leurs empreintes. Une seule signature suffit donc — à une condition qui doit être dite plutôt que sous-entendue : un exécutable absent du manifeste n’est couvert par rien.

5bis.2 L’étiquette de domaine, et pourquoi elle est indispensable

Le message signé est étiquette || SHA-256(artefact), avec deux étiquettes disjointes (air.bundle.manifest.v1\0, air.bundle.grant.v1\0 — l’octet nul garantit qu’aucune ne peut être le préfixe d’une autre, y compris celles qu’on ajoutera).

Sans elle, une signature produite sur un octroi vaudrait sur un manifeste. On pourrait croire que les clés distinctes suffisent — le développeur signe le manifeste, la machine signe l’octroi (D1). Mais rien n’oblige ces deux clés à différer : sur un poste où le développeur est aussi l’administrateur, ce sont les mêmes mains. La distinction ne peut donc pas reposer sur la clé ; elle doit être portée par le message signé lui-même.

5bis.3 Deux gardes, et ne pas les confondre

L’artefact déclare son sujet, et le vérificateur en attend un. Ce sont deux protections distinctes, et les confondre reviendrait à croire prouvée une chose qui ne l’est pas :

Le message signé est toujours reconstruit avec le sujet attendu, jamais avec celui que l’artefact déclare : un subject falsifié fait donc simplement échouer la vérification, au lieu de choisir l’espace de signature à la place du vérificateur.

5bis.4 Un refus au coût constant

Les deux conditions sont évaluées sans court-circuit (&, pas &&), et la vérification cryptographique est payée dans tous les cas. C’est la leçon d’ADR-150 D3 conséquence 1 : un refus qui coûte moins cher qu’un autre dit laquelle des conditions a échoué, et devient un canal auxiliaire.

5ter. L’émission (incrément 3)

5ter.1 Vérifier ne suffit pas — l’invariant est rendu inviolable

Grant::authorizes vérifie qu’un octroi ne dépasse pas la demande. C’est indispensable : il faut savoir juger un octroi qu’on n’a pas produit. Mais c’est une vérification a posteriori — elle suppose qu’un octroi excessif puisse exister, et se contente de le refuser au lancement.

issue ferme la porte plus tôt. Elle ne prend pas « ce qu’on accorde » : elle prend ce qu’on propose, et rend l’intersection avec ce que le manifeste demande. Quoi que propose l’administrateur — y compris n’importe quoi — l’octroi produit est un sous-ensemble de la demande par construction. Il n’existe aucun argument qui fasse sortir un octroi excessif de cette fonction.

C’est la différence entre « on vérifie que la règle est respectée » et « la règle ne peut pas être enfreinte ». Seule la seconde survit à un appelant distrait — et l’émetteur d’octroi sera un jour un outil d’administration écrit par quelqu’un d’autre.

La propriété est démontrée par property-based testing : pour toute demande et toute proposition engendrées, l’octroi émis est accepté par la vérification. Des cas choisis ne pourraient pas dire cela — ils diraient seulement que les cas auxquels l’auteur a pensé passent, ce qui est le contraire de ce qu’on veut démontrer d’une garantie par construction.

5ter.2 Ce que le property-based testing a trouvé

Une demande peut porter deux règles pour le même chemin. Laquelle fait foi ? Toutes les réponses sont mauvaises : prendre la première perd la seconde, l’union élargit ce que le développeur a écrit, l’intersection restreint sans le dire.

La réponse n’a pas été d’assouplir la propriété, mais de refuser l’ambiguïté à la source : un artefact qui déclare deux règles de même clé (chemin, service) est rejeté à la lecture. C’est l’invariant sur lequel intersect s’appuie pour rapprocher chaque règle demandée d’au plus une règle proposée.

Ce cas n’existait nulle part ailleurs dans les tests : il fallait un générateur pour le produire.

5ter.3 Une règle réduite à rien disparaît

Elle n’est pas rendue « à droits nuls » : elle est absente. Les deux ont le même effet, et la seconde ne laisse pas croire, à la relecture de l’octroi, qu’un accès a été accordé quelque part.

Corollaire qui a demandé de reformuler une propriété : « proposer la demande rend exactement la demande » est faux — une règle demandée sans aucun droit disparaît. La formulation juste est que proposer la demande donne l’octroi maximal : aucune autre proposition ne peut accorder davantage.

5ter.4 L’octroi s’encode, et c’est cet artefact que la machine signe

Grant::encode produit l’artefact complet — enveloppe AIRCFGv1 puis ConfigEnvelope portant le domaine air.grant. C’est cet artefact entier que la clé de la machine signe (§5bis.1). L’encodage est déterministe ([ADR-025]) : sans cela, l’empreinte d’un octroi n’aurait aucun sens et deux émissions identiques sembleraient différer.

5ter.5 La révocation n’a pas de mécanisme, et n’en aura pas

Elle est l’absence d’octroi (ADR-150 D3, conséquence 4). Retirer le fichier fait échouer l’étape 2 ; le binaire reste sur le disque, inerte.

5ter.6 Où vit l’octroi — ce qui est acquis, ce qui ne l’est pas

Acquis (D1) : hors du bundle, sur la partition inscriptible, émis à l’installation.

L’étude de placement (docs/notes/etude-administration-et-placement-configuration-fr.md §3.2/§3.4) donne le critère — « cette configuration décide-t-elle quel code s’exécute ? » — et l’octroi y répond oui. Il n’est pourtant pas plaçable dans l’image : installer une application demanderait alors une image nouvelle. Ce qui le protège est donc la composition de trois choses déjà décidées : il est signé par la machine, il n’est écrivable que par la porte d’administration, et l’étape 3 de l’arbitrage le plafonne par l’enveloppe de l’image.

Reste à fixer le chemin exact et la convention de nommage. Cette spec a d’abord annoncé que ce serait « un détail d’implémentation qui vient avec l’arbitrage » : la prédiction était fausse. L’arbitrage est venu (#655) et le chemin n’est toujours fixé nulle part — parce qu’il ne dépend pas de l’arbitre, qui reçoit un octroi, mais de la disposition sur disque d’ADR-010, qui n’est pas écrite. C’est une décision en attente, pas un reste mécanique.

5quater. L’arbitrage (incrément 4)

Trois étapes, dans cet ordre, et l’ordre est une condition de validité :

1. la signature du manifeste — établit qui ;
2. l’octroi valide pour cette identité — établit ce qui lui a été accordé ici ;
3. la conformité à l’enveloppe de l’image — établit si cet accord tient encore.

5quater.1 L’enveloppe est une entrée, pas un choix de l’arbitre

L’arbitre n’a pas besoin de connaître la largeur des enveloppes pour exister : il reçoit l’enveloppe. Ce qui manquait était une valeur, pas un mécanisme.

Cette valeur est depuis tranchée — question ouverte n° 1, option B (#657) : enveloppes filesystem écrites, familles sans applicateur vides par défaut, donc tout octroi qui les invoque est refusé explicitement plutôt que par omission. Le rapprochement enveloppe ↔ octroi n’est pas Entitlements::covers, contrairement à ce que cette section prévoyait : l’égalité stricte aurait exigé une image par application. Il se fait par gabarit — deux variantes typées (Exact, Subtree) plus un marqueur {bundleId}, aucun glob, et une comparaison composant par composant qui referme le piège "/vart".starts_with("/var"). Cette spec ne le décrit pas ; la description de référence est le module lui-même, crates/air-bundle/src/ceiling.rs.

5quater.2 Ce que l’étape 2 vérifie vraiment

Que l’octroi est signé par la machine, pas qu’il est « signé ». Vérifier la seconde chose sans la première laisserait n’importe qui fabriquer le sien : il lui suffirait d’émettre un octroi large et de le signer avec sa propre clé. La clé publique de la machine vient de l’image ; c’est une entrée de l’arbitrage.

5quater.3 L’altération est vue par la signature, pas par le checksum

On pourrait croire que le checksum de l’enveloppe attrape un artefact modifié. Il l’attrape — mais il ne protège rien : FNV-1a-64 n’est pas cryptographique, et n’importe qui le recalcule après avoir modifié l’artefact. Ce qui résiste à un adversaire est la signature, et l’ordre des étapes fait qu’elle parle la première. Un test le fixe, en « réparant » le checksum pour montrer que cela n’avance à rien.

5quater.4 Le refus est muet, et le type y veille

Refusal ne rend rien d’exploitable en s’affichant. Son motif ne s’obtient qu’en appelant for_journal(), dont le nom dit où il a le droit d’aller — un geste visible en relecture, là où un {refusal} distrait passerait inaperçu.

C’est la discipline d’ADR-150 D4 : un motif rendu au demandeur est un oracle d’énumération, il dit quelle condition il reste à satisfaire. Un test vérifie que trois causes très différentes rendent le même texte.

5quater.5 Une enveloppe rétrécie arrête un octroi jusque-là valide

C’est la conséquence 3 d’ADR-150 D3, et c’est voulu : l’image fixe le plafond, la partie mutable remplit dedans. Une mise à jour d’image peut donc empêcher une application de se relancer. Le motif de journal lui est propre (OutsideEnvelope) précisément pour que cela s’annonce au lieu de se découvrir.

5quater.6 L’enveloppe d’artefact est réimplémentée, et pourquoi

air-config-compile expose verify_checksum, et air-sshd s’en sert. Le lanceur ne peut pas : cette crate est un compilateur, elle embarque le lexeur et le parseur du format de source. Y faire entrer un parseur généraliste — même inutilisé — contredirait la décision qui structure tout ce chantier.

Le module envelope refait donc les trente lignes du format figé, et un test confronte les deux implémentations octet pour octet. air-config-compile reste une dépendance de test : le compilateur n’entre jamais dans le binaire livré.

6. Ce qui reste, et dans quel ordre

Cette table a menti jusqu’au 2026-08-12. Elle annonçait l’incrément 4 « à faire » et le 5 « bloqué » alors que les deux étaient mergés depuis le 10 août. Les incréments avançaient dans le code sans que la spec soit relue — la même classe de défaut que celle corrigée en #682, où un test annonçait son saut à un flux que personne ne lit.

Le mécanisme d’ADR-150 est complet. Ce qui reste (incrément 6) n’en est pas un morceau manquant mais son raccordement au disque, et ce raccordement suppose une décision que personne n’a prise : la disposition d’un bundle et l’emplacement d’un octroi. Mesure du manque, à cette date : spec.granted n’est renseigné que depuis les tests — aucun chemin de production ne mène du disque à un octroi arbitré.

7. Le codec texte, et pourquoi il n’ajoute pas de risque

ADR-150 D2 veut que le développeur rédige en texte et que le lanceur ne lise que le binaire. Les deux artefacts sont donc enregistrés comme domaines du registre (air-config-schema), ce qui les rend compilables par air-config-compile.

C’est l’inverse d’une facilité : écrire un parseur bespoke pour le manifeste aurait ajouté une seconde surface d’analyse syntaxique au voisinage d’une décision de privilèges, exactement ce que le Principe 11 cherche à éviter. Le parseur employé est celui qui existe déjà — borné (Limits), fuzzé, couvert à 100 % — et il vit hors de la porte d’exécution : son échec n’est qu’un refus de compilation, jamais une compromission.

Le format de source emploie le nom du champ tel qu’il est écrit dans le schéma (bundleId, pas bundle_id) : le binder est schema-directed et ne traduit aucune convention de nommage. C’est la règle de tous les domaines, pas une particularité d’ADR-150.

Ces domaines n’ont pas d’annotation $Air.backend : ils ne se projettent sur aucun fichier /etc. Le backend est documentaire et facultatif.

8. Preuves

• crates/air-bundle/src/tests.rs — 35 tests : lecture, bornes, chemins, identifiants, et l’invariant sous ses angles d’attaque (droit ajouté, chemin jamais demandé, port élargi, service AirCom voisin, octroi d’un autre bundle, manifeste réécrit, même bundle signé par un autre).
• crates/air-launchd/tests/garde_de_domaine.rs — la garde de domaine, prouvée mordante : la désarmer fait tomber deux tests sur quatre.
• crates/air-launchd/tests/codec_texte.rs — le chemin complet source → artefact → lecture validée, pour les deux domaines, plus le refus d’un domaine qui ne concorde pas et celui d’un champ inconnu.
• crates/air-config-schema/src/lib.rs — tout domaine déclaré doit s’instancier ; ce test rend vraie l’hypothèse que le compilateur traite comme structurellement acquise.
• crates/air-bundle/src/arbitrate/tests.rs — 15 tests. Le montage construit une chaîne cohérente puis chaque test casse un maillon et un seul : sans cela, une assertion ne dit pas quelle étape a rattrapé quoi.
• crates/air-bundle/src/envelope.rs — le verrou du duplicata d’enveloppe.
• crates/air-bundle/src/issue/tests.rs — 4 propriétés (proptest) + 9 cas nommés : aucune proposition ne produit un octroi excessif, l’intersection est idempotente, l’octroi maximal domine, l’aller-retour d’encodage, le déterminisme, et la boucle complète émettre → encoder → signer avec la clé machine → vérifier.
• crates/air-bundle/src/signature/tests.rs — 14 tests : les deux gardes du §5bis.3 séparément, le rejeu inter-domaines, l’octet d’enveloppe modifié, la signature d’un tiers, les longueurs exactes, une clé qui ne décode aucun point de courbe, un sujet hors schéma. La séparation cryptographique est prouvée mordante : rendre les deux étiquettes identiques fait tomber relabelling_a_signature_does_not_make_it_valid_elsewhere.

Licence du document : MPL 2.0