Anforderungen an die Sicherheitsschicht (REQ-SAF)

Umgesetzt in crates/railit-safety (Kanäle, Voter, Watchdog, sicherer Zustand; no_std, ohne Allokator) und crates/railit-runtime (Einbindung je Stellbereich, Journal). Nachweise in crates/railit-safety/tests/voter.rs, den Kani-Nachweisen (proofs.rs in railit-safety, railit-types, railit-rasta, railit-embedded), den Fuzz-Zielen (crates/railit-fuzz, fuzz/), den Szenarien 20 und 21, crates/railit-runtime/tests/ und apps/railitd/tests/api.rs.

ID	Anforderung	Gefährdung	Nachweis
REQ-SAF-001	Jeder Stellbereich kann in zwei Kanälen (2-von-2) rechnen: Derselbe Kern läuft mit eigenem Zustandsspeicher je Kanal. Weitergegeben werden die Ausgaben nur, wenn die Digests beider Kanäle (SHA-256 über Ergebnis, Stellbefehle, Ereignisse und – alle state_check_every Zyklen – den gesamten Zustand, plattformunabhängig kodiert) übereinstimmen; jede Abweichung führt in den sicheren Zustand. Mit fehlerfreien Kanälen verhält sich das Stellwerk genau wie mit einem.	H-001, H-007, H-015	healthy_channels_are_transparent, two_out_of_two_trips_on_stray_command, two_out_of_two_detects_state_divergence, Property-Test voted_outputs_are_reference_outputs_or_safe, all_scenarios_pass_with_three_channels, Kani voter_forwards_only_confirmed_outputs, Szenario 21
REQ-SAF-002	Mit drei Kanälen (2-von-3) entscheidet die Mehrheit: Ein überstimmter oder stillstehender Kanal wird ausgeschlossen, der Betrieb läuft als 2-von-2 weiter. Gibt es keine zwei übereinstimmenden Kanäle, folgt der sichere Zustand.	H-007, H-015	two_out_of_three_masks_one_channel, Property-Test voted_outputs_are_reference_outputs_or_safe, Kani voter_forwards_only_confirmed_outputs, redundant_channels_over_api, Szenario 20
REQ-SAF-003	Ein ausgeschlossener Kanal wird nur auf Anforderung wieder aufgenommen: Er übernimmt den gesamten Zustand eines gesunden Kanals und wählt ab dem nächsten Zyklus mit. Im sicheren Zustand ist keine Wiederaufnahme möglich. Die Wiederaufnahme steht im Journal.	H-007, H-015	two_out_of_three_masks_one_channel, journal_covers_trip_and_reset_of_the_safety_layer, redundant_channels_over_api, Szenario 20
REQ-SAF-004	Im sicheren Zustand der Schicht wird keine Ausgabe eines Kanals mehr weitergegeben. Die Schicht stellt allein aus dem Plan alle Signale auf Halt, schaltet Ersatzsignale aus, lehnt alle Anforderungen ab und versetzt die Kernzustände in den sicheren Zustand (safety_layer). Ein zu kleiner Ausgabepuffer führt ebenfalls dorthin. Rücksetzen ist ein Recht der Instandhaltung, wird protokolliert und wirkt wie ein Neustart des Bereichs (alle Elemente unbekannt). Abschaltung und Rücksetzen stehen im Journal; das Abspielen vergleicht davor und danach.	H-001, H-006, H-009, H-015	two_out_of_two_trips_on_stray_command, external_trip_holds_all_signals, output_overflow_trips, journal_covers_trip_and_reset_of_the_safety_layer, redundant_channels_over_api, roles_grant_their_permissions, Szenarien 20 und 21
REQ-SAF-005	Ein Watchdog überwacht je Bereich die Rechenzeit eines Zyklus und den Abstand der Zyklen anhand einer monotonen Uhr. Überschreitung, ausbleibende Zyklen und eine rückwärts laufende Uhr führen in den sicheren Zustand.	H-007, H-015	deadline_and_gap, backward_clock_trips_even_without_deadline, external_trip_holds_all_signals, Kani watchdog_detects_every_overrun, watchdog_trips_on_overrun
REQ-SAF-006	Zentrale Eigenschaften sind formal für alle Eingaben nachgewiesen (Kani, Bounded Model Checking) und werden in der CI geprüft: Voter (gibt nur bestätigte Ausgaben weiter, schaltet genau ohne Mehrheit ab), Watchdog, Ausgabepuffer (kein stiller Verlust), Bitmengen, Zeitarithmetik, MD4 und Prüfung beliebiger empfangener Bytes durch RaSTA (ohne Panik, Überlauf oder Zugriff außerhalb von Grenzen; die aufgebaute Verbindung prüfen Fuzzing und Property-Test), Paketierung der Telegramme des sicheren Rechners.	H-007, H-014	voter_forwards_only_confirmed_outputs, watchdog_detects_every_overrun, fixed_outputs_never_lose_silently, bitset_insert_remove_are_exact, bitset_union_is_exact, time_never_overflows, md4_never_panics_on_shortest_pdu, md4_never_panics_on_two_blocks, closed_connection_never_delivers, packer_respects_the_payload_limit
REQ-SAF-007	Alle Eingangsschnittstellen werden gefuzzt (libFuzzer, in der CI regelmäßig): Plan-Image (mit neu berechnetem Hash bis in Kern, Signalbilder und ETCS-Fahrerlaubnis jedes angenommenen Plans), rail-it-TOML und railML 3 (bis in die Projektierung), Fahrplan, Journal, RaSTA, EULYNX SCI, Binärprotokoll des sicheren Rechners. Dieselben Ziele laufen auf stabilem Rust mit Startkorpus, gezielten Veränderungen und Zufallseingaben.	H-004, H-008, H-014	seeds_pass, plan_mutation_sweep, truncated_sources, random_plan_mutations, random_bytes
REQ-SAF-008	Zyklische Speicherprüfung: Je Zyklus prüfen Knoten und Dienst (Kanäle im Prozess) einen Teil des Plan-Images im Speicher gegen die beim Laden festgehaltene Prüfsumme (4 KiB je Zyklus) und einen Teil eines eigenen RAM-Prüfbereichs mit einem Marsch-Test (Muster und Komplement, auf- und absteigend). Eine Abweichung führt in den sicheren Zustand (MemoryFault). Der Kernzustand selbst ist durch die getrennten Speicher der Kanäle und den Voter abgedeckt.	H-015	a_flipped_plan_bit_is_found_within_one_pass, intact_memory_passes_and_counts_passes, memory_check_finds_a_corrupted_plan