Automatyczna symboliczna weryfikacja programów i protokołów kryptograficznych w systemach rozproszonych

Cel naukowy

Weryfikacja modelowa (ang. model checking) jest uważana za jedno z najbardziej spektakularnych zastosowań informatyki teoretycznej w praktyce programistycznej. Poprawność danego systemu rozproszonego, programu współbieżnego, bądź też protokołu kryptograficznego względem podanej specyfikacji jest najważniejszą kwestią, która musi być rozstrzygnięta zanim trafi on do masowej eksploatacji. Ewentualne błędy w programach kontroli lotów (np. przypadek rakiety Ariane 5), kontroli jakości, obsługi urządzeń do radioterapii, czy też w działaniu procesora (przypadek modułu dzielenia procesora Pentium) mogą mieć tragiczne skutki zarówno w sferze finansowej, jak też dla zdrowia i życia ludzi. Wiadomo, że przetestowanie programu dla dowolnej liczby danych nie zagwarantuje, że program będzie się zachowywał prawidłowo dla innego zbioru danych. Metody aksjomatyczne, użyte w celu dowiedzenia poprawności, wymagają olbrzymiego wkładu pracy człowieka, który jednak także może popełnić błąd. Nie dają zatem całkowitej gwarancji. Pełne gwarancje może dać tylko zastosowanie metody automatycznej, to znaczy innego programu, który sprawdzi czy testowany program spełnia podaną specyfikację. Sam program testujący, który zazwyczaj nie jest bardzo duży, jest sprawdzany wszystkimi dostępnymi metodami. Weryfikacja modelowa jest najważniejszą klasą metod automatycznej weryfikacji. Główna idea polega na przedstawieniu (lub zakodowaniu) programu jako automatu (ogólniej: systemu tranzycyjnego), którego stany (osiągalne) stanowią badany model i przedstawieniu (zakodowaniu) specyfikacji jako formuły logicznej. Sprawdzane jest algorytmicznie czy formuła jest prawdziwa w modelu. Może to być dokonane wieloma metodami: bezpośrednio, symbolicznie, bądź też poprzez skonstruowanie automatu, który akceptuje wszystkie modele dla danej formuły i sprawdzenie, czy akceptuje również model zadany przez program. Takie metody są stosowane w działach ds. weryfikacji największych firm informatycznych jak Microsoft, Intel, AT&T, Motorola i inne. Jednocześnie niektóre kraje, np. Francja, wprowadzają obowiązek formalnej weryfikacji systemów i oprogramowania mającego krytyczne zastosowania (np. obsługa elektrowni jądrowych). Dlatego uważamy, że takie metody muszą być też rozwijane i implementowane w Polsce. Jest kwestią niedalekiej przyszłości, kiedy wymóg formalnej weryfikacji będzie dotyczył niektórych systemów i krytycznego oprogramowania opracowywanego również w Polsce (jako kraju członkowskim Unii Europejskiej).

Głównym problemem występującym w automatycznej weryfikacji jest wykładnicza eksplozja liczby stanów modeli. Dla potrzeb weryfikacji systemów współbieżnych zostały opracowane różne metody, które istotnie ograniczają rozmiary przestrzeni stanów. Oczywiście metody te są dostosowane do używanych języków specyfikacji, tzn. języków logik (temporalnych, czasowych, epistemicznych), w których wyrażane są weryfikowane własności. Praktyka weryfikacji pokazuje jednak, że metody symboliczne bazujące na BDD (boolowskich diagramach decyzyjnych) lub SAT (testowaniu spełnialności formuły zdaniowej) są najczęściej wykorzystywane w przypadku systemów o wielkich przestrzeniach stanów, tzn. rzędu 10²⁰ i większych.

Cele projektu

Cele projektu można podzielić na bezpośrednie i perspektywiczne. Cele bezpośrednie są następujące:

Opracowanie nowych metod automatycznej weryfikacji modelowej programów napisanych w językach wysokiego poziomu Promela, Timed-UML i Java

Opracowanie nowych metod bazujących na końcowej translacji do SAT uzupełnione będzie adaptacją i integracją (dla tych metod) różnych technik prowadzących do redukcji przestrzeni stanów [JJ04,Min99,GKPP99], zarówno na etapie translacji z języka wysokiego poziomu, jak również na etapie samej weryfikacji modelowej. Promela [Hol91,Ho97,BD98] jest uznanym językiem do specyfikacji protokołów komunikacyjnych i systemów rozproszonych oraz językiem wejściowym dla narzędzia SPIN [Hol97], rozwijanego w AT&T. Timed-UML [GOO04] staje się standardem w specyfikacji systemów rozproszonych i jest językiem wejściowym dla narzędzia IF [BFG+99,BFG+99a]. Protokoły i biblioteki napisane w Javie są od dawna przedmiotem zainteresowania badaczy w NASA [Hav00]. W szczególności programy obsługi sond marsjańskich implementowane są w języku Java [HR01].

Rozszerzenie implementacji systemu VerICS, w którym będą zrealizowane nowe translacje oraz techniki weryfikacji zaproponowane powyżej

Zaimplementowany system będzie umożliwiać zastosowanie symbolicznych metod weryfikacji, bazujących na translacji do SAT i SAT-testerach [WPZ03,Str00,McM03,SLB03], do programów napisanych w językach wysokiego poziomu. Planujemy opracowanie nowej metody dyskretyzacji dla sieci automatów czasowych, gdzie dozwolone są nierówności dotyczące różnic na zegarach. Ponadto opracujemy moduł nieograniczonej weryfikacji modelowej (UMC), realizujący translację problemu poprawności programu do spełnialności formuły zdaniowej [KLP04,KP04] oraz optymalizacje dla UMC i ograniczonej weryfikacji modelowej (BMC). Jako języka specyfikacji użyjemy fragmentów języka TCTL, tzn. czasowej wersji CTL.

Opracowanie nowych metod weryfikacji protokołów kryptograficznych i ich implementacja jako modułu systemu VerICS

