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

Automatyczna weryfikacja działających w sieci (np. w Internecie) systemów rozproszonych o skończonej lub nieskończonej liczbie stanów, wykonywana poprzez analizę ich przestrzeni stanów, jest niezwykle aktywną dziedziną badawczą, która już od kilkunastu lat przynosi obiecujące praktyczne rozwiązania. W ramach poprzedniego projektu KBN Automatyczna weryfikacja systemów zależnych od czasu nasz zespół opracował, zaimplementował i uruchomił system weryfikacyjny VerICS. Opis systemu został opublikowany na dwóch renomowanych konferencjach w tej dziedzinie: zagranicznej TACAS'03 [DJJ+03a] i polskiej SCR'03 [DJJ+03b], a sam system jest dostępny poprzez interfejs www pod adresem http://pegaz.ipipan.waw.pl/~verics/. Ponadto wyniki projektu, opublikowane w ponad 30 pracach, zostały bardzo wysoko ocenione przez KBN, co znalazło wyraz w ocenie końcowej projektu "znakomity". Projekt ten miał charakter zdecydowanie teoretyczny (opracowanie nowych metod weryfikacji i ich matematyczne uzasadnienie). Obecny projekt zamierzamy zorientować na cele praktyczne. Jego głównym zamierzeniem jest opracowanie środowiska programistycznego ułatwiającego zewnętrzny dostęp do systemu VerICS i zastosowanie go do weryfikacji poprawności rozproszonych systemów oprogramowania i protokołów kryptograficznych.

Naszym celem jest zatem nie tylko uzyskanie nowych wyników teoretycznych w dziedzinie symbolicznej weryfikacji (poprzez translację do SAT ¹) dla systemów specyfikowanych w językach wysokiego poziomu oraz protokołów kryptograficznych, ale także rozbudowa systemu weryfikacyjnego VerICS tak, aby mógł być wykorzystany do automatycznej weryfikacji wyżej omówionych systemów. Oznacza to podjęcie następujących zadań. Dla potrzeb weryfikacji programów główny model narzędzia VerICS, którym są sieci automatów czasowych, zostanie rozszerzony o możliwość wykonywania operacji na zmiennych przy wykonywaniu przejść akcyjnych, a główny moduł weryfikacyjny, tzn. BMC (ograniczona weryfikacja modelowa) zostanie zmodyfikowany, aby uwzględnić to rozszerzenie. Planujemy również opracowanie i dodanie nowego modułu UMC (nieograniczona weryfikacja modelowa), który będzie umożliwiał dowodzenie pełnej poprawności dla systemów czasowych metodą symboliczną poprzez translację do SAT. Do zbudowania odpowiedniego środowiska programistycznego niezbędne będzie opracowanie metod translacji z programów wysokiego poziomu do rozszerzonych sieci automatów czasowych lub opracowanego w systemie VerICS języka bazowego. Obecnie VerICS umożliwia to w pewnym stopniu dla języka Estelle, przeznaczonego głównie do specyfikowania protokołów telekomunikacyjnych. Planujemy dodatkowo opracowanie translacji (połączonych z redukcjami) dla istotnych fragmentów następujących języków specyfikacji i programowania: Promela, Timed-UML i Java. Jest to trudne zadanie szczególnie dla języka UML, który nie ma sprecyzowanej semantyki i którą trzeba będzie zdefiniować dla potrzeb tego projektu. Język Java jest ostatnio najczęściej stosowany w programowaniu obiektowym, a język UML w specyfikowaniu systemów rozproszonych. Język Promela umożliwia włączenie do systemu VerICS metod i rozwiązań proponowanych dla istniejącego narzędzia SPIN.

Planujemy również opracowanie nowych metod weryfikacji poprawności kryptograficznych protokołów uwierzytelniania stron w sieciach teleinformatycznych i zaimplementowanie ich w systemie VerICS. Dostosowanie systemu VerICS do problematyki związanej z weryfikacją poprawności kryptograficznego oprogramowania zabezpieczającego przesyłane informacje i transakcje sieciowe będzie ważnym zadaniem tego projektu. Wymienione powyżej cele zostaną osiągnięte poprzez zdefiniowanie metody specyfikacji protokołów (również z ograniczeniami czasowymi) w jednym z dostępnych języków wejściowych lub też zaproponowanie nowego języka zdefiniowanego specjalnie w tym celu. Do specyfikowania własności przewidujemy konieczność użycia języka TCTL lub CTL rozszerzonego o operatory wiedzowe i deontyczne.

powrót