Stan zagrożeń w internecie znajduje się obecnie na poziomie standardowym. Nie występują duże epidemie a eksperci z Kaspersky Lab nie zanotowali żadnych poważnych incydentów związanych z bezpieczeństwem. Poziom zagrożenia: 1

Potęga V&V

Dodany 23 listopada 2015, 11:33 CET
Tagi:

Bezpieczny system – zwłaszcza taki, który jest wykorzystywany do zapewniania bezpieczeństwa – musi budzić zaufanie. Na czym jednak opiera się to zaufanie? Jaki mamy dowód na to, że główne komponenty naszego zaufanego systemu zostały właściwie zaimplementowane i nie zawiodą w krytycznym momencie? Wspominaliśmy o tym w naszym ostatnim artykule dotyczącym bezpiecznego systemu operacyjnego i – zgodnie z obietnicą – wracamy do tego zagadnienia.

Celem weryfikacji i walidacji (V&V) jest zapewnienie, że oprogramowanie (czy też cały system lub urządzenie) rzeczywiście posiada określone cechy. Chociaż terminy te (V&V) brzmią dość podobnie i są wykorzystywane w połączeniu ze sobą, posiadają dość odmienne znaczenie. Podsumujmy:   

Weryfikacja to proces służący określeniu, czy wynik danego etapu rozwoju produktu (tj. rozwoju oprogramowania) spełnia ściśle wymagania postawione na początku etapu.

Walidacja to proces, którego celem jest ustalenie, czy produkt (program komputerowy, system operacyjny, aplikacja itd.) jest zgodny z założeniami dotyczącymi użycia oraz spełnia potrzeby użytkownika. Wymagania, procesy w ramach cyklu życia oraz inne pomocnicze artefakty również mogą zostać poddane walidacji w celu sprawdzenia ich zgodności z oczekiwanymi wynikami.

Upraszczając, w weryfikacji zostaje zadane pytanie: „Czy poprawnie zaimplementowaliśmy system?”, natomiast w walidacji pytanie brzmi: „Czy zaimplementowaliśmy poprawny system?” O ile drugie pytanie wymaga udziału eksperta (którego opinia tworzy podstawę całego wachlarza problemów dotyczących walidacji, od walidacji wymogów po ostateczny test integracji), na pierwsze należy odpowiedzieć przy użyciu metod formalnych.  

A zatem, jedno nie może istnieć bez drugiego. System może zostać zweryfikowany tylko w odniesieniu do określonej właściwości, np. dowodu, że w programie nie wystąpiły zakleszczenia. Walidacji należy poddać fakt, że ta właściwość ma sens. Ponadto, weryfikację można przeprowadzić w prosty sposób poprzez ograniczenie możliwości blokowania zasobów – to może jednak zaburzyć integralność tych zasobów. Dlatego też należy dokonać walidacji dodatkowego warunku. W niektórych przypadkach, definicja właściwości również może być przedmiotem weryfikacji, jeśli wymagania eksperta mogą zostać odpowiednio sformalizowane do celu weryfikacji.   

vv_article_eng_1_auto.jpg

Aby zrozumieć proces weryfikacji, spróbuj wyobrazić sobie „magicznego testera”, który jednym kliknięciem może ocenić dowolny kod źródłowy: czy kod jest prawidłowy czy nie? Jest bezpieczny czy nie? I tak dalej. Jednak nawet tak idealny model wzbudza wiele pytań. Pierwsze z nich brzmi: co tak naprawdę udowodnimy? Jakie twierdzenia mogą zostać udowodnione poprzez weryfikację? Poprawność, kompletność, spójność danych, dokładność  bezpieczeństwo wykonania…Wykazano, że wszystkie te właściwości mogą być reprezentowane jako połączenie dwóch podstawowych właściwości – właściwości „bezpieczeństwa” oraz właściwości „żywotności”. Właściwość bezpieczeństwa zakłada, że system nie może osiągnąć określonego stanu (brak bezpieczeństwa). Innymi słowy, to oznacza, że „nigdy nie zdarzy się nic złego”. Z kolei właściwość żywotności gwarantuje, że po określonym przebiegu system osiągnie określony stan – innymi słowy, „z pewnością zdarzy się coś dobrego”.  

Jednak świadomość możliwości dekompozycji celu weryfikacji to jedno, a poprawna i ważna reprezentacja takiego zdekomponowanego celu bez utraty sensu to, najwyraźniej, drugie. Niekiedy, próba dekompozycji reguły dla modelu systemu przynosi negatywny wynik: model pozostaje w obszarze „bezpieczeństwa” reguły, nie mogąc ustanowić części „żywotności”. To narzuca procesowi dekompozycji dodatkowe warunki. W innych realistycznych scenariuszach, oprócz bezpieczeństwa i żywotności należy dodatkowo uwzględnić „właściwość słuszności” (jak w prawdziwym życiu).    

vv_article_eng_21_auto.jpg

