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

22

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

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

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

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

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

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

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

Дэйв Кларк
источник

Ответы:

15

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

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

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

М.С. Дусти
источник
Спасибо Садек. В более ранние годы я освещал Epistemic Logic в своем введении в Modal Logic для курса, но в этом году я отказался от него. Студент часто выбирает логику БАН для темы эссе. Другие предложения очень полезны, особенно инструменты, которые всегда предлагают возможные задания для студентов.
Дэйв Кларк
@Dave: Рад это слышать! Однажды я принял участие в отличном ускоренном курсе (~ 3 часа) на тему «Эпистемическая логика для протоколов безопасности» доктора Рамазняна. Презентацию можно найти здесь: ifile.it/xljn9s8/EpistemicLogic.rar . Я предлагаю взглянуть на это, прежде чем полностью отказаться от темы.
MS Dousti
Спасибо за ссылку. Эпистемическая логика не была отброшена полностью; это просто не подходило в этом году.
Дэйв Кларк
12

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

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

Роб Симмонс
источник
Спасибо, Роб. Фактически, я использовал эти две страницы, когда разработал оригинальное содержание курса.
Дэйв Кларк
Ааа. Ну тогда я предполагаю, что его дополнительная полезность для вас ограничена! Надеюсь, другие тоже найдут это полезным :).
Роб Симмонс
6

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

Сильвен Пейроннет
источник
Интересный. Знаете ли вы какие-либо приложения безопасности PRISM или эти логики?
Дэйв Кларк
В тематических исследованиях ( prismmodelchecker.org/casestudies/index.php ) есть несколько примеров, связанных с безопасностью. Большинство из них - MDP, но это больше касается безопасности протоколов, чем безопасности реализаций.
Сильвен Пейроннет
3

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

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

Стефан Чобака
источник
Говорить по-французски ...
Дейв Кларк
Эта ссылка ведет на английскую версию: mpri.master.univ-paris7.fr/C-2-30en.html
Сильвен,
1

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

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

Чарльз
источник