Ученые из австралийского исследовательского центра NICTA нашли способ математически доказать, что определенное ПО не содержит ошибок и, соответственно, не станет причиной отказа управляемого им оборудования. Проведение такого рода тестирования жизненно необходимо во многих отраслях промышленности, таких как, например, авиа и автомобилестроение, где сбои в бортовой компьютерной сети возникают чаще, чем поломки механических агрегатов.
Для проведения теста было взято микроядро Secure Embedded L4 (seL4), содержащее 8700 строк кода базирующегося на open source проекте OKL4. Ядро является ключевым компонентом любых современных встраиваемых устройств, и имеет неограниченный доступ ко всем работающим системам. Суть тестирования заключалась в том, чтобы доказать, что написанный код удовлетворяет всем тем спецификациям, которые были заложены на этапе проектирования. В результате, испытание было пройдено успешно и достигнуто 100% соответствие предъявляемым требованиям.
Работой по формулировке алгоритма математического доказательства в течение четырех лет занималась команда из 12 исследователей NICTA, аспирантов и техников. Они успешно проверили более 10 тыс. промежуточных теорем, изучив более чем 200 тыс. строк кода. Итоговый анализ выполняется с помощью интерактивной программы Isabelle, и на сегодняшний день является самой объемной автоматизированной проверкой выполнения условий теорем.
Наряду с доказательством соответствия программного кода выполняемым функциям, тестирование показало, что seL4 не подвержен большинству известных хакерских атак. Например, атака «переполнение буфера», позволяющая внедрить злонамеренный код и захватить управление работой ядром, не даст результата.
Полное изложение работы исследователей будет озвучено на 22-ом симпозиуме, посвященном принципам работы операционных систем (SOSP). Также ожидается, что NICTA передаст все интеллектуальные права на результаты исследования opensource компании Open Kernel Labs.
14.08.2009