W celu sformalizowania tak zdefiniowanych kryteriów często stosowana jest logika klasyczna lub temporalna, natomiast w celu weryfikacji właściwości systemu zgodnie z tymi kryteriami – odpowiednie języki programowania. W szczególności, w przypadku zdań logiki klasycznej, dość popularny jest Prolog, podczas gdy w przypadku logiki temporalnej, wykorzystywane są języki Promela oraz SPIN. Jednak, nie jest to jedyny sposób definiowania celów weryfikacji. Formalne określenie poprawnego zachowania programu oraz weryfikacja tego zachowania jest tak specyficzna i tak istotna, że w 1969 r. informatyk i logik C. A. R. Hoare zaproponował formalną teorię, której celem było określenie poprawności programów komputerowych w sposób dedukcyjny. Podstawą tej teorii jest zestaw reguł logicznych określanych w sposób imitujący semantykę imperatywnych konstrukcji językowych. Później zostało opracowane podejście do specyfikacji kryteriów, które jeszcze bardziej przypomina abstrakty programowania oraz obsługuje dalsze tworzenie oprogramowania – programowanie oparte na kontrakcie.      

Kolejnym istotnym problemem jest wybór obiektu weryfikacji. Mimo że procedura weryfikacji implikuje dokładną ewaluację, należy dokonać właściwego wyboru obiektu, aby mieć zaufanie do wyniku.  

Na przykład, do weryfikacji można wybrać statyczną konfigurację systemu – tj. parametry systemu, aplikacje i ograniczenia polityki bezpieczeństwa. Tester przyjmuje te dane, wykonuje procedury weryfikacji zgodnie z zasadami logiki (w oparciu o wiedzę ekspercką) i generuje wynik „zaliczył” lub „nie zaliczył”. Tester może np. ocenić, czy możliwy jest określony rodzaj ataku na system lub czy użytkownik nie posiadający przywilejów może uzyskać nieautoryzowany dostęp do określonych zasobów w systemie itd.      

Weryfikacja konfiguracji systemu może potwierdzić, że zachowanie systemu jest zaufane, jeśli jego komponenty są poprawnie skonfigurowane. To oznacza, że wszystkie usługi oraz aplikacje systemu powinny działać tak, jak określono, i nie zawierać żadnych błędów lub luk w zabezpieczeniach, które mogą zostać wykorzystane i wpłynąć na funkcjonowanie całego systemu.

Jednak, w rzeczywistości sytuacja ta często wygląda inaczej. Dlatego należy zweryfikować wewnętrzne komponenty oprogramowania. W tym punkcie jedno jest jasne – ponieważ wewnętrzne komponenty oprogramowania posiadają wiele warstw reprezentacji, po raz kolejny pojawia się konieczność dokonania właściwego wyboru. Jaki obiekt należy zweryfikować – kod źródłowy wysokiego poziomu czy sekwencje instrukcji maszynowych? Czy należy uwzględnić środowisko programów oraz jak modelować to środowisko? Czy zbadanie określonych zależności wykonania na niskim poziomie z platformy sprzętowej ma jakąkolwiek wartość…? Ponownie, wybór zależy m.in. od celu weryfikacji. Przypuśćmy, że chcesz mieć pewność, że oprogramowanie nie zawiera określonego rodzaju luki (przykład ten można interpretować w większości przypadków jako wspomniany wyżej problem bezpieczeństwa). Testy i statyczna analiza kodu, których celem jest znalezienie typowych zagrożeń, zwykle nie są uważane za formalne metody weryfikacji ze względu na to, że nie obejmują wszystkich możliwych sytuacji (chociaż istnieją wyjątki). W celu rozwiązania tego problemu metody weryfikacji należy wykonać obliczenia logiczne, aby wykazać, że dowolny fragment ciągły na wykresie przebiegu programu (w tym wszystkie przejścia nielinearne) nie jest podatny na daną metodę wykorzystywania. Wszystko, co trzeba zrobić, to sformalizować, w ogólny sposób, odpowiednie ważne warunki oraz zaimplementować skuteczne algorytmy ewaluacji dla całego kodu programu.      

Problem dodatkowo komplikuje brak gwarancji, że kompilator zapisze udowodnione właściwości dla uzyskanego kodu maszynowego, oraz konieczność zagwarantowania właściwości określonych pierwotnie dla kodu niskiego poziomu. To właśnie ze względu na tę złożoność weryfikacji kodu programu metody weryfikacji są stosowane w odniesieniu do kodu w możliwie najprostszy i najkrótszy sposób. Priorytet ma kod jądra systemu operacyjnego oraz kod usług niskiego poziomu, który leży u podstaw bezpieczeństwa całego systemu. 

vv_article_eng_31_auto.jpg