Planujemy opracowanie narzędzi do weryfikacji poprawności i systematycznego konstruowania protokołów kryptograficznych, tzn. protokołów umożliwiających wiarygodne (bezpieczne) przesyłanie, przetwarzanie i przechowywanie informacji w sieciach teletransmisyjnych. Algorytmy i protokoły kryptograficzne stały się przedmiotem szerokiego zainteresowania w ostatnich latach, od kiedy media elektronicznego porozumiewania się zyskują atrybut powszechności. Niezbędność zapewnienia dyskrecji, poufności czy tajności, a także wiarygodnego potwierdzania tożsamości porozumiewających się stron w wielu sytuacjach jest zrozumiała, na przykład w przypadku komercyjnych negocjacji lub transakcji finansowych dokonywanych drogą elektroniczną. Gwałtowny wzrost dostępności do mediów elektronicznych poprzez rozległe sieci teleinformatyczne umożliwia dziś, a nawet wymusza, masową skalę elektronicznego handlu, bankowości, itp. W niektórych sektorach trudno już w ogóle wyobrazić sobie funkcjonowanie bez sieci takich jak Internet. Tymczasem ciągle poważne wyzwanie natury technologicznej, pomijając zagadnienia prawne, stanowi wiarygodność i poprawność algorytmów i protokołów (oraz ich implementacji), zabezpieczania poufności, tajności, niepodrabialności dokumentów, potwierdzania tożsamości autorów, nadawców i adresatów przesyłanych elektronicznie dokumentów, uwierzytelniania stron itp.
 
Zamierzamy opracować i zaimplementować w systemie VerICS nowe metody, szczególnie do weryfikacji protokołów uwierzytelniania stron i wiarygodnego uzgadniania kluczy kryptograficznych dla szyfrów zwanych symetrycznymi i asymetrycznymi, w tym protokołów ze znacznikami czasu. Takie protokoły są obecnie najbardziej czułym punktem kryptograficznej ochrony danych i transakcji sieciowych. Uważa się, że dysponujemy już dostatecznie silnymi, obliczeniowo trudnymi do złamania algorytmami szyfrowania opartymi na zaawansowanych technikach teorii liczb i algebry. Można stosować je jednak dopiero po uwierzytelnieniu tożsamości zainteresowanych stron i dokonaniu niezbędnych uzgodnień klucza lub zestawu kluczy szyfrujących i rozszyfrowujących przesyłane dokumenty.
 
Mimo iż obecnie najczęściej stosowane w praktyce są protokoły uwierzytelniania wykorzystujące znaczniki czasu, to jednak procesowi weryfikacji najlepiej poddają się protokoły, których moc kryptograficzna (trudność złamania) oparta jest na liczbach jednorazowego użytku (ang. nonces). Dotychczas znane metody pozwalały na uzyskanie zadowalających wyników przeprowadzanych weryfikacji dla tego typu protokołów. Jednak nikomu dotąd nie udało się przeprowadzić weryfikacji poprawności protokołów uwierzytelniania stron z zależnościami czasowymi. Chcemy do tego wykorzystać metody bazujące na translacji tego problemu do problemu testowania spełnialności formuł zdaniowych.

Systemy automatycznej weryfikacji budowane są w kilku ośrodkach na świecie np. COSPAN [HKK96] w AT&T, a niektóre z nich są publicznie dostępne jak NuSMV [NuSMV], KRONOS [Yov97], HyTECH [HH95], SPIN [Hol91,Hol97], VERUS [VC97], lub UppAal [LPY97,BLL+98]. Jednakże naszym głównym celem jest rozbudowa polskiego oryginalnego systemu weryfikacyjnego VerICS o nowe moduły, które powstaną jako wynik końcowy naszych rozwiązań teoretycznych. Opracowane translacje z języka Promela, Timed-UML, Java do języka bazowego systemu VerICS umożliwią wykorzystanie istniejących (lub nowych) modułów VerICSa do weryfikacji tych programów. Dzięki takim translacjom uzyskamy jako pierwsi na świecie możliwość wykorzystania metod BMC i UMC (bazujących na SAT-testerach) do weryfikacji programów w wyżej wymienionych językach. Ze względu na dużą efektywność metod bazujących na SAT-testerach liczymy na przesunięcie granic możliwości dla weryfikacji modelowej programów i protokołów kryptograficznych.

Podjęcie tego problemu w Polsce uzasadnia także gwałtownie rosnący popyt na metody weryfikacji dla programów zależnych od czasu, takich jak np. protokoły komunikacyjne, protokoły kryptograficzne (uwierzytelniania stron i wiarygodnego uzgadniania kluczy kryptograficznych ze znacznikami czasu (ang. time stamps), z określonym okresem ważności (ang. lifetime)) oraz inne programy realizujące różne usługi w sieciach komputerowych. Panuje również opinia, że dalszy dynamiczny rozwój technologii informatycznych jest istotnie uzależniony od dostępności metod weryfikacji.

Podjęcie proponowanego tematu przez nasz zespół uzasadniają wcześniejsze wyniki osiągnięte przez wykonawców projektu (i ich doktorantów) w dziedzinie weryfikacji systemów czasu rzeczywistego [DPP01, DPP02a, DPP02b, DDJJ02, JJ04, PP01, PP04a, PP04b, PPS03, PWZ02, WZP03, Zbrz04], systemów wieloagentowych [KL04, KLP03, KLP04, LŁP03, LP03a, LP03b], protokołów kryptograficznych i systemów kontroli dostępu do danych [JP00, JP00a, JS02, Kur02, KM03, KP03, Kur03], semantyki dla systemów i języków z czasem [DB87, Demb89, Demb97]. Należy zwrócić uwagę, że wiele z naszych wyników uzyskało międzynarodowe uznanie (patrz publikacje na konferencjach FTRTFT, TACAS, ICATPN, AAMAS, FORMATS, FAMAS), a jeden z głównych wykonawców pełnił rolę konsultanta w AT&T Bell Labs. USA, pracując nad zastosowaniem metod redukcji częściowo-porządkowych w systemie SPIN.

