Компания AdaCore, производитель средств разработки и верификации ПО критических для безопасности встраиваемых систем, объявила о начале сотрудничества с корпорацией NVIDIA по применению языков программирования Ada и SPARK при разработке критического для информационной безопасности (security critical) ПО будущих систем-на-кристалле NVIDIA, построенных на базе новой открытой архитектуры RISC-V. Переходы NVIDIA на архитектуру RISC-V и на языки Ada и SPARK обусловлены возросшими требованиями к безопасности и защищенности ПО, предъявляемыми новыми ответственными применениями, такими как автоматизированные и автоматические транспортные средства. На странице www.adacore.com/resources можно загрузить руководство «AdaCore Technologies for Cyber Security» по применению языков Ada и SPARK и продуктов AdaCore для разработки ПО, критически важного для информационной безопасности.
Архитектура RISC-V разработана в Университете Беркли и поддерживается консорциумом RISC-V Foundation, объединяющим более 200 компаний, таких как NVIDIA, NXP, Marvell, Google, Thales, Samsung, Qualcomm и Western Digital. Недавно компания AdaCore стала членом консорциума RISC-V Foundation, и внесла свой вклад в поддержку архитектуры выпуском компиляторов GNAT Pro Ada и GNAT Pro C для 32-бит и 64-бит RISC-V, а также бесплатного варианта компилятора GNAT Community для 32-бит RISC-V.
Язык программирования Ada создавался специально для разработки ПО с повышенными требованиями к надежности, и в настоящее время Ada является основным языком для разработки ПО систем, критически важных для безопасности. Язык Ada является международным стандартом ISO 8652. В последней редакции стандарта ISO 8652-2012 (Ada 2012) введена конструкция для задания «контрактов» — требований к результатам работы программного модуля, описанных непосредственно в тексте программы на языке Ada. «Контракт» предназначен для использования компилятором для вставки динамических проверок или средствами статического анализа для формальной верификации. Язык SPARK является подмножеством Ada 2012, позволяющим проводить формальную верификацию ПО – доказательство математическими методами, что ПО делает то, что от него требуется и не делает того, что не требуется.
Недавно компания AdaCore завершила исследовательский проект, целью которого было продемонстрировать применение формальных методов для выполнения требований стандарта функциональной безопасности автомобильного ПО ISO 26262 в части обеспечения «Freedom from Interference» (Свободы от Вторжений) – защиты приложений с высоким уровнем критичности для безопасности ASIL (Automotive Safety Integrity Level) от влияния сбоев, возникших в приложениях с низким уровнем критичности ASIL, унаследованных (legacy) из предыдущих проектов и написанных на языке Си. В этом проекте компания AdaCore выступила не только поставщиком средств формальной верификации ПО на языке SPARK, но и разработчиком методологии создания «контрактов» для обеспечения требований Freedom from Interference в ISO 26262, а также технологии «гибридной верификации» — совмещения формальных методов с традиционной верификацией ПО, основанной на тестировании.
Комплекс инструментальных средств GNAT Pro Ada включает в себя компилятор, поддерживающий все версии стандартов Ada (Ada 83, Ada 95, Ada 2005 и Ada 2012), интегрированную среду разработки, визуальный отладчик, средства автоматизации тестирования, средства статического анализа (контроль стандартов кодирования, сбор метрик программного кода, анализатор стека), средства формальной верификации (доказательства корректности работы ПО с помощью математических методов) и средства интеграции Ada и C/C++ программ. Комплекс GNAT Pro Ada поддерживает микропроцессорные архитектуры x86, PowerPC, ARM и LEON. Поддерживаются целевые платформы с операционными системами LynxOS, PikeOS, QNX, VxWorks, Embedded Linux и без ОС (bare metal). Вариант GNAT Pro Assurance предназначен для разработки ПО систем, сертифицируемых по стандартам функциональной безопасности, таким как DO-178C (авионика), EN 50128 (ж/д системы), ISO 26262 (автоэлектроника) и ECSS-E-ST-40C/Q-ST-80C (космическая техника).
Другие продукты AdaCore: CodePeer — статический анализатор / детектор потенциальных ошибок и уязвимостей в программах на языке Ada, SPARK Pro – комплекс средств верификации ПО на языке SPARK – формально верифицируемом подмножестве языка Ada, QGen – квалифицируемый генератор программного кода на языках MISRA C и SPARK из моделей Simulink/Stateflow.
Дистрибьютор компании AdaCore в России – компания АВД Системы, поставщик средств разработки программного обеспечения критически важных для безопасности сертифицируемых встраиваемых компьютерных систем. Предлагаем предприятиям, заинтересованным в получении дополнительной информации о языках Ada и SPARK и современных технологиях разработки и верификации ПО, проведение бесплатного семинара.
