Формальная верификация операционных систем

Операционные системы и их ядра лежат в основе любых программных систем и оказывают важнейшее влияние на их устойчивость и безопасность (и в смысле security, и в смысле safety). Но как мы можем доверять операционным системам? Нет ли в их реализации (разумеется, на безумной смеси С и языка ассемблера) ошибок? Не приведут ли эти ошибки к нарушениям в функционировании программной системы в целом? В этом докладе мы поговорим о том, что такое ядро операционной системы и как оно устроено, пройдёмся по проектам последнего десятилетия по формальной верификации ядер операционных систем и выясним, каков текущий прогресс в этой области. Мы также познакомимся с инструментарием формальной верификации, узнаем, почему ему можно доверять, и обсудим, как во всё это вкатываться, если вам вдруг станет ясно, что ничем другим заниматься уже и не хочется.


Виталий Брагилевский,

JetBrains

@_bravit
Формальная верификация операционных систем
Виталий Брагилевский,
JetBrains
@_bravit
Операционные системы и их ядра лежат в основе любых программных систем и оказывают важнейшее влияние на их устойчивость и безопасность (и в смысле security, и в смысле safety). Но как мы можем доверять операционным системам? Нет ли в их реализации (разумеется, на безумной смеси С и языка ассемблера) ошибок? Не приведут ли эти ошибки к нарушениям в функционировании программной системы в целом? В этом докладе мы поговорим о том, что такое ядро операционной системы и как оно устроено, пройдёмся по проектам последнего десятилетия по формальной верификации ядер операционных систем и выясним, каков текущий прогресс в этой области. Мы также познакомимся с инструментарием формальной верификации, узнаем, почему ему можно доверять, и обсудим, как во всё это вкатываться, если вам вдруг станет ясно, что ничем другим заниматься уже и не хочется.
О докладчике
О докладчике
Разработчик JetBrains, преподаватель факультета математики и компьютерных наук СПбГУ, член наблюдательного комитета по разработке компилятора GHC языка Haskell, автор книги «Haskell in Depth».
Все спикеры SnowOne
Все спикеры SnowOne
Click to order
Total: 
Пришлём подтверждение оплаты на указанную почту в течение 30 минут
Имя
Фамилия
Компания
Должность
E-mail
Оплачивая участие, вы соглашаетесь на обработку персональных данных и с условиями пользования сайтом