Program: Logiczne / formalne metody bezpieczeństwa

22

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.

Dave Clarke
źródło

Odpowiedzi:

15

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

MS Dousti
źródło
Dzięki Sadeq. We wcześniejszych latach omawiałem Epistemiczną Logikę we wprowadzeniu do Logiki Modalnej na kurs, ale w tym roku porzuciłem ją. Student często wybiera logikę BAN dla tematu eseju. Inne sugestie są bardzo przydatne, zwłaszcza narzędzia, które zawsze sugerują możliwe zadania dla studentów.
Dave Clarke
@Dave: Miło to słyszeć! Raz brałem udział w doskonałym kursie awaryjnym (~ 3 godz.) Na temat „Logiki epistemicznej protokołów bezpieczeństwa” dr. Ramazniana. Prezentację można znaleźć tutaj: ifile.it/xljn9s8/EpistemicLogic.rar . Proponuję przyjrzeć się temu, zanim całkowicie zrezygnuję z tematu.
MS Dousti
Dzięki za link. Logika epistemiczna nie została całkowicie odrzucona; po prostu nie pasowało w tym roku.
Dave Clarke
12

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 .

Rob Simmons
źródło
Dzięki, Rob. W rzeczywistości skorzystałem z tych dwóch stron, projektując oryginalną treść kursu.
Dave Clarke
Aaa Myślę, że jego dodatkowe narzędzie jest dla ciebie ograniczone! Mam nadzieję, że inni też się przydadzą :).
Rob Simmons,
10

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.

Mark Reitblatt
źródło
6

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 ).

Sylvain Peyronnet
źródło
Ciekawy. Czy znasz jakieś aplikacje bezpieczeństwa PRISM lub te logikę?
Dave Clarke
w studiach przypadków ( prismmodelchecker.org/casestudies/index.php ) istnieje kilka przykładów związanych z bezpieczeństwem. Większość z nich to MDP, ale bardziej dotyczy bezpieczeństwa protokołów niż bezpieczeństwa implementacji.
Sylvain Peyronnet,
1

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.

Charles
źródło