Jednym z obiecujących podejść do weryfikacji jest gwarantowanie bezpieczeństwa niektórych właściwości kodu (lub stworzenie podstawy takiej gwarancji) podczas tworzenia takiego kodu. Wykazując, że zapis lub język programowania potrafi nadać niezbędne cechy kodu programu, można uniknąć żmudnych procedur sprawdzania przynajmniej dla tych właściwości. Generowanie kodu minimalizuje błędy człowieka (tzw. bugi) podczas tworzenia kodu oprogramowania. Jest to dość skuteczne podejście, stosowane obecnie jedynie w przypadku ograniczonej liczby algorytmów w określonym kontekście – przynajmniej do czasu rozwiązania kolejnego bardziej skomplikowanego zadania. Zadanie to pojawia się dlatego, że nie eliminujemy kwestii weryfikacji kodu, ale zamiast tego przekazujemy ją na wyższy poziom – poziom weryfikacji języka (lub kompilatora). Dlatego też musimy zweryfikować czy język jest bezpieczny, czyli czy wszystkie konstrukcje stworzone przy użyciu tego języka są bezpieczne we wcześniejszym znaczeniu. Nie jest to błahe zadanie, wystarczy jednak, że zostanie raz wykonane, aby rozwiązać kwestie weryfikacji dla dowolnego kodu stworzonego przy użyciu ocenianych wcześniej metod.      

Kolejną metodą implementacji weryfikalności kodu programu podczas tworzenia jest zastosowanie podejścia programowania opartego na kontrakcie. W tym przypadku, implementacja rozpoczyna się od określenia dokładnych specyfikacji formalnych programowania interfejsów, które określają warunki wstępne (zobowiązania przyjęte przez klientów interfejsów), warunki końcowe (zobowiązania przyjęte przez dostawcę interfejsu) oraz niezmienne (zobowiązania dotyczące zapisu pewnych właściwości związanych z interfejsem). Wiele języków programowania obsługuje programowanie oparte na kontrakcie w sposób natywny lub przy pomocy rozszerzeń zewnętrznych producentów (np. języki C oraz Java).

„Weryfikacja laboratoryjna” kodu programu może prowadzić do skarg, jeśli na zachowanie kodu w dużej mierze ma wpływ środowisko. Naturalnie, byłoby dobrze, gdyby system złożony z luźnie połączonych ze sobą zaufanych komponentów z odpowiednio zdefiniowanymi interfejsami mógł zapewnić 100% gwarancję, że będzie działał poprawnie, jednak w rzeczywistych systemach dość trudno jest przewidzieć, jaki wpływ na poszczególne komponenty będzie miało środowisko. Aby ocenić poprawność systemu, należy zastosować analizę zachowania równoległych komponentów. Formalną weryfikację tego, czy dany wzór logiczny jest odpowiedni dla systemu z paralelną architekturą wykonania określa się jako sprawdzanie modelu. Metoda ta łączy aktualną wiedzę i doświadczenie w zakresie weryfikacji oprogramowania i jest powszechnie wykorzystywana na całym świecie do oceny aktualnych systemów sprzętowych i oprogramowania. Wyróżnienie Turing Award zostało przyznane dwukrotnie za pracę w dziedzinie sprawdzania modeli. Pierwsze wyróżnienie przyznano w 1996 r. Amirowi Pnueli „za owocną pracę nad wprowadzeniem logiki temporalnej do informatyki oraz za wybitny wkład w dziedzinie weryfikacji programów oraz systemów” . Drugie wyróżnienie przypadło w 2007 r. trzem naukowcom: Clarke’owi, Emersonowi oraz Sifakisowi „za ich udział w rozwinięciu Model-Checking w niezwykle skuteczną technologię weryfikacji, która jest powszechnie wykorzystywana w branży sprzętu i oprogramowania”.       

Podczas ceremonii Turing Award w 2007 r. przewodniczący ACM Stuart Feldman tak wyraził się o metodzie sprawdzania modeli: „Jest to doskonały przykład technologii przeobrażającej branżę, która powstała na gruncie wysoce teoretycznych badań”. Z pewnym przekonaniem możemy stwierdzić, że jeśli przyszłość wszelkich aspektów naszego życia zależy od technologii, które są bezpieczne i inteligentne w każdym znaczeniu tego słowa, metody walidacji i weryfikacji wskazują drogę ku tej przyszłości.  

Nie jest możliwe przyjrzenie się wszystkim aspektom V&V w jednym artykule. Tym, którzy są szczególnie zainteresowani tematem, polecamy pracę autorstwa jednego z pionierów podejścia „model checking”, Edmunda M. Clarke’a, pt.: „The Birth of Model Checking”, oraz jego książkę „Model Checking”, napisaną wspólnie z Orna Grumbergiem i Doronem A. Peledem, w których metoda ta została zbadana w bardziej szczegółowy sposób. Najlepszym sposobem poznania aspektów bezpieczeństwa, żywotności oraz innych głównych właściwości jest odwołanie się do oryginalnych prac wyszczególnionych w artykule autorstwa Ekkarta Kindlera pt. „Safety and Liveness Properties: A Survey”. Rewelacyjna monografia autorstwa G. Tela pt. „Introduction to distributed algorithms” szczegółowo wyjaśnia formalną reprezentację i rozwój poprawnych i zależnych algorytmów w złożonych systemach.