POLITECHNIKA GDAŃSKA WYDZIAŁ ELEKTRONIKI, TELEKOMUNIKACJI I INFORMATYKI Tadeusz Cichocki Metoda analizy bezpieczeństwa komputerowych systemów sygnalizacji kolejowej ROZPRAWA DOKTORSKA PROMOTOR: Prof. dr hab. inż. Janusz Górski Gdańsk, czerwiec, 2002 Metoda analizy bezpieczeństwa ... Stałe wsparcie szeregu osób umożliwiło mi wykonanie tej pracy. Szczególnie gorąco dziękuję za to prof. Januszowi Górskiemu, mojej żonie Annie oraz koleżankom i kolegom w firmie Bombardier Transportation (Zwus) Polska w Katowicach. Tadeusz Cichocki 1 / 183 Metoda analizy bezpieczeństwa ... Spis treści pracy 1. WSTĘP..................................................................................................................................................................1 1.1. BEZPIECZEŃSTWO SYSTEMÓW KOLEJOWYCH..................................................................................................1 1.2. CEL I TEZA ROZPRAWY.....................................................................................................................................1 1.3. STRUKTURA I ZAKRES PRACY..........................................................................................................................1 1.4. KONWENCJE NOTACYJNE PRZYJĘTE W PRACY.................................................................................................1 2. METODY ANALIZY BEZPIECZEŃSTWA SYSTEMÓW Z OPROGRAMOWANIEM........................1 2.1. ZAGROŻENIA I ICH PRZYCZYNY.......................................................................................................................1 2.2. METODA FMEA...............................................................................................................................................1 2.3. METODA FTA..................................................................................................................................................1 2.4. METODA HAZOP............................................................................................................................................1 2.5. METODY FORMALNE W ANALIZIE BEZPIECZEŃSTWA.......................................................................................1 3. BEZPIECZEŃSTWO SYSTEMÓW SYGNALIZACJI KOLEJOWEJ.......................................................1 3.1. ARCHITEKTURA SYSTEMÓW SYGNALIZACJI KOLEJOWEJ.................................................................................1 3.2. WZORCE PROJEKTOWE UKIERUNKOWANE NA BEZPIECZEŃSTWO....................................................................1 3.3. TECHNIKI ZWIĘKSZANIA WIARYGODNOŚCI KOMPONENTÓW PROGRAMOWYCH..............................................1 3.4. SAMOCZYNNA BLOKADA LINIOWA – PRZYKŁAD SYSTEMU SYGNALIZACJI.....................................................1 4. REGULACJE, NORMY I CERTYFIKACJA SYSTEMÓW KOLEJOWYCH..........................................1 4.1. WYMAGANIA PRAWNE DLA SYSTEMÓW SYGNALIZACJI KOLEJOWEJ...............................................................1 4.2. WYMAGANIA NORMATYWNE DLA SYSTEMÓW SYGNALIZACJI KOLEJOWEJ.....................................................1 4.2.1. Norma EN 50126 - kryteria dotyczące RAMS........................................................................................1 4.2.2. Norma EN 50128 - kryteria względem oprogramowania......................................................................1 4.2.3. Norma EN 50129 - kryteria dla pakietu bezpieczeństwa.......................................................................1 4.2.4. Inne normy...............................................................................................................................................1 4.2.5. Zakres analizy błędów i usterek..............................................................................................................1 4.3. PODSUMOWANIE..............................................................................................................................................1 5. FORMALIZACJA OPISU ARCHITEKTURY SYSTEMU...........................................................................1 5.1. MODELE KLAS I WSPÓŁPRACY SYSTEMU.........................................................................................................1 5.2. MODEL FORMALNY ZACHOWANIA SYSTEMU...................................................................................................1 5.2.1. CSP..........................................................................................................................................................1 5.3. ANALIZA SPÓJNOŚCI SPECYFIKACJI ARCHITEKTURY.......................................................................................1 5.3.1. Zakres analizy..........................................................................................................................................1 5.3.2. Automatyzacja analizy.............................................................................................................................1 6. WPROWADZENIE DO METODY OF-FMEA...............................................................................................1 6.1. CEL METODY....................................................................................................................................................1 6.2. MODEL USTEREK..............................................................................................................................................1 6.3. WZORCE MODELOWANYCH USTEREK..............................................................................................................1 6.4. PODSUMOWANIE..............................................................................................................................................1 7. OPIS METODY OF-FMEA................................................................................................................................1 7.1. KROKI METODY OF-FMEA.............................................................................................................................1 KROK 1: Wybór poziomów dekompozycji: poziomu referencyjnego analizy oraz poziomu bazowego komponentów.....................................................................................................................................................1 KROK 2: Analiza uszkodzeń dla poszczególnych komponentów.....................................................................1 KROK 3: Walidacja rodzajów uszkodzeń i wyselekcjonowanie tych, które zostaną poddane dalszej analizie ............................................................................................................................................................................1 KROK 4: Modelowanie rodzajów uszkodzeń....................................................................................................1 KROK 5: Eksperymenty iniekcji usterek...........................................................................................................1 KROK 6: Interpretacja uzyskanych wyników...................................................................................................1 KROK 7: Decyzje (akceptacja lub zmiany projektu systemu)..........................................................................1 7.2. PRAGMATYKA METODY OF-FMEA.................................................................................................................1 2 / 183 Metoda analizy bezpieczeństwa ... 7.2.1. Środowisko narzędziowe procesu OF-FMEA.........................................................................................1 7.2.2. Metoda OF-FMEA w procesie wytwórczym...........................................................................................1 8. STUDIUM PRZYPADKU: ANALIZA BEZPIECZEŃSTWA SYSTEMU LBS.........................................1 8.1. OPIS EKSPERYMENTU.......................................................................................................................................1 8.1.1. Cel eksperymentu.....................................................................................................................................1 8.1.2. Przedmiot i warunki eksperymentu.........................................................................................................1 8.2. OF-FMEA DLA LBS – KROK 1.......................................................................................................................1 8.3. OF-FMEA DLA LBS – KROKI 2-7...................................................................................................................1 8.4. OGÓLNE WNIOSKI Z EKSPERYMENTU...............................................................................................................1 9. ZAKOŃCZENIE..................................................................................................................................................1 9.1 PODSUMOWANIE WYNIKÓW PRACY..................................................................................................................1 9.1.1. Cel, teza i zakres pracy............................................................................................................................1 9.1.2. Wybory dokonane w trakcie pracy..........................................................................................................1 9.1.3. Oryginalne wyniki pracy.........................................................................................................................1 9.2. AKTUALNY STAN BADAŃ W DZIEDZINACH ZWIĄZANYCH Z PRACĄ.................................................................1 9.2.1. Analiza bezpieczeństwa i metodyka wytwarzania oprogramowania.....................................................1 9.2.2. Iniekcje usterek........................................................................................................................................1 9.2.3. Wspomaganie narzędziowe w procesie analitycznym............................................................................1 10. LITERATURA...................................................................................................................................................1 11. DODATKI...........................................................................................................................................................1 A. SŁOWNIK TERMINÓW.........................................................................................................................................1 B. WYKAZ AKRONIMÓW I OZNACZEŃ.....................................................................................................................1 C. PEŁNA SPECYFIKACJA SYSTEMU LBS................................................................................................................1 C.1. Dokumenty prawne, standardy i specyfikacje techniczne dotyczące systemów sygnalizacji kolejowej..1 C.2. Specyfikacja systemów sygnalizacji kolejowej według przepisów w Polsce............................................1 C.3. Wymagania bezpieczeństwa dla systemu blokady liniowej LBS...............................................................1 C.4. Modele architektury RAILWAY_SYSTEM.................................................................................................1 C.5. Formalna specyfikacja interakcji obiektów RAILWAY_SYSTEM............................................................1 D. NOTACJA CSP/FDR...........................................................................................................................................1 E. OPIS FDR I INSTALACJI......................................................................................................................................1 3 / 183 Metoda analizy bezpieczeństwa ... 1. WSTĘP Rozdział zawiera prezentację kontekstu pracy (p. 1.1), cel i tezę rozprawy (p. 1.2) oraz jej strukturę i zakres (p. 1.3). W p. 1.4 zawarto informację o zastosowanej notacji. 1.1. Bezpieczeństwo systemów kolejowych Rośnie zakres i różnorodność funkcji sterujących systemów, które są realizowane za pomocą oprogramowania. W przypadku systemów sterowania ruchem kolejowym poprawność realizacji tych funkcji decyduje o efektywnym przejeździe taboru przez szlaki i węzły kolejowe oraz o przeciwdziałaniu kolizjom i wykolejeniom pojazdów. Krytycznym czynnikiem w realizacji misji bezpiecznego zarządzania ruchem taboru kolejowego staje się złożoność modeli systemów z oprogramowaniem w ich środowisku działania, która przejawia się poprzez [HeH96], [Kur00], [EgM99]: • złożoną strukturę programów do celów sterowania ruchem kolejowym, • różnorodność interakcji programu i jego środowiska, • złożone scenariusze zdarzeń związanych z reakcją systemu na uszkodzenia jego komponentów, • dynamikę środowiska wykonania programów, • podatność na trudne do wykrycia błędy specyfikacji oraz zaburzenia kodu ze strony środowiska użytkowania (szczególnie „trudnego” środowiska kolejowego). W trakcie eksploatacji systemu kolejowego trzeba liczyć się z możliwością uszkodzeń jego elementów. Niektóre uszkodzenia prowadzą do zagrożeń (a niektóre z tych zagrożeń do wypadków), inne do przerwania usługi, a jeszcze inne nie zakłócą funkcjonowania systemu (są tolerowane). Bezpieczeństwo jest atrybutem jakości systemu [Lev86]. Bezpieczeństwo nie jest mierzone wartością absolutną [Lev95] i jest definiowane w odniesieniu do pojęcia ryzyka: bezpieczeństwo, to (w aktualnym stanie lub stale) brak nieakceptowanego poziomu ryzyka [Iso9000], [EN126]. Ryzyko jest definiowane jako funkcja zagrożeń. Zagrożenie (ang. hazard) jest rozumiane jako taki stan systemu lub procesu, który w połączeniu z określonym warunkiem w środowisku umożliwia wystąpienie zdarzenia prowadzącego do niepożądanych skutków. Dla danego zagrożenia ryzyko zależy od • możliwego zakresu strat związanych z wystąpieniem tego zagrożenia, oraz • wynikającej z działania i użytkowania systemu częstotliwości wystąpienia tego zagrożenia. Bezpieczeństwo jest więc definiowane w odniesieniu do zewnętrznych skutków: zniszczeń środowiska, zniszczeń dobytku materialnego, a szczególnie utraty zdrowia lub życia ludzi. W odniesieniu do komputerowych systemów sterowania ruchem kolejowym podstawowe wymaganie bezpieczeństwa można sformułować następująco [Acruda]: „Dowolne uszkodzenie kolejowego systemu sterowanego komputerowo musi prowadzić do takiego stanu systemu, aby będący w interakcji z nim tabor kolejowy przechodził do lub pozostał w stanie bezpiecznym.” Stan bezpieczny to taki stan, z którego nie jest możliwe bezpośrednie przejście do stanu zagrożenia. Sukces projektu dotyczącego systemu z wymaganiami bezpieczeństwa zależy w znacznym stopniu od: 4 / 183 Metoda analizy bezpieczeństwa ... • zastosowania adekwatnych mechanizmów przeciwdziałania usterkom, oraz • dowodu poprawności konstrukcji systemu i procesu jego tworzenia względem wymagań, przepisów i norm w dziedzinie bezpieczeństwa. Argumentacja na rzecz bezpieczeństwa polega więc na pokazaniu, w jaki sposób „wbudowano” je w system [Gór99r]. Kluczową częścią dowodu bezpieczeństwa systemu jest identyfikacja zagrożeń, ocena związanego z nimi ryzyka oraz analiza możliwości obniżenia tego ryzyka. Pojawienie się w systemach oprogramowania rodzi nowe problemy, a szczególnie w zakresie: • modelowania komponentów programowych, ich zależności i potencjalnych rodzajów uszkodzeń (defekty programowe są usterkami projektowymi), • koincydencji usterek programowych z dodatkowymi usterkami sprzętowymi, błędami użytkowników lub operatorów lub specyficznymi wpływami środowiska, • wyjaśniania wpływu komponentów programowych na ich środowisko, • braku ciągłości (małe zmiany programu mogą prowadzić do dowolnie dużych zmian w jego zachowaniu). Bezpośrednią przyczyną zagrożeń są w niemal wszystkich przypadkach [Lev00]: • niekompletne lub niepoprawne założenia o działaniu systemu sterowanego lub o wymaganym zachowaniu systemu sterującego, • niekompletna specyfikacja zachowania dla wszystkich stanów systemu i warunków środowiska, • brak kompletnej specyfikacji reakcji bezpieczeństwa systemu lub niewiarygodna jej implementacja, • specyfikacja zachowania komponentu, która prowadzi do zagrożeń z punktu widzenia całego systemu (w jego środowisku), • specyfikacja zachowania oprogramowania wbudowanego, która zawiera niezamierzone rozszerzenia (potencjalnie prowadzące do zagrożeń) w stosunku do specyfikacji wymagań. Redukcja złożoności oprogramowania może być osiągnięta przez jego reprezentację w postaci struktury obiektów [OMA] i projektowanie systemu drogą kolejnych uściśleń. Formalizacja przygotowanych modeli systemów ma na celu podniesienie ich precyzji i jednoznaczności. W metodach formalnych poszukuje się precyzyjnych i efektywnych technik opisu i analizy systemów. Formalne techniki weryfikacji składają się z trzech części [HuR99]: • ram pojęciowych i języka do modelowania systemów, • języka specyfikacji własności, które mają być implementowane i weryfikowane, • metody weryfikacji mającej na celu ustalenie czy opis systemu spełnia specyfikację. Potrzebna jest metoda identyfikacji i oceny ryzyka pozwalająca na podejmowanie decyzji, które zredukują ryzyko do dozwolonego minimum w ramach przewidzianych dla danego projektu ograniczeń kosztów i czasu. Decyzje te powinny dotyczyć zarówno walidacji specyfikacji wymagań dla komponentów systemu (w odniesieniu do struktury, w którą będą wbudowane) jak i gwarantowanej wiarygodności (ang. dependability) [AvL00] implementacji tych specyfikacji. Celem inżynierii bezpieczeństwa jest przeciwdziałanie tym wypadkom, które można przewidzieć oraz minimalizacja skutków wypadków nieprzewidzianych poprzez implementację wymagań norm, zastosowanie właściwych metod i technik analizy i projektowania, posługiwanie się dobrymi praktykami w zakresie struktur systemów i prowadzenia projektu. Główne i ustabilizowane zasady w inżynierii bezpieczeństwa są następujące [Sch98], [Lev95], [Gór90], [BaL01]: • bezpieczeństwo systemu powinno być rozważane z perspektywy określonego (całego) systemu, jego wpływu na środowisko, a nie z perspektywy wyróżnionych komponentów lub np. tylko oprogramowania, • bezpieczeństwo powinno być wbudowane w system przez stałe analizy w trakcie jego cyklu życia (zagrożenia powinny być identyfikowane i rozwiązywane możliwie najwcześniej), a nie dodane do tego systemu po zakończeniu etapów wytwarzania, 5 / 183 Metoda analizy bezpieczeństwa ... • analizy są istotnym rozszerzeniem dotychczasowych doświadczeń i standardów gdyż umożliwiają identyfikację szerokiej gamy zagrożeń, a szczególnie tych, które nie wystąpiły w dotychczasowych systemach, • w inżynierii bezpieczeństwa istotną rolę odgrywają podejścia jakościowe, gdyż eliminacja zagrożeń poprzez właściwą konstrukcję wymaga identyfikacji zagrożeń na możliwe najwcześniejszym etapie wytwarzania, gdy informacja ilościowa jeszcze nie istnieje lub jest nieprecyzyjna, szczególnie dla komponentów programowych lub nowych komponentów elektronicznych, • inżynieria bezpieczeństwa powinna mieć szerszy zakres niż tylko uszkodzenia komponentów i wynikające stąd skutki (nie tylko uszkodzenia komponentów generują zagrożenia), • wymagania bezpieczeństwa mogą być w konflikcie z innymi wymaganiami (np. dostępnością). 1.2. Cel i teza rozprawy Celem rozprawy jest opracowanie metody analizy bezpieczeństwa systemów komputerowych stosowanych do sterowania ruchem kolejowym. Z rozprawą wiąże się teza, sformułowana następująco: Zintegrowane podejścia: modelowanie obiektowe, modelowanie i analiza formalna oraz analiza klas i skutków usterek umożliwiają efektywną analizę bezpieczeństwa komputerowych systemów sterowania ruchem kolejowym. Cel ten osiągnięto przez zaproponowanie metody OF-FMEA (ang. Object-oriented Formal FMEA), która wykorzystuje i integruje: • metodę modelowania obiektowego UML (ang. Unified Modelling Language), • metodę formalnej specyfikacji zachowania systemów CSP (ang. Communicating Sequential Processes), • metodę analizy skutków uszkodzeń FMEA (ang. Failure Mode and Effect Analysis), oraz stosuje programowe narzędzie analityczne FDR1 (ang. Failures Divergence Refinement) do wspomagania procesu analizy formalnej. Metoda OF-FMEA umożliwia modelowanie i analizowanie skutków uszkodzeń systemów, których komponenty są zrealizowane przez oprogramowanie. Do specyfikowania i analizy systemu metoda OF-FMEA wykorzystuje aparat formalny i w ten sposób zapewnia wysoką precyzję specyfikacji i pewność odnośnie wyników analiz. Analizy są w znacznym stopniu zautomatyzowane (poprzez wykorzystanie narzędzia FDR) i dzięki temu metoda jest możliwa do zastosowania w stosunku do nietrywialnych przypadków. W celu potwierdzenia stosowalności i skuteczności metody OF-FMEA zastosowano ją w stosunku do rzeczywistego systemu dotyczącego sterowania ruchem kolejowym. Zrealizowane studium przypadku dotyczyło systemu blokady liniowej LBS (ang. Line Block System) i zostało przygotowane na podstawie rzeczywistego systemu sygnalizacji kolejowej budowanego w firmie Bombardier Transportation (Zwus) Polska Sp. z o.o. w Katowicach. 1 Sponsorem licencji na oprogramowanie FDR (por. Dodatek E) do celów badawczych w Katedrze Zastosowań Informatyki na Wydziale ETI Politechniki Gdańskiej była firma Bombardier Transportation (Zwus) Polska Sp. z o.o. (dawniej: Adtranz Zwus Sp. z o.o.) w Katowicach. 6 / 183 Metoda analizy bezpieczeństwa ... 1.3. Struktura i zakres pracy Na rys. 1. przedstawiono diagram reprezentujący zakres tematyczny oraz strukturę niniejszej pracy. Diagram ten został wyrażony z pomocą notacji UML [BoR99]. Praca Teza i jej kontekst Rozdział 1: Wstęp Rozdział 2: Metody analizy bezpieczeństwa systemów z oprogramowaniem Rozdział 3: Bezpieczeństwo systemów Prezentacja problemu sygnalizacji kolejowej Rozdział 4: Regulacje, normy i certyfikacja systemów kolejowych Rozdział 5: Formalizacja opisu architektury systemu Prezentacja Rozdział 6: Wprowadzenie do metody rozwiązania problemu OF-FMEA Rozdział 7: Opis metody OF-FMEA Rozdział 8: Studium przypadku: analiza bezpieczeństwa systemu LBS Walidacja i ocena zaproponowanego rozwiązania Rozdział 9: Zakończenie {Zawarto w nich dodatki uzupełniające prezentację: • słownik terminów, Literatura • wykaz akronimów i oznaczeń, • pełną specyfikację LBS, • opis notacji CSP, Materiały pomocnicze • opis narzędzia FDR} Rysunek 1. Struktura pracy wyrażona w notacji UML. 7 / 183 Metoda analizy bezpieczeństwa ... 1.4. Konwencje notacyjne przyjęte w pracy W pracy zastosowano notację UML (ang. Unified Modelling Language) w dwóch obszarach: do opisu systemów modelowanych i analizowanych za pomocą zaproponowanej metody OF-FMEA oraz do opisu samej metody i niektórych elementów dotyczących niniejszej pracy. Ponieważ środki modelowania UML wykorzystywane w pracy są obecnie powszechnie znane w środowiskach informatycznych, zrezygnowano z zamieszczania w pracy ich opisu. Zainteresowany czytelnik może sięgnąć np. do [UML1] lub [BoR99]. W prezentowanych w p. 8.2 i p. 8.3 kartach eksperymentów przyjęto następujące konwencje oznaczeń: • W – wsadowy tryb przebiegu FDR • I – interaktywny tryb przebiegu FDR • (cid:57) – asercja jest spełniona • ו – asercja nie jest spełniona (i znaleziony został kontrprzykład). Pozostałe konwencje notacyjne zostały przedstawione w Dodatkach zamieszczonych w pracy: • Słownik terminów jest zawarty w Dodatku A i (w zakresie terminów kolejowych) Dodatku C.2. • Wykaz akronimów i oznaczeń jest zawarty w Dodatku B. • Słownik danych modeli systemu LBS jest zawarty w Dodatku C.4. • Zestawienie wyjaśnień do elementów notacji CSP/FDR zawiera Dodatek D. 8 / 183 Metoda analizy bezpieczeństwa ... 2. METODY ANALIZY BEZPIECZEŃSTWA SYSTEMÓW Z OPROGRAMOWANIEM Kluczowym problemem projektu rozwojowego dla systemu związanego z bezpieczeństwem jest ustalenie i interpretacja (por. [EN126]): • wymagań bezpieczeństwa oraz • czynników, które mogą prowadzić do ich niespełnienia w projekcie lub do ich naruszenia w zrealizowanym systemie. Wśród wspomnianych czynników są usterki, które mogą być wygenerowane w systemie lub w jego środowisku. Wymagania bezpieczeństwa nie mogą być naruszone nawet w przypadku wystąpienia zdefiniowanych klas usterek. Analiza bezpieczeństwa ma na celu ustalenie wymagań bezpieczeństwa oraz wykazanie, że system pozostaje bezpieczny nawet w sytuacjach wystąpienia określonych klas usterek. Środowisko dla analizy bezpieczeństwa przedstawiono na Rys. 2. Środowisko dla analizy bezpieczeństwa Struktura organizacyjna projektu i dokumentacji Procedura zarządzania ryzykiem Procedury zapewniania przedsięwzięcia jakości Standardy i przewodniki Procedury zarządzania projektem Biblioteka {and} dokumentacji Specyficzne dla projektu projektu szablony dokumentów {w tym dostępna Przygotowane {w tym instalacja wiedza o usterkach} modele Narzędzia oprogramowania architektury systemu wspomagające analitycznego} Przeszkolenie uczestników projektu w zakresie celów i przebiegu analizy oraz elementów jej środowiska Rysunek 2. Struktura środowiska dla analizy bezpieczeństwa. W kolejnych punktach tego rozdziału omówimy podstawowe metody analizy bezpieczeństwa systemów z oprogramowaniem praktykowane lub rekomendowane dla projektów rozwojowych w dziedzinie systemów kolejowych. 9 / 183