Podjęty temat ma również ścisły związek z doświadczeniami i potrzebami wynikającymi z prowadzonych równolegle przez członków zespołu badań związanych z systemami wieloagentowymi i ich implementacją na uniwersalnej platformie wykorzystującej możliwości języka Java i rzeczywistą sieć połączeń internetowych. Te badania prowadzone są między innymi w ramach grantu wspierającego projekt Unii Europejskiej ALFEBIITE. Inne doświadczenia i związki wynikają z wieloletnich prac głównych wykonawców nad narzędziami wspomagającymi projektowanie, implementację i weryfikację protokołów komunikacyjnych, w szczególności przy wykorzystaniu standardowego języka Estelle [ISO97].

Celem perspektywicznym jest dalszy rozwój prototypowego narzędzia, jakim jest obecnie VerICS, do uzyskania w pełni profesjonalnej wersji weryfikatora, która może stać się systemem używanym przez polskie ośrodki badawcze lub wręcz systemem komercyjnym.

Istniejący stan wiedzy w zakresie tematu badań

Automatyczna weryfikacja programów o skończonej liczbie stanów poprzez analizę ich modeli (przestrzeni stanów) jest niezwykle aktywną dziedziną badawczą, która już przyniosła obiecujące praktyczne rozwiązania. Wyniki te są dokumentowane między innymi w czasopiśmie Formal Methods in System Design (Kluwer) oraz materiałach takich konferencji, jak Computer Aided Verification czy też Tools and Algorithms for the Construction and Analysis of Systems, publikowanych przez Springer-Verlag. Poniżej przedstawiamy kolejno opisy stanu wiedzy dotyczącej weryfikacji programów w Javie, Promeli, Timed-UML oraz algorytmów uwierzytelniania stron. W kolejnej sekcji omawiamy szczegółowo, na czym polega oryginalność i nowatorstwo proponowanych przez nas badań.

Java jest językiem obiektowo zorientowanym z wbudowanymi mechanizmami obsługi wątków oraz zaawansowaną obsługą pamięci. Jest wykorzystywana do modelowania systemów czasu rzeczywistego w NASA. Praktycznie zastosowano ją podczas realizacji projektu "Deep Space 1". Java została również wykorzystana do modelowania systemu operacyjnego sond marsjańskich, po tym jak stwierdzono wiele uchybień w działaniu oprogramowania w misji sondy PathFinder w 1997 r. Projekt Java PathFinder 1 (JPF1) [HP99], zakładał realizację translatora kilku klas języka Java w wersji 1.0 do języka Promela systemu SPIN [Hol91,Hol97]. Do czasu powstania projektu JPF1 do testowania oprogramowania używano systemu SPIN, a źródła programów LISP przepisywano ręcznie na język Promela. Proces weryfikacji w JPF1 polegał na przepisaniu źródeł systemów operacyjnych sond z języka LSP na język Java, wykonaniu translacji Java do Promela, a następnie testowaniu kodu w SPIN. Translator JPF1 został napisany w języku LISP, natomiast parser dla Java w MoscowML. Technika testowania kodu w Promeli wykorzystuje logiki temporalne LTL [CGP99] i ma na celu detekcję zakleszczeń (ang. deadlock). Z uwagi na duże problemy z translacją wyjątków języka Java, na prośbę autorów projektu, Gerard Holzmann dokonał zmian w semantyce Promeli. Translator tłumaczy tworzenie obiektów, dziedziczenie, wątki oraz synchronizację (metody "wait" i "notify"), wyjątki, przerwania wątków, standardowe instrukcje warunkowe oraz pętle. Translator nie obsługuje: pakietów, przeciążania metod, rekursji, łańcuchów znaków, danych zmiennoprzecinkowych, zmiennych statycznych, metod statycznych, niektórych operacji na wątkach. Liczba obiektów danej klasy ograniczona jest do siedmiu, dlatego też zaniechano rozwoju translatora i wykonywania testów za pomocą SPIN na rzecz własnego systemu testującego o nazwie Java PathFinder 2 [VHB+03].

Java PathFinder 2 powstał jako system weryfikacyjny, którego motor stanowi wirtualna maszyna Javy, oznaczana w literaturze dla odróżnienia od produktu firmy SUN jako JVMJPF. Testowanie programów w języku Java za pomocą JPF2 odbywa się na poziomie skompilowanego kodu bajtowego. Do analizy tego kodu bajtowego jest stosowana biblioteka BCEL API [Dah01] autorstwa Markusa Dahm'a. Do wykrywania zjawiska "data racing'u" w kodzie bajtowym Javy zastosowano algorytm Eraser [SBN+97] autorstwa firmy Compaq. Wykrywanie zjawiska zakleszczenia zrealizowano za pomocą algorytmu GoodLock [Hav00], czasem nazywany również LockTree. Za pomocą JPF2 testowano głównie nowy system zarządzania statkami kosmicznymi o nazwie Remote Agent [FinRep00]. Jego zadaniem jest podejmowanie samodzielnych decyzji w przestrzeni kosmicznej na podstawie wskazania czujników bez kontaktu z naziemną kontrolą lotów. Po kolejnych niepowodzeniach z lądowaniami sond marsjańskich postanowiono wrócić do testowania oprogramowania za pomocą LTL. Projekt nazwano Java PathExplorer (JPAX) [HR01]. JPAX działa tak samo jak JPF2, analizuje kod bajtowy z tym, że algorytmy Eraser oraz LockTree zostały zastąpione rozwiązaniami wykorzystującymi logiki temporalne.

Do testowania programów napisanych w Javie opracowano w laboratoriach SAnToS (ang. The Laboratory for Specification, Analysis, and Transformation of Software) narzędzie o nazwie BANDERA [CDH+00]. System BANDERA sam w sobie nie jest narzędziem testującym, lecz generującym kod w Promeli, który następnie jest testowany za pomocą systemu SPIN. Zadaniem systemu BANDERA jest translacja kodu źródłowego Javy do języka Jimple kompilatora Soot [VHS+99], opracowanego w University of McGill. Podczas translacji z Java do Jimple jest wyodrębniana cześć kodu, która ma podlegać testowaniu przez moduł Slicer oraz jest redukowany rozmiar tak powstałego modelu poprzez moduł BABS (Bandera Abstraction-Based Specializer). Tak powstały kod w Jimple trafia do modułu BIRC (Bandera Intermediate Representation Constructor), który dokonuje kolejnej translacji na język BIR (Bandera Intermediate Representation). Na koniec kod w języku BIR jest przetwarzany przez moduł SPIN Trans na język Promela. Nikt dotąd nie zastosował metod bazujących na SAT do weryfikacji programów w Javie.

