Аспирантский семинар: Формальная верификация модуля безопасности ядра Linux / Выбор контрольных точек проектов с учетом возможного изменения состава работ

Место: Факультет компьютерных наук, Кочновский проезд, д. 3, ауд. 317
Время: 16 июня, 18:30 – 20:00 

Доклады состоятся в рамках научно-исследовательского семинара аспирантской школы по компьютерным наукам.

Первый доклад

Тема:  Формальная верификация модуля безопасности ядра Linux
Докладчик:  Денис Ефремов, аспирант первого года обучения, базовая кафедра "Системное программирование" ИСП РАН факультета компьютерных наук

Формальной верификацией называют доказательство соответствия предмета верификации его формальному описанию. В данном случае предметом верификации выступает модуль (драйвер) ядра Linux, описанием является математическая модель требований по доступу к информации. В ходе доклада будут затронуты темы формальной верификации математической модели системы безопасности, верификации её реализации в виде модуля безопасности ядра Linux и вопросы проверки соответствия модели и реализации. Будут представлены текущие результаты работы над проектом по формальной верификации модуля безопасности Parsec операционной системы специального назначения Astra Linux.
 

Второй доклад

Тема: Выбор контрольных точек проектов с учетом возможного изменения состава работ
Докладчик:  Максим Марон, аспирант второго года обучения, кафедра бизнес-аналитики школы бизнес-информатики факультета бизнеса и менеджмента

Доклад посвящен проблеме контроля реализации мультисценарных проектов, при планировании которых необходимо предусмотреть не один, а несколько сценариев выполнения, отличающихся друг от друга составом работ. В качестве метода контроля предлагается проведение промежуточных проверок. Задача состоит в том, чтобы определить после выполнения каких работ эти проверки необходимо осуществлять.

Предложено решение для двух наиболее важных практических случаев: когда число допустимых промежуточных проверок задано, и когда их число не задается, но требуется достижение определенного уровня информационной полноты контроля.