Разработчики из Австралии показали способ с помощью которого можно математически доказать стабильность, надежность и принципиальную возможность применения какого-либо программного обеспечения для решения критически важных задач. В частности это касается систем охраны и безопасности, используемых в самолетах и автомобилях.
Австралийская приватная организация Information and Communications Technology Centre of Excellence (Nicta) объявила на прошлой неделе о завершении разработки продукта для испытания надежности любого компьютерного кода. Их проект носит название secure embedded L4 (seL4).
Лоуренс Полсон (Lawrence Paulson), профессор вычислительной логики компьютерной лаборатории университета Кембридж, рассказал британским журналистам о том, что разработанная технология станет настоящим прорывом для бизнеса. «Я считаю, что в области ПО сейчас творится настоящий беспорядок. Если вы вообще используете компьютеры, то должны знать насколько ненадежными они порой бывают. Теперь у нас будет возможность изменить все к лучшему» — объяснил Полсон.
Главный научный сотрудник Nicta, Гервин Кляйн (Gerwin Klein), рассказал о том, что ранее разрабатываемые проекты такого рода специализировались на проверке конкретных отдельных сегментов ПО, однако сейчас его команде удалось сделать намного больше, разработать целостную систему верификации продуктов высокого уровня сложности, никогда ранее не существовавшую в мире.
Участники проекта Nicta утверждает, что большинство детских болезней программ, например возможность переполнения буфера, не ускользнут от проверки seL4.
Права на интеллектуальную собственность, созданную в Nicta, будут переданы в Open Kernel Labs для дальнейшего развития. Исследование заняло 4 года и было проведено 12 сотрудниками Nicta в сотрудничестве с университетом New South Wales.