PROMELA (PROtocol MEta LAnguage) jest niedeterministycznym językiem wysokiego poziomu. Wykorzystywana jest głównie w systemie SPIN [Hol04, Hol91,Hol97]. System ten jest efektywnym narzędziem służącym do weryfikacji programów współbieżnych i protokołów komunikacyjnych "on-the-fly". Komunikacja między procesami umożliwiana jest za pomocą mechanizmów rendez-vous, buffered message passing oraz komunikacji poprzez pamięć dzieloną zarówno w trybie synchronicznym, jak i asynchronicznym. System SPIN cieszy się uznaniem na całym świecie i jest stosowany w wielu projektach, np. w PathFinder [HP99]. SPIN posiada graficzną nakładkę o nazwie XSPIN umożliwiającą łatwą nawigację po opcjach programu, szybką korekcję błędów w kodzie specyfikacji oraz generowanie obrazu systemu i symulację przebiegu procesu. System został rozbudowany o obsługę czasu dyskretnego DTSPIN [BD98,Bos97,TC96], który został zaimplementowany poprzez wprowadzenie typu timer będącego liczbą całkowitą nieujemną. Na zegarach dozwolona jest operacja set, która ustawia zegar na daną parametrem wartość. Ważne jest to, że w odróżnieniu od innych rozwiązań zegar odlicza w dół aż do momentu uzyskania wartości expire (domyślnie 0).

