Учебный план: логические / формальные методы в безопасности

В настоящее время я преподаю небольшой курс (четыре двухчасовых лекции на уровне магистратуры) по логическим методам в безопасности , хотя название « Формальные методы в безопасности» может быть более подходящим. В нем кратко рассматриваются следующие темы (с соответствующими логическими методами):

• Управление цифровыми правами и применение политик (общая формализация, модальная логика, принудительное применение с помощью автоматов)

• Код с доказательством и проверка подлинности с доказательством (теория доказательств, логические системы, изоморфизм Карри-Говарда, проверка)

• Контроль доступа (неклассическая логика, теория доказательств)

• Проверка стека (семантика языка программирования, контекстная эквивалентность, бисимуляция)

Естественно, курс имеет несколько целей, одна из которых - привлечение потенциальных аспирантов.

В ближайшие годы курс может быть расширен до обычного курса, для которого потребуется больше контента. Учитывая, что опыт людей здесь сильно отличается от моего, я хотел бы знать, какой контент вы бы включили в такой курс.

Предлагаю ознакомить студентов со следующей логикой:

• Эпистемическая логика: Используется для моделирования знаний различных сторон, участвующих в протоколе, и доказывает, что противник не может получить знания какой-либо тайны.
• Логика BAN: старая логика для проверки различных свойств протоколов аутентификации. (Другие логики верования также уместны.)
• Логика для систем перехода. Сюда входят такие логики, как LTL, CTL и LTL *. (такая логика действует на Kripke-подобных моделях протокола.)
• Алгебры процессов. Некоторые алгебры процессов, такие как Spi-calculus (или CSP , и его связанный с безопасностью инструмент Casper ), полезны для моделирования протоколов безопасности.
• Введение инструменты , такие как Avispa из NuSMV очень полезны.
• Я также предлагаю Формальную правильность протоколов безопасности в качестве одного из учебников курса.

Мой друг, Мортеза Амини , недавно получил докторскую степень. по моделированию контроля доступа с логикой. Он разработал новую логику под названием , которая означает «многоуровневая деонтическая логика и логика описания». Как следует из названия, оно объединяет две неклассические логики (деонтическая логика + логика описания), чтобы решить, имеет ли объект доступ к объекту. Если хотите, я могу побудить его предоставить больше информации.$MA(DL)^2$

Несколько лет назад в Carnegie Mellon проводился курс чтения « Languages ​​and Logics for Security» («Языки и логика для безопасности») , в ходе которого была предпринята попытка изучить некоторую литературу по аутентификации, авторизации, обмену информацией, исчислениям протоколов, защите и доверительному управлению; На веб-странице курса есть слайды для статей, которые мы обсуждали, а также список литературы по каждой теме. В частности, поток информации может стоить взглянуть на те темы, которые вы перечислили.

Учебный план курса Anupam Datta « Основы безопасности и конфиденциальности» также имеет значение.

Ответ Роба напомнил мне о подобной группе по чтению Корнелла, которую Майкл Кларксон организовал в течение нескольких лет: дискуссионная группа по безопасности Корнелла . Возможно, стоит пролистать там бумаги.

Я не уверен, что вы скрываете под словом «проверка», поэтому я попробую. Может быть, вы можете добавить что-то о количественной проверке процессов принятия решений Маркова и использовании вероятностной временной логики (pLTL и PCTL). В этой среде у вас есть очень хороший способ моделирования противников, выражения свойств, и существуют простые в использовании инструменты проверки ( например, PRISM ).

Вы также можете взглянуть на следующий курс для аспирантов по протоколам безопасности в Париже (текст в основном на французском):

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

Лекция по Provable Security может быть интересной, в частности, с использованием теории игр. Я думаю, что главы 8 и 25 книги Nisan et al., Посвященной теории алгоритмических игр, могли бы послужить хорошей основой.

Я также включил бы краткое описание существующих стандартов безопасности / безопасности, таких как ITSEC / TCSEC и Common Criteria. Всегда приятно отметить, что для достижения наивысшего уровня Общих критериев необходимо формально проверить, спроектировать и протестировать систему.