Развитие безрисковых и стабильных программных продуктов, возможно, станет
менее проблематичным после запуска адресованного сообществу разработчиков
программ с открытым исходным кодом проекта под названием Tokeneer. Автором этой
разработки выступает Агентство национальной безопасности США (NSA).
Права на запуск проекта Tokeneer были делегированы Агентству компанией Praxis
High Integrity Systems, цель - продемонстрировать миру образец разработки
безрисковых приложений. Проект, разработанный на основе методики этой компании
под названием Correctness by Construction (CbyC), использует язык
программирования SPARK Ada и среду разработки AdaCore GNAT Pro. Приведенные
образцы демонстрируют каким образом нужно выстраивать программу, чтобы она
отвечала требованиям стандарта Evaluation Assurance Level (EAL) 5, и, тем самым,
показывают возможное направление развития ПО в области его соответствия самым
высоким требованиям безопасности.
Tokeneer написан на высокоуровневом языке программирования SPARK Ada,
созданном специально для разработки безопасных приложений. И поскольку этот язык
является одной из разновидностей языка Ada, программы на основе SPARK, по сути
своей - это программы на Ada. Ada – весьма логичный выбор для отказоустойчивых,
высокоинтегрированных систем, поскольку он предлагает комбинацию гибкости,
надежности и простоты в использовании, а его вариант SPARK добавляет к этому
инструментарий статической верификации, позволяющий обеспечивать глубину,
прочность, эффективность и гарантию соответствия стандартам.
Проект нацелен как на индустриальное, так и на академическое сообщество, и
создает идеальные предпосылки для развития исследований в области безопасного
программирования, также он будет полезен преподавателям в качестве
высокотехнологичного инструментария для помощи в обучении.
Все материалы проекта, включая требования, цели, спецификации, модели
разработки, исходные коды и примеры доступны по этому
адресу.