Po wczytaniu specyfikacji systemu wyrażonej za pomocą języka Promela następuje proces weryfikacji, w którym powstaje program (automat Büchi'ego) zoptymalizowany pod kątem weryfikacji "on-the-fly", następnie kod zostaje przeanalizowany za pomocą algorytmu zagnieżdżonego DFS i w rezultacie zostaje zwrócony kontrprzykład. Ponieważ graf wynikowy może posiadać ogromne ilości węzłów, SPIN używa metod optymalizacji i minimalizacji takich jak redukcja częściowo-porządkowa, kompresja stanów czy bit-state hashing. Zatem metoda weryfikacji nie jest symboliczna i dotąd nie została opracowana metoda weryfikacji programów w Promeli bazująca na translacji do SAT.

Jednocześnie w dziedzinie systemów wieloagentowych wiele opracowywanych metod weryfikacji bazuje na translacji do Promeli i użyciu narzędzia SPIN [BFP+03,WFH+02]. Translacja z Promeli do jednego z wejść systemu VerICS pozwoli zatem na weryfikację systemów wieloagentowych metodami symbolicznymi.

UML (Unified Modeling Language) jest graficznym językiem służącym do projektowania, modelowania i analizy systemów informatycznych. Obecnie jest jednym z dominujących standardów w dziedzinie tworzenia oprogramowania. Zasadniczo jest używany do modelowania systemów z użyciem obiektów. Notacja UML opiera się na dwunastu typach diagramów. Każdy z nich ukazuje modelowany system z innej perspektywy, więc zbiór diagramów pozwala opisać go bardzo dokładnie. Istnieje wiele podzbiorów UML umożliwiających modelowanie specyficznych klas systemów takich jak np. systemy czasu rzeczywistego, systemy odporne na uszkodzenia (fault-tolerant systems) czy systemy transakcyjne. Najciekawszym obszarem badań nad językiem UML w powiązaniu z systemem VerICS wydaje się problem weryfikacji systemów wyspecyfikowanych za pomocą czasowego UML [GOO03].

Zastosowanie technik formalnej analizy języka UML oraz weryfikacja czasowego UML jest możliwa do przeprowadzenia dzięki istniejącym narzędziom do weryfikacji systemów czasowych. Zasadniczym problemem jest zatem translacja z diagramów UML do reprezentacji akceptowanej przez istniejące narzędzia służące do symulacji i weryfikacji. Jednym ze środowisk, które pozwala na weryfikację czasowego UML jest środowisko IF. Tutaj odbywa się translacja diagramów UML z postaci zgodnej ze standardem XMI do komunikujących się rozszerzonych automatów czasowych [GO03, GOO04] reprezentowanych w języku bazowym środowiska IF [BFG+99,BFG+99a]. Weryfikacja modelowa i/lub symulacja wykonywana jest przy użyciu narzędzia KRONOS [BDM+98] lub CADP [GLM02].

HUGO/RT [KM02, KMR02, SKM01] jest translatorem modeli UML do języka Promela oraz wewnętrznego języka systemu UPPAAL. Dzięki temu możliwy jest proces weryfikacji za pomocą środowiska SPIN oraz UPPAAL.

TURTLE [ACL+04, ASK03, SAL+02] jest narzędziem umożliwiającym edycję diagramów czasowego UML, przy zastosowaniu specjalnych rozszerzeń UML, np. specyficznych dla pakietu TURTLE stereotypów. Na podstawie diagramów UML generowana jest specyfikacja w języku Real Time LOTOS. Weryfikacja lub symulacja odbywa się w środowisku Real Time LOTOS.

Język bazowy systemu VerICS [DJJ02, JJ04] został opracowany w ramach naszego poprzedniego projektu KBN. Jest to język modelowania systemów, do którego mogą być tłumaczone języki wyższego poziomu (dotychczas opracowano translację z języka Estelle [DJJ+03a,DJJ03b]). Język bazowy pozwala na opisanie sieci procesów z zadanymi ograniczeniami czasowymi komunikujących się w sposób asynchroniczny (przez bufory i zmienne dzielone) lub synchroniczny (metodą spotkań). Opracowano również wstępne metody analizy statycznej (analizy kodu) do zmniejszenia rozmiaru automatów czasowych powstałych w wyniku translacji z języka bazowego. Metody te obejmują analizę zmiennych żywych i cięcie (ang. slicing). Analiza zmiennych żywych pozwala na wyeliminowanie martwych wartości zmiennych, czyli takich, które nie będą wykorzystane w dalszych obliczeniach. Metoda cięcia polega na usunięciu kodu nieistotnego z punktu widzenia weryfikowanych własności [JJ04].

Oryginalność naszego pomysłu polega na wykorzystaniu do weryfikacji programów dwóch komplementarnych metod symbolicznej weryfikacji: BMC (ograniczonej weryfikacji modelowej) i UMC (nieograniczonej weryfikacji modelowej), które wykorzystują translacje do SAT i SAT-testery. Ponadto, w odróżnieniu od istniejących i opisanych powyżej metod, już na etapie translacji z języka programowania do języka bazowego (lub bezpośrednio do rozszerzonej sieci automatów) zamierzamy zastosować metody cięcia [JJ04], redukcji częściowo-porządkowych [GKPP99] i symetrii [God99], które dokładniej omawiamy w dalszej części projektu. Zastosowanie redukcji na tak wczesnym etapie jest niezwykle istotne, gdyż jak pokazuje praktyka, rozmiar programu lub sieci automatów po translacji może być często zbyt duży, aby dalsza weryfikacja była możliwa. Ponadto translacja z programów i BMC będą wykonywane "on-the-fly", gdyż tylko fragment sieci automatów jest potrzebny do weryfikacji, której zadaniem jest znajdowanie błędów, jak to ma miejsce w przypadku BMC. Stanowi to dużą przewagę naszego systemu nad środowiskiem IF. Moduły weryfikacyjne BMC i UMC są częścią środowiska VerICS, a więc możemy je połączyć z translatorami w najbardziej efektywny sposób. Podobny pomysł został wykorzystany w weryfikatorze VeriSoft [God03], gdzie jednak weryfikacja nie jest wykonywana symbolicznie.

Stan wiedzy w zakresie protokołów uwierzytelniania stron

Do najbardziej znanych protokołów należą protokół Needhama-Schroedera i schemat Kerberos [MOV01]. Są one podstawowymi komponentami większych systemów ochrony dostępu do zasobów, potwierdzania transakcji płatniczych w e-bankowości, e-handlu, także w e-administracji. Metody weryfikacji poprawności protokołów uwierzytelniania stron badane są i rozwijane ostatnio intensywnie w USA - w Carnegie Mellon University (przez Edmunda Clarke'a i jego współpracowników) [MCJ97, CJM98, CJM00] i w Naval Research Laboratory w Waszyngtonie (przez Catherine Meadows) [Mea95, Mea01, Mea03, Mea03a], w Anglii w Cambridge [Low02, Low95, Low96, LS03] i we Francji [Bol97, Bol97a]. Prace nad tymi zagadnieniami prowadzą także członkowie zespołu: Marian Srebrny, Mirosław Kurkowski i Gizela Jakubowska [Kur02, Kur03, KM03, KP03, JP00, JP00a, JS02]. Interesującą próbę w tej dziedzinie przeprowadzili autorzy [PST02] przy pomocy narzędzia NuSMV. Jednak weryfikacji poddano tylko własności nie zawierające w ogóle znaczników czasu. Nikomu dotąd nie udało się przeprowadzić weryfikacji poprawności protokołów uwierzytelniania stron z zależnościami czasowymi.

Najbardziej znaną próbą sformalizowanej analizy własności protokołów uwierzytelniania stron była specjalnie skonstruowana logika uwierzytelniania [BAN90], nazywana też logiką BAN. Interesującą wersję logiki BAN, nazywaną czasem logiką BANK, z dość naturalną semantyką i własnością pełności przedstawił niedawno [Kur03]. Metody dedukcyjne (theorem proving) z ogólnym systemem Isabelle proponowali Bella i Paulson [BP97], z Murphi proponowali [MMS97], także NRL Catherine Meadows [Mea96], Dominique Bolignano [Bol97] i inni.

Weryfikacja modelowa protokołów uwierzytelniania stron jest od kilku lat przedmiotem intensywnych badań w wielu ośrodkach naukowych i komercyjnych. Użytkownik zadaje protokół i specyfikację śladów (przeplotów) niepożądanych wykonań protokołu a "model checker" buduje model (fragment modelu) protokołu i sprawdza, czy niepożądane ślady są w modelu. W porównaniu z innymi rodzajami protokołów trudność polega tu przede wszystkim na konieczności uwzględnienia zmian wiedzy nabywanej przez poszczególnych uczestników (agentów) w trakcie wykonań protokołu. Chodzi przede wszystkim o informacje na temat uzgodnień kluczy kryptograficznych na określoną sesję albo na ustalony okres ważności. Trzeba to uwzględniać przy redukcji przestrzeni możliwych stanów.

Często próbuje się to robić przy pomocy ogólnych (ang. general purpose) narzędzi weryfikacji modelowej ([Lowe97], [Ros96]), tj. narzędzi nie wyspecjalizowanych dla protokołów kryptograficznych. W [CJM98] zaproponowano narzędzie specjalnie skonstruowane dla weryfikacji protokołów uwierzytelniania stron. Specjalnie zaprojektowane z myślą o weryfikacji poprawności protokołów kryptograficznych redukcje częściowo-porządkowe zaimplementowane zostały w systemie o wdzięcznej nazwie Brutus ([CJM00], [CMJ00a]).

W typowym podejściu weryfikacji modelowej modele wykonań tego rodzaju protokołów można rozumieć jako asynchroniczne złożenia procesów, które reprezentują zachowania poszczególnych uczestników, w tym także nieuczciwego uczestnika, zwanego intruzem. Procesy te są sekwencyjne. Mogą porozumiewać się przekazując (przesyłając) sobie informacje o określonej składni i semantyce. Tak jak w prawdziwej sieci teleinformatycznej, przesyłane informacje mogą być przechwytywane przez intruza, kopiowane, przeadresowywane itp. Intruz może też sam generować informacje i przesyłać je do upatrzonych adresatów.

By zapewnić, że model jest skończony, wprowadza się ograniczenia na ilość uczestników i ilość wykonań protokołu (sesji). Każdy uczestnik może brać udział w kilku sesjach jednocześnie. Rozmiar modelu rośnie jednak wykładniczo ze względu na te parametry. Redukcje częściowo-porządkowe zmniejszają przestrzeń badanych stanów modelu przez pominięcie przeplotów wykonań nie wnoszących nic istotnego z punktu widzenia sprawdzanej własności poprawności modelowanego protokołu. Typowym przykładem może być relacja równoważności utożsamiająca przeploty różniące się tylko kolejnością następujących po sobie akcji wysyłania informacji, które należą do różnych sesji.

Własności poprawności protokołów kryptograficznych są na ogół formułowane w języku logiki temporalnej CTL (Computation Tree Logic). Czasem w języku logiki wyspecjalizowanej odpowiednio dla stosowanego narzędzia weryfikującego. Na przykład, językiem opisu protokołów kryptograficznych Catherine Meadows jest NPATRL. Lowe w swoich pracach wykorzystuje CSP jako sposób prezentacji modelu protokołu w środowisku FDR - model checker. System Brutus ma swoją własną, oryginalną tzw. logikę Brutusa. Jest to wersja temporalnej logiki pierwszego rzędu z kwantyfikatorami po skończonych podzbiorach modelu, z czasem liniowym, z operatorem przeszłości (ang. the past-time operator) oraz z atomowymi wyrażeniami dla akcji i zmian wiedzy poszczególnych uczestników. Algorytm Brutusa nie odwołuje się do testerów SAT.

Metody testerów SAT stosowane są w niektórych najnowszych systemach. NuSMV używa testera zChaff, ale również metod opartych na BDD. Autorzy [PST02] nie piszą, która z tych metod była zastosowana w ich eksperymentach. Nowy system SATMC [AC03] jest interesującą próbą zaprzęgnięcia najlepszych testerów SAT do weryfikacji poprawności protokołów kryptograficznych.

Wykorzystanie metod SAT do weryfikacji modelowej

Symboliczna weryfikacja modelowa stanowi jedno z podejść umożliwiających zmniejszenie wpływu wykładniczej eksplozji stanów. Głównym założeniem jest reprezentowanie przeszukiwanej przestrzeni stanów w sposób symboliczny, poprzez formuły logiczne. Początkowe lata rozwoju metod symbolicznych to wykorzystanie binarnych diagramów decyzyjnych (BDD), opracowanie efektywnych operacji oraz translacje różnych formalizmów opisu systemów i własności. Około roku 1998 zauważono, że pojawiły się wysoce wydajne implementacje algorytmów testowania spełnialności formuł zdaniowych (SAT) i stało się możliwe zastosowanie tej metodologii do symbolicznej weryfikacji modelowej. Największą popularność zdobyły algorytmy SAT i ich implementacje (SAT-testery) bazujące na schemacie DPLL i wykorzystujące wysoce efektywne struktury danych. Oczywiście pisząc o efektywności należy pamiętać, że problem SAT należy do klasy złożoności NP-zupełne, co implikuje istnienie przykładów instancji, dla których czas wykonania (testowania) rośnie wykładniczo ze względu na rozmiar badanej formuły. (Przy założeniu N nie równe NP.) Okazuje się jednak, że spełnialność wielu formuł kodujących rzeczywiste systemy może być testowana efektywnie.

Pierwszym zastosowaniem SAT do weryfikacji modelowej była Ograniczona Weryfikacja Modelowa (Bounded Model Checking, BMC). Ogólna idea może być przedstawiona jako symboliczne kodowanie fragmentu modelu i poszukiwanie w tym fragmencie kontrprzykładu falsyfikującego badaną własność. Problem ten jest reprezentowany poprzez formułę zdaniową, której spełnialność jest testowana za pomocą efektywnych narzędzi tzw. SAT-testerów. Ogólne podejście BMC doczekało się licznych rozszerzeń i optymalizacji. Klasa weryfikowanych systemów została poszerzona o automaty z czasem, czasowe sieci Petriego [PP04b] i systemy interpretowane [PL03a], a testowanych własności - o uniwersalny podzbiór języków TCTL [PWZ02], CTLK [PL03b, LŁP03]. Ofer Stichman [Str00] w swych badaniach usiłował odpowiedzieć na pytanie, czy efektywność metody może być zwiększona poprzez testowanie spełnialności SAT z wykorzystaniem wiedzy o strukturze problemu. Uzyskał zachęcające wyniki, ale opracowane algorytmy miały charakter optymalizacji nie wpisujących się w ramy jednolitej metodologii (w przeciwieństwie do wielu metod optymalizacji stosowanych w weryfikacji modelowej, np. redukcji częściowo-porządkowych lub redukcji wykorzystujących symetrię badanych systemów).

BMC jest w praktyce algorytmem falsyfikacji, zdolnym do znajdowania pewnych błędów w systemach o ogromnej liczbie stanów, ale w większości przypadków nie umożliwiającym przeszukania pełnej przestrzeni stanów. Zaproponowany przez Kena McMillana w pracy [McM02] algorytm nieograniczonej weryfikacji modelowej (UMC) jest przeniesieniem metodologii BDD na grunt metod SAT. Kluczowym komponentem, na którym opiera się metoda, jest algorytm eliminacji kwantyfikatorów uniwersalnych, bazujący na algorytmie SAT. Metoda UMC nie doczekała się dotąd wielu uogólnień i kontynuacji, w [McM02] wyraża się przypuszczenie, że praktyczna efektywność jest uwarunkowana dokonaniem optymalizacji w zakresie generowania i reprezentacji klauzul blokujących.

Wyzwaniem dla badaczy dziedziny weryfikacji modelowej jest analiza systemów z czasem. Algorytm BMC został uogólniony w tym kierunku [WZP03,Zbrz04,Sor02]. Pojawiła się także realizacja UMC dla systemów z czasem [SB03], w której najbardziej istotny problem rozwiązywania równań opisujących zależności czasowe jest sprowadzony do problemu SAT poprzez kodowanie "Per-Constraint-Encoding" [SLB03].

Metodyka badań

Translacje z fragmentów języków programowania Java, Promela, Timed-UML

Pierwszym zadaniem jest wyodrębnienie podzbioru języka Java, który obecnie może zostać zaimplementowany za pomocą języka bazowego i/lub rozszerzonych sieci automatów czasowych. W obu przypadkach translacja będzie uwzględniać metodę cięcia [HCD+99] oraz inne redukcje. Następnie zostaną opracowane dwa modele translacji typu:

• proces w języku Java -> proces w języku bazowym,
• proces w języku Java -> automat lub zbiór automatów czasowych,

Zostanie opracowany i zaimplementowany translator przy użyciu narzędzi Flex [Pax95] i Bison [DS02]. Są to narzędzia oparte na licencji GNU[Gnu]. Flex jest generatorem analizatorów leksykalnych, który łączy w sobie elementy języka wyrażeń regularnych z elementami programowania w języku C. Natomiast Bison jest generatorem translatorów łączącym w sobie cechy generatora Flex oraz możliwość stosowania gramatyk niejednoznacznych. Celem jest uzyskanie funkcjonalności translatora przynajmniej JPF1.

Kolejnym celem jest opracowanie modułu translatora z Promeli do języka bazowego systemu VerICS i/lub rozszerzonej sieci automatów czasowych (w kodzie Kronosa akceptowanym przez VerICS), jak również opracowanie modułu obsługi rozszerzenia Promeli o specyfikacje czasu rzeczywistego [BD98]. Translacja będzie wykorzystywać metodę cięcia [MT98] i pozostałe redukcje: częściowo-porządkowe i symetrie. Zamierzamy osiągnąć funkcjonalność zbliżoną do SPIN i DTSPIN.

W translacji Timed-UML pierwszym zadaniem jest wyodrębnienie zbioru notacji, rozszerzeń i diagramów UML, które będą poddawane weryfikacji. Wymaga to określenia precyzyjnej semantyki dla tego zbioru. Następnie zostanie opracowana metoda translacji wybranych diagramów UML do języka bazowego systemu VerICS i/lub do postaci rozszerzonej sieci automatów czasowych w formacie KRONOS. Jak w przypadku Javy i Promeli translacja będzie wykorzystywać znane redukcje. Na tym etapie zostanie rozważona możliwość wykorzystania fragmentów systemu IF [BFG+99]. Zostanie zaimplementowane narzędzie do automatycznej translacji diagramów UML do postaci akceptowanej przez system VerICS.

Metoda symetrii, cięcia i redukcji częściowo-porządkowych w translacji

Głównym problemem weryfikacji modelowej jest tzw. wykładnicza eksplozja stanów modelu, która w poważny sposób ogranicza rozmiary systemów, z którymi można zmierzyć się w procesie weryfikacji. Dlatego przestrzenie stanów są redukowane tak, aby zostały maksymalnie zmniejszone, a jednocześnie testowane własności zostały zachowane. Symetria [God99, HBG+03] jest metodą, która pozwala wykorzystać informację o tym, że system składa się z wielu symetrycznych (identycznych) komponentów.
Kolejną z metod radzenia sobie z problemem eksplozji stanów jest metoda cięcia [JJ04] polegająca na usunięciu zmiennych nieistotnych z punktu widzenia weryfikacji. Metodę cięcia po raz pierwszy zastosował Weiser [Wei84] do eliminacji nieistotnych szczegółów podczas śledzenia zachowania i symulacji programów sekwencyjnych. Od tej pory była ona intensywnie rozwijana i znajdowała coraz więcej zastosowań. Tip w pracy [Tip95] prezentuje wyczerpujący przegląd różnych odmian tej metody. Millett i Teitelbaum [MT98] jako pierwsi zaproponowali użycie metody cięcia do redukcji przestrzeni stanów w procesie weryfikacji modelowej systemów bezczasowych. Autorzy przeprowadzili redukcję programów zapisanych w Promeli, języku wejściowym weryfikatora modelowego SPIN [Hol97]. Praca [HDZ99] przedstawia formalną analizę metody cięcia dla języków sekwencyjnych zachowującą spełnialność formuł logiki LTL. Z kolei jej kontynuacja [HCD+99] prezentuje zastosowanie tej techniki do wielowątkowych programów w Javie, formalizmie wejściowym systemu weryfikacyjnego Bandera [DHS99]. Metoda cięcia jest obecna również w środowisku IF [BFG+99, BFG+99a], jednak podobnie jak w poprzednich przypadkach jej zastosowanie jest ograniczone do systemów bezczasowych [BFG00]. Praca A. i P. Janowskich [JJ04] jest pierwszą próbą wykorzystania metody dla systemów z czasem.

Kolejną metodą są redukcje częściowo-porządkowa [Pel98, GKPP99] wykorzystujące fakt, że weryfikowane własności w wielu przypadkach nie zależą od kolejności, w jakiej występują niezależne od siebie zdarzenia. Redukcje częściowo-porządkowe systemów czasu rzeczywistego [BJLW98] są zadaniem trudniejszym niż w przypadku systemów bezczasowych, ponieważ ograniczenia na czas wykonania tranzycji wprowadzają nowego rodzaju zależności. Pierwsza próba połączenia redukcji częściowo-porządkowych i automatów z czasem opisana została w [Pag96]. Wprowadza ona model stref czasowych i rozważa zależności między tranzycjami czasowymi i akcyjnymi. Jedyną zachowywaną własnością jest osiągalnosć. [DGKK98] rozszerza pojęcie relacji niezależności na systemy czasowe. Korzysta z logiki LTL do specyfikacji własności. W [VP99] metody redukcji częściowo-porządkowych zachowują logikę CTL a jako model systemu użyte są sieci Petriego z czasem. [Min99] korzysta z lokalnej semantyki dla systemu, dzięki czemu ogranicza liczbę zależności i pozwala na bardziej wydajne redukcje (choć osiągnięte kosztem synchronizowania automatów). Tradycyjnie, metoda redukcji częściowo-porządkowych wprowadza zmiany do algorytmu przeszukiwania przestrzeni stanów modelu polegające na tym, że zamiast wszystkich tranzycji, umożliwionych w stanie globalnym modelu, brany jest pod uwagę tylko pewien ich podzbiór. Wadą takiego podejścia z naszego punktu widzenia jest to, że bez znaczących modyfikacji sposobu przeszukiwania przestrzeni stanów nie można połączyć redukcji częściowo-porządkowych z symbolicznymi technikami weryfikacji modelowej, które są najbardziej efektywną metoda tej weryfikacji, co potwierdzają nasze doświadczenia przy projektowaniu systemu VerICS [WZP03]. Dlatego też chcemy zaproponować inne podejście, a mianowicie zastosować metody redukcji częściowo-porządkowych na etapie generowania rozszerzonego automatu z czasem dla danego systemu (opisanego w języku bazowym [DJJ02] lub innym języku programowania poddawanym translacji). W ten sposób zamiast zmieniać algorytm przeszukiwania przestrzeni stanów otrzymanej za pomocą oryginalnej relacji przejścia możemy przeprowadzić zwykłe przeszukiwanie przestrzeni stanów otrzymanej przy wykorzystaniu zmodyfikowanej relacji przejścia. Pozwala to na bezpośrednie zastosowanie dowolnych istniejących narzędzi weryfikacji modelowej (w tym symbolicznej). Podejście takie zostało zastosowane (dla systemów bez czasu) na etapie kompilacji języka SDL do języka wejściowego weryfikatora COSPAN [KLM+98].

Nowe metody weryfikacji

Proponowane tematy badań dotyczące symbolicznej weryfikacji modelowej z wykorzystaniem SAT można podzielić na dwa nurty: opracowywanie nowych metod oraz optymalizacja algorytmów. Przeszłość dziedziny weryfikacji modelowej pokazuje, że algorytmy najczęściej stawały się praktycznie użyteczne i dostępne do zastosowania w analizie rzeczywistych systemów dopiero po optymalizacji początkowej koncepcji. Projekt zakłada podjęcie takich prac w odniesieniu do przedstawionych powyżej algorytmów BMC i UMC.

Metoda BMC dla rozszerzonych automatów czasowych

W przypadku BMC głównym zadaniem optymalizacyjnym będzie testowanie spełnialności formuły zdaniowej kodującej problem przy wykorzystaniu informacji o strukturze problemu. Projekt zakłada opracowanie algorytmu testowania SAT parametryzowanego przez metodę optymalizacji niesymbolicznej weryfikacji modelowej (np. redukcje częściowo-porządkowe, symetria). Fakt, że algorytm BMC jest oparty na pojęciu ścieżki, pozwala przypuszczać, że algorytmy opracowane dla podejść niesymbolicznych będą funkcjonować efektywnie. Szczególny nacisk będzie położony na takie zwiększenie efektywności oraz opracowanie rozwiązań algorytmicznych, aby umożliwić walidację systemów (stwierdzenie, że badana własność jest prawdziwa w pełnym modelu). Wstępne rozwiązanie zostało już opisane przez A. Zbrzeznego [Zbrz04]. Pierwszoplanowym przedmiotem badań będą rozszerzone sieci automatów czasowych [AD90, NSY92] bez ograniczeń na różnice zegarów.

Metoda UMC dla rozszerzonych automatów czasowych

Głównym zadaniem badawczym dotyczącym UMC będzie opracowanie tej metody dla rozszerzonych sieci automatów i języków opisu własności CTL i TCTL, a następnie opracowanie optymalizacji, które przyczynią się do praktycznej efektywności metody. Najważniejsze stwierdzone przyczyny nieefektywności to nieodpowiednia reprezentacja klauzul blokujących oraz wykładniczo duża ich liczba. Planujemy zastosowanie BDD jako reprezentacji badanego zbioru stanów oraz konstrukcję klauzul blokujących nad poszerzonym zbiorem literałów, zawierającym zmienne odpowiadające dowolnym podformułom. Docelowym rezultatem opisanych rozszerzeń ma być zastosowanie metody UMC do weryfikacji systemów z czasem, co ze względu na przedstawione problemy nie jest obecnie możliwe (mimo, że algorytm działa poprawnie i efektywnie dla systemów bezczasowych). Odnosząc się do pracy [SB03], opisującej realizację czasowej wersji UMC, nasza propozycja zakłada zakodowanie problemu w logice zdaniowej z wykorzystaniem dyskretyzacji opisanej w [Zbrz04], a następnie uogólnionej do różnic na zegarach. Takie rozwiązanie w przypadku BMC okazało się bardziej efektywne w porównaniu z kodowaniem "Per-Constraint-Encoding" ([Sor02,Zbrz04]).

Nowa metoda dyskretyzacji przestrzeni stanów

Dotychczas znane metody dyskretyzacji [Zbrz04] stosowane w wykorzystującej SAT analizie problemu osiągalności dla automatów czasowych nie uwzględniały automatów czasowych, w których występują warunki zegarowe umożliwiające porównywanie wartości dwóch zegarów. Opracowanie metody dyskretyzacji dającej się zastosować do badania problemu osiągalności dla takiej klasy automatów ma istotne znaczenie w wykorzystującym SAT rozwiązywaniu zadań planowania, które modelowane są przy pomocy automatów czasowych. Jednym z istotnych zagadnień jest tu problem znajdowania najkrótszej ścieżki pomiędzy dwoma wierzchołkami grafu. Jak wykazały wcześniejsze badania, dla węższej klasy automatów czasowych (a mianowicie takich, w których tylko wartość zegara można porównywać ze stałą) wykorzystujące SAT metody znajdowania ścieżek są tu bardzo efektywne, co daje nadzieję, iż dla rozszerzonej klasy automatów czasowych okażą się równie efektywne.

Literatura