Kurikulum: Metode Logis / Formal dalam Keamanan

22

Saat ini saya mengajar kursus kecil (Empat dua jam kuliah di tingkat Master) tentang Metode Logika dalam Keamanan , meskipun judul Metode Formal dalam Keamanan mungkin lebih tepat. Ini mencakup secara singkat topik-topik berikut (dengan metode logis terkait):

  • Manajemen Hak Digital dan Penegakan Kebijakan (formalisasi umum, logika modal, penegakan via automata)

  • Kode pembawa bukti dan otentikasi pembawa bukti (teori bukti, sistem logis, Curry-Howard Isomorphism, verifikasi)

  • Kontrol Akses (logika non-klasik, teori bukti)

  • Stack Inspection (semantik bahasa pemrograman, kesetaraan kontekstual, bisimulasi)

Tentu saja, program ini memiliki beberapa tujuan, di mana salah satunya menarik minat calon mahasiswa pascasarjana.

Di tahun-tahun mendatang kursus dapat diperluas ke kursus reguler, yang akan membutuhkan lebih banyak konten. Mengingat latar belakang orang-orang di sini sangat berbeda dengan saya, saya ingin tahu konten apa yang akan Anda sertakan dalam kursus semacam itu.

lo.logic cr.crypto-security teaching security formal-methods Dave Clarke
sumber

Jawaban:

15

Saya sarankan untuk membiasakan para siswa dengan logika berikut:

  • Logika epistemik: Digunakan untuk memodelkan pengetahuan berbagai pihak yang berpartisipasi dalam protokol, dan membuktikan bahwa musuh tidak dapat memperoleh pengetahuan tentang suatu rahasia.
  • BAN logic: Logika lama untuk membuktikan berbagai properti protokol otentikasi. ( Logika kepercayaan lain juga cocok.)
  • Logika untuk sistem transisi: Ini termasuk logika seperti LTL, CTL, dan LTL *. (Logika tersebut bekerja pada model protokol Kripke-like.)
  • Aljabar proses: Beberapa aljabar proses, seperti Spi-calculus (atau CSP , dan alat terkait keamanannya, Casper ) berguna untuk memodelkan protokol keamanan.
  • Memperkenalkan alat seperti AVISPA dari NuSMV sangat berguna.
  • Saya juga menyarankan Kebenaran Resmi Protokol Keamanan sebagai salah satu buku pelajaran saja.

Seorang teman saya, Morteza Amini , baru-baru ini mendapatkan gelar Ph.D. pada pemodelan kontrol akses dengan logika. Dia menyusun logika baru, bernama , yang merupakan singkatan dari "multi-authority deontic logic dan description description." Seperti namanya, ini menggabungkan dua logika non-klasik (logika deontik + logika deskripsi) untuk memutuskan apakah suatu entitas memiliki akses ke objek. Jika Anda suka, saya dapat mendorongnya untuk memberikan informasi lebih lanjut.M.SEBUAH(DL.)2

MS Dousti
sumber
Terima kasih Sadeq. Pada tahun-tahun sebelumnya saya membahas Logika Epistemik dalam pengantar saya untuk Modal Logic untuk kursus, tapi saya menjatuhkannya tahun ini. Siswa sering memilih logika BAN untuk topik esai. Saran lainnya sangat berguna, terutama alat, yang selalu menyarankan kemungkinan tugas siswa.
Dave Clarke
@ Dave: Senang mendengarnya! Saya pernah mengambil bagian dalam kursus kilat yang sangat baik (~ 3 jam) pada "Logika Epistemik untuk Protokol Keamanan" oleh Dr. Ramaznian. Presentasi dapat ditemukan di sini: ifile.it/xljn9s8/EpistemicLogic.rar . Saya sarankan melihat itu, sebelum menjatuhkan topik sama sekali.
MS Dousti
Terima kasih untuk tautannya. Logika Epistemik belum sepenuhnya dijatuhkan; itu tidak cocok tahun ini.
Dave Clarke
12

Ada kursus membaca di Carnegie Mellon beberapa tahun yang lalu, Languages ​​and Logics for Security , yang mencoba mensurvei beberapa literatur dalam otentikasi, otorisasi, aliran informasi, kalkuli protokol, perlindungan, dan manajemen kepercayaan; halaman web kursus memiliki slide untuk makalah yang kami diskusikan serta daftar referensi lebih lanjut untuk setiap topik. Aliran informasi khususnya mungkin sesuatu yang layak untuk dilihat relatif terhadap topik yang Anda daftarkan.

Kurikulum untuk kursus Anupam Datta, Yayasan Keamanan dan Privasi juga relevan.

Rob Simmons
sumber
Rob terima kasih. Sebenarnya saya menggunakan dua halaman ini ketika saya mendesain konten kursus asli.
Dave Clarke
Aah. Kalau begitu saya kira utilitas tambahan untuk Anda terbatas! Semoga orang lain akan merasakan manfaatnya juga :).
Rob Simmons
10

Jawaban Rob mengingatkan saya pada kelompok membaca Cornell yang serupa yang diorganisasi Michael Clarkson selama beberapa tahun: Kelompok Diskusi Keamanan Cornell . Mungkin perlu membaca sekilas di sana untuk beberapa kertas.

Tandai Reitblatt
sumber
6

Saya tidak yakin dengan apa yang Anda sembunyikan di bawah kata "verifikasi" jadi saya coba. Mungkin Anda dapat menambahkan sesuatu tentang verifikasi kuantitatif Proses Keputusan Markov dan penggunaan logika temporal probabilistik (pLTL dan PCTL). Dalam kerangka ini Anda memiliki cara yang cukup baik untuk memodelkan musuh, mengekspresikan properti, dan ada alat verifikasi yang mudah digunakan ( misalnya, PRISM ).

Sylvain Peyronnet
sumber
Menarik. Apakah Anda tahu ada aplikasi keamanan PRISM atau logika ini?
Dave Clarke
dalam studi kasus ( prismmodelchecker.org/casestudies/index.php ), ada beberapa contoh yang terkait dengan keamanan. Sebagian besar dari mereka adalah MDP tetapi lebih tentang keamanan protokol daripada keamanan implementasi.
Sylvain Peyronnet
1

Ceramah tentang Keamanan yang Dapat Dibuktikan bisa menarik, khususnya menggunakan Teori Permainan. Saya berpikir bahwa Bab 8 dan 25 dari buku Nisan et al tentang Teori Permainan Algoritma dapat memberikan dasar yang baik.

Saya juga akan memasukkan deskripsi singkat tentang standar keamanan / keselamatan yang ada, seperti ITSEC / TCSEC dan Kriteria Umum. Itu selalu baik untuk menunjukkan bahwa untuk mencapai tingkat tertinggi dari Kriteria Umum, perlu secara formal memverifikasi, merancang dan menguji suatu sistem.

Charles
sumber