Program: Logiczne / formalne metody bezpieczeństwa

Obecnie prowadzę mały kurs (cztery dwugodzinne wykłady na poziomie magisterskim) na temat metod logicznych w zakresie bezpieczeństwa , chociaż tytuł Formalne metody w zakresie bezpieczeństwa może być bardziej trafny. Obejmuje krótko następujące tematy (wraz z powiązanymi metodami logicznymi):

• Cyfrowe zarządzanie prawami i egzekwowanie zasad (ogólna formalizacja, logika modalna, egzekwowanie za pośrednictwem automatów)

• Kod dowodu i uwierzytelnienie dowodu (teoria dowodu, systemy logiczne, izomorfizm Curry'ego-Howarda, weryfikacja)

• Kontrola dostępu (logika nieklasyczna, teoria dowodu)

• Inspekcja stosu (semantyka języka programowania, równoważność kontekstowa, bisimulacja)

Oczywiście kurs ma wiele celów, z których jeden przyciąga potencjalnych absolwentów.

W nadchodzących latach kurs może zostać rozszerzony na zwykły kurs, który będzie wymagał więcej treści. Biorąc pod uwagę, że pochodzenie ludzi tutaj jest zupełnie inne niż moje, chciałbym wiedzieć, jakie treści włączylibyście w taki kurs.

Sugeruję zapoznanie studentów z następującą logiką:

• Logika epistemiczna: służy do modelowania wiedzy różnych stron uczestniczących w protokole i dowodzenia, że ​​przeciwnik nie może uzyskać wiedzy na temat jakiejś tajemnicy.
• Logika BAN: stara logika do potwierdzania różnych właściwości protokołów uwierzytelniania. ( Również inne logiki przekonań są odpowiednie).
• Logika dla systemów przejściowych: Obejmuje logikę taką jak LTL, CTL i LTL *. (taka logika działa na modele protokołu podobne do Kripke).
• Algebry procesów: Kilka algebrów procesów, takich jak Rachunek Spi (lub CSP i jego narzędzie związane z bezpieczeństwem, Casper ) są przydatne do modelowania protokołów bezpieczeństwa.
• Bardzo przydatne są narzędzia takie jak AVISPA firmy NuSMV .
• Proponuję również formalną poprawność protokołów bezpieczeństwa jako jeden z podręczników kursu.

Mój przyjaciel, Morteza Amini , niedawno uzyskał tytuł doktora. na temat modelowania kontroli dostępu za pomocą logiki. Opracował nową logikę o nazwie , która oznacza „logikę deontyczną i logikę opisu z wieloma uprawnieniami”. Jak sama nazwa wskazuje, łączy dwie nieklasyczne logiki (logika deontyczna + logika opisu), aby zdecydować, czy jednostka ma dostęp do obiektu. Jeśli chcesz, mogę zachęcić go do podania dodatkowych informacji.$MA(DL)^2$

Kilka lat temu odbył się kurs czytania w Carnegie Mellon, Languages ​​and Logics for Security , który próbował przejrzeć część literatury na temat uwierzytelniania, autoryzacji, przepływu informacji, obliczeń protokołów, ochrony i zarządzania zaufaniem; strona internetowa kursu zawiera slajdy do artykułów, które omawialiśmy, a także dodatkową listę odniesień do każdego tematu. Zwłaszcza przepływ informacji może być czymś, na co warto spojrzeć w odniesieniu do wymienionych tematów.

Istotny jest także program kursu Anupam Datta Podstawy bezpieczeństwa i prywatności .

Odpowiedź Roba przypominała mi podobną grupę czytelniczą Cornell, którą Michael Clarkson organizował przez kilka lat: Cornell Security Discussion Group . Być może warto przejrzeć niektóre dokumenty.

Nie jestem pewien, co kryjesz pod słowem „weryfikacja”, więc spróbuję. Być może możesz dodać coś o ilościowej weryfikacji Procesów Decyzji Markowa i zastosowaniu probabilistycznej logiki czasowej (pLTL i PCTL). W tej strukturze masz całkiem dobry sposób modelowania przeciwników, wyrażania właściwości i istnieje łatwe w użyciu narzędzia weryfikacyjne ( na przykład PRISM ).

Możesz także rzucić okiem na następujący kurs podyplomowy dotyczący protokołów bezpieczeństwa w Paryżu (tekst w większości po francusku):

http://mpri.master.univ-paris7.fr/C-2-30.html

Wykład na temat sprawdzalnego bezpieczeństwa może być interesujący, w szczególności z wykorzystaniem teorii gier. Myślę, że rozdziały 8 i 25 książki Nisan i wsp. Na temat algorytmicznej teorii gier mogłyby stanowić dobrą podstawę.

Chciałbym również zawrzeć krótki opis istniejących norm bezpieczeństwa / ochrony, takich jak ITSEC / TCSEC i wspólne kryteria. Zawsze warto zauważyć, że aby osiągnąć najwyższy poziom wspólnych kryteriów, należy formalnie zweryfikować, zaprojektować i przetestować system.