Wir greifen unseren eigenen Build bei jeder Änderung an

Hier ist eine unbequeme Frage an jeden Sicherheitstest: Ist er je fehlgeschlagen? Ein Test, der nie fehlgeschlagen ist, besteht vielleicht, weil das System in Ordnung ist, oder weil der Test überhaupt nichts sehen kann. Von außen sieht beides genau gleich aus.

Deshalb testet NoWayOS seine Sicherheit nicht nur. Es greift sie an, bei jeder Änderung, und prüft, dass die Angriffe aufgefangen werden.

Nach dem greifen, was einem nicht gehört

Jeder Teil eines NoWayOS-Systems läuft in seiner eigenen Kammer auf seL4 und hält nur, was ihm freigegeben wurde. Die Isolationstests schicken absichtlich Sonden über diese Grenzen. Eine liest eine Adresse, die ihr nie gegeben wurde. Eine schreibt auf eine Seite, die sie nur lesen darf. Eine, die genau das hält, was die Benutzeroberfläche hält, versucht, die Steuerseite der Anzeige zu beschreiben, die die Oberfläche nur lesen darf. Eine weitere, die genau das hält, was der Netzwerk-Client hält, versucht, in den Speicher des Netzwerktreibers zu schreiben.

seL4 muss jede einzelne stoppen, und ein unbeteiligter Teil muss unberührt weiterlaufen.

Ein Test, der fehlschlagen muss

Dann kommt die Wendung. Neben dem Isolationstest der Benutzeroberfläche steht eine Variante, bei der eine Freigabe absichtlich erweitert wurde: Der Stellvertreter der Oberfläche bekommt die private Seite der Anzeige. Der Test dieser Variante muss fehlschlagen. Würde er je bestehen, wäre der Isolationstest blind, und der Build würde es sagen.

Derselbe Gedanke zieht sich durch die übrigen Prüfungen. Jeder Decoder für Nachrichten zwischen den Teilen hat beschränkte Beweise aus dem Model Checker Kani, dass er nie in Panic gerät, nie überläuft und nie außerhalb der Grenzen liest. Mutationsprüfungen machen die Decoder dann absichtlich kaputt, um zu zeigen, dass die Beweise es merken. Jeder Parser für Eingaben von außen wird mit feindseligen Daten gefuzzt.

All das gehört zu make ci, dem Gate, das jede Änderung passieren muss. Die Isolationstests laufen jedes Mal; ein Beweis oder ein Fuzz-Lauf wird wiederholt, sobald sich der Code ändert, den er abdeckt.

Gates außer Reichweite

Ein Gate ist nur so stark wie die Hand, die es ändern kann. Deshalb sind die Prüfungen, die jeder Beitrag zu NoWayOS bestehen muss, in Defence Agent definiert, einem eigenen öffentlichen Repository. Ein Pull Request, der ein Gate berührt, wird für den Maintainer markiert.

Defence Agent testet sich selbst auf dieselbe Weise: zwanzig präparierte Pull Requests, von denen jeder etwas versteckt, das einem Reviewer entgehen könnte. Da ist versteckter Rechts-nach-links-Text in einem Kommentar, ein Buchstabe, der gegen sein kyrillisches Ebenbild getauscht wurde, eine Abhängigkeit, die direkt aus einem Git-Repository geholt wird, ein Workflow, der nicht vertrauenswürdigen Code ausführen würde. Jeder muss aufgefangen werden, während drei echte frühere Änderungen durchgehen müssen.

Nachweise statt Adjektive

Nichts davon macht ein Gerät “unhackbar”. Das tut nichts, und wir werden es nie sagen. Was Sie bekommen, sind Nachweise: ein Protokoll dessen, was versucht wurde, was gestoppt wurde, und der Befehl, der es zeigt. Lesen Sie die Nachweise eines echten Images oder die Gates selbst.