Компьютер дал неожиданный сбой…  В некоторых случаях такая ситуация может показаться концом света. Нет ничего хуже, например, чем катастрофа в компьютерных системах, работающих в спасательных медицинских приборах, системах управления дорожным транспортом или сложными технологическими процессами.

Исследователи из Национального исследовательского центра информационных технологий Австралии (NCITA) работают над проблемой защиты от подобных аварий. Джуна Андроник (June Andronick) и ее команда занимаются разработкой ядра операционной системы, поставив перед собой задачу спроектировать ОС, не подверженную падениям.

Сушествующая методика создания надежного программного обеспечения основана на методе проб и ошибок, когда разработчики ПО предусматривают максимальное количество возможных ситуаций, после чего запускают тесты. NCITA работает по методике формальной верификации, которая до этого считалась непригодной для практического применения.

Однако Ардроник и ее коллеги смогли использовать эту методику для формальной проверки кода, который составляет большую часть ядра операционной системы, предназначенной для процессоров, применяемых в смартфонах, портативных машинах и медицинском оборудовании.

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

Эта технология также может помочь защититься от кибер-атак, так как операционная система может блокировать несанкционированные действия, которые выдаются программным обеспечением.

В результате команда Джуны Андроник сумела написать небольшую операционную систему, которая всегда будет вести себя точно так, как предусмотрели ее разработчики, не подвергаясь сбоям (за исключением случаев неправильной установки оборудования).