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

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