Construction sans réseau, vérifiée à chaque démarrage
Une sonde exécute une construction réelle : elle vérifie qu'aucune interface hors boucle locale
n'existe, qu'aucune route ne mène ailleurs et que la connexion TCP échoue. Si la sonde
réussit à sortir, le démon refuse de démarrer.
Zéro secret sur disque
Les clés de Previewd sont des identifiants systemd. Les secrets applicatifs vivent en
mémoire verrouillée et n'atteignent le conteneur que comme fichiers d'un ramfs
en lecture seule. Ni variable d'environnement, ni docker inspect, ni couche d'image.
Piste d'audit à chaîne de hachages
Chaque décision d'autorisation est écrite dans un journal append-only où chaque entrée
scelle la précédente. Previewd audit verify rejoue la chaîne ;
audit export produit une preuve lisible par un tiers.
Routage sans socket Docker
Traefik lit un unique dossier de fichiers de routes, en lecture seule, sans API ni
fournisseur Docker. Une image compromise ne peut pas fabriquer une route : elle n'a
aucun moyen d'en écrire une.
Un analyseur qui refuse ce qu'il ignore
Le contrôle du Dockerfile ne bloque pas une liste de choses dangereuses : il n'autorise
qu'une liste de choses comprises. Une directive ajoutée par une future version de Docker
devient un refus, pas une faille silencieuse.
La CI interdit la télémétrie
Un contrôle sur le binaire lié échoue si OpenTelemetry, gRPC ou un SDK cloud apparaît
dans les dépendances. Un second contrôle analyse le code et les fichiers de déploiement.
L'absence de fuite est mesurée, pas déclarée.
Sondes d'exfiltration réelles
La suite de bout en bout fait exécuter à une demande de fusion une connexion TCP et une requête DNS vers un écouteur de l'hôte : aucune ne doit aboutir. Une construction témoin, elle, doit l'atteindre — à défaut, le test ne démontrerait rien et échouerait.
Modèles formels et tests de propriétés
Onze configurations TLA+ couvrent la file, les approbations, le redémarrage, le TTL et
les workers. En parallèle, des tests par propriétés génèrent des millions de séquences
d'événements pour chercher une violation d'invariant — pas un exemple choisi à la main.
Redémarrage et panne, traités comme un risque
Au démarrage, un balayage inventorie ce qui tourne, détruit ce qui n'est plus gardé,
vérifie qu'aucune route n'oriente vers un environnement non gardé — et refuse de servir
si ce n'est pas le cas.