Granty
Granty realizowane w Instytucie Informatyki
Kierownik grantu
dr hab. inż. Franciszek Seredyński
Lista wykonawców
dr Jarosław Skaruz
Okres realizacji
od 10-2008 do 9-2009
Opis grantu
Problemy włamań do sieciowych systemów informatycznych i związana z tym konieczność automatycznej detekcji takich włamań (ataków, intruzów) należą do jednych z najbardziej aktualnych zagadnień informatyki, wymagających szybkich i efektywnych rozwiązań. Prezentowany projekt badawczy dotyczy jednego z zagadnień tej problematyki, mianowicie zagadnienia wykrywania ataków na aplikacje WWW z użyciem poleceń języka SQL.
Jedną z najpopularniejszych metod wykonania ataku jest wykorzystanie formularzy znajdujących się na stronach WWW. Poprzez wpisanie znaków specjalnych oraz słów kluczowych języka SQL dokonywana jest zmiana postaci zapytania SQL zaimplementowanego przez programistę aplikacji. W rezultacie ataku zmodyfikowane zapytanie SQL jest wykonywane przez system zarządzania bazą danych, co prowadzi do ujawnienia informacji z bazy danych, do których użytkownik aplikacji WWW nie ma uprawnień. W projekcie, do rozwiązania problemu wykrywania ataków SQL proponuje się wykorzystanie trzech metod: rekurencyjnych sieci neuronowych, sztucznych systemów immunologicznych oraz ewolucyjnej metody określanej jako Gene Expression Programming (GEP).
Kierownik grantu
prof. dr hab. inż. Wojciech Penczek
Lista wykonawców
Artur Niewiadomski
Okres realizacji
od 2009-05-19 do 2010-06-01
Opis grantu
Głównym celem niniejszego projektu jest opracowanie nowej, oryginalnej metody weryfikacji modelowej dedykowanej dla systemów specyfikowanych w UML, pozwalającej na testowanie kluczowych własności systemu w początkowych fazach projektowania. Metoda ta ma polegać na zakodowaniu wszystkich możliwych wykonań systemu specyfikowanego w UML jako formuły zdaniowej. Następnie spełnialność tej formuły – w koniunkcji z symbolicznie zakodowaną testowaną własnością – będzie sprawdzana za pomocą istniejących, wyspecjalizowanych narzędzi, tzw. SAT-solverów. Jeżeli formuła ta będzie spełnialna, to znaczy że sprawdzana własność zachodzi w systemie, a SAT-solver zwróci wartościowanie zmiennych zdaniowych użytych do konstrukcji formuły. Wartościowanie to zostanie zdekodowane jako sekwencja stanów globalnych systemu. Umożliwi to wizualizację wykonania systemu, które prowadzi do stanu, w którym zachodzi testowana własność. Jeżeli system będzie sprawdzany pod kątem istnienia własności niepożądanych (np. zakleszczenia), to wizualizacja wykonania systemu, w którym taka własność zachodzi znacznie ułatwi projektantowi odnalezienie błędu.
Kierownik grantu
prof. dr hab. inż. Wojciech Penczek
Lista wykonawców
dr Artur Niewiadomski, dr Jarosław Skaruz, dr Agata Półrola, dr Mariusz Jarocki, dr Maciej Szreter, dr Łukasz Mikulski
Okres realizacji
od 2011-12-27 do 2015-04-26
Opis grantu
Rozwój sieci Internet zmienił sposoby osiągania złożonych celów, realizowanych poprzez współdziałanie wielu usługobiorców i usługodawców. Mało sformalizowane kontakty przez pocztę elektroniczną zostały zastąpione najpierw przez interakcję użytkowników z serwisami WWW, a następnie przez wymianę danych między aplikacjami kooperujących podmiotów. Następnym naturalnym etapem jest automatyzacja budowy planów złożonych przedsięwzięć (np. budowa domu, podróż dookoła świata) oraz znajdowanie optymalnych ofert dla usług z tych planów, pochodzących z Internetu.
System PlanICS, rozwijany w projekcie badawczym, realizuje ten cel, poprzez rozwiązanie kilka kluczowych problemów. Pierwszy problem to brak jednolitej semantyki usług udostępnianych w sieci, co uniemożliwia ich automatyczne współdziałanie. Proponowane rozwiązanie w odróżnieniu od istniejących pozwala na budowanie ontologii dziedzinowych i rejestru usług, które nie muszą opisywać całego świata dostępnych usług, pozwalając integratorowi na rozwiązywanie tylko interesującej go klasy zadań, na przykład związanych z danym sektorem przemysłu czy usług. Pokazujemy, że bazę wiedzy (ontologię) o usługach sieciowych, dostarczającą informacje niezbędne do automatyzacji procesu planowania każdy integrator takich usług może zbudować sam, bez konieczności modyfikacji istniejących interfejsów sieciowych po stronie kooperantów.
Problem wnioskowania w powyższym systemie wiedzy związany jest z wykładniczą eksplozją liczby możliwych rozwiązań, a także dynamiką informacji. Oferty usługodawców są nie tylko zmienne w czasie, ale również zależne od (potencjalnie nieznanych) kontekstów, których odkrycie jest możliwe poprzez zapytania ofertowe. Zatem, PlanICS realizuje koncepcję planowania wielofazowego, a moduły planujące wykorzystują najnowsze metody ze sztucznej inteligencji, jak algorytmy genetyczne i symboliczne kodowanie poprzez translację do problemu spełnialności formuł logicznych. Wielofazowość połączona z efektywnością tych metod gwarantuje skuteczność procesu planowania, zarówno na poziomie planowanie abstrakcyjnego w typach (“jak to zrobić”) jak i konkretnego w usługach (“z kim można zrobić to optymalnie”). Każdy etap planowania wymagał rozwiązania specyficznych problemów. Na przykład przy planowaniu abstrakcyjnym ważna była konstrukcja algorytmów umożliwiających znajdowanie istotnie różnych rozwiązań, do czego przyczyniło się opracowanie metody kompaktowej reprezentacji planów abstrakcyjnych, bazującej na koncepcji wielo-zbiorów i porządków częściowych.
Głównym wynikiem projektu jest opracowanie i zastosowanie, dla dwóch faz planowania, algorytmów hybrydowych będących pomysłowym rozwiązaniem łączącym szybkość algorytmów genetycznych z precyzją rozwiązań bazujących na testowaniu problemu spełnialności formuł. Ponadto, została opracowana nowatorska metoda parametrycznego planowania, w której system podpowiada modyfikacje zapytania w celu uzyskania planu. Wyniki zostały opisane w licznych publikacjach oraz wykorzystane w modułach systemu PlanICS.