Владимир Буренков, разработчик-исследователь Лаборатория Касперского. Кандидат технических наук
Сфера научных интересов: методы и средства разработки и верификации микропроцессорных и программных систем.
Разработал ряд инструментов для верификации микропроцессоров с архитектурой "Эльбрус", а также метод формальной верификации протоколов когерентности памяти, применяемых в многопроцессорных системах. В Лаборатории Касперского занимается разработкой и анализом моделей и политик безопасности для систем, работающих под управлением операционной системы KasperskyOS.
Модели мандатного контроля целостности в операционных системах, как правило, накладывают ограничения на доступы активных компонент системы к пассивным и представляют эти доступы непосредственно. Такое представление можно использовать в случае операционных систем с монолитной архитектурой, где части системы, обеспечивающие доступ к ресурсам, входят в доверенную вычислительную базу. Однако доказательство отсутствия в ошибок в таких компонентах и, следовательно, соответствия модели реальной системе является чрезвычайно трудной задачей. KasperskyOS – операционная система, основанная на микроядре и позволяющая организовать доступ к ресурсам с помощью компонентов, не обязательно входящих в доверенную вычислительную базу. Для KasperskyOS разработана модель мандатного контроля целостности, учитывающая наличие таких компонентов и возможность их некорректного функционирования. В докладе представлен процесс формализации этой модели на языке Event-B и автоматизированного доказательства свойств, обеспечиваемых моделью.
