Ефремов Денис

Закончил ВМиК МГУ им. М.В. Ломоносова в 2011 году. Основная область деятельности - формальная верификация кода, разработка статических и динамических анализаторов. Разработчик ядра ОС Linux, мейнтейнер флоппи драйвера.

Тема: «Формальная верификация программного кода механизмов защиты операционных систем». 

Аннотация к докладу

В докладе будет рассказано как строится процесс разработки спецификаций на код модуля безопасности ядра ОС Linux. Будет описан процесс последовательного уточнения спецификаций и их доказательства от минимальных, гарантирующих отсутствие в коде некоторых классов ошибок времени выполнения языка Си, до полных, включающих в себя требования высокоуровневой модели, описанной, например, на Event-B/Rodin. Будет рассмотрен использующийся инструментарий Frama-C/ACSL, его достоинства и недостатки.