В эпоху стремительного развития технологий искусственного интеллекта, автономных систем и робототехники особое внимание уделяется безопасности и надежности встроенного программного обеспечения. Компания NVIDIA, мировой лидер в области графических процессоров и платформ для вычислений, сделала стратегический шаг в сторону улучшения безопасности, отказоустойчивости и функциональной безопасности своих критически важных программных продуктов, приняв решение применять язык программирования SPARK для разработки безопасного и надежного фирменного программного обеспечения. SPARK — это подмножество языка Ada, созданное с целью выполнения формальной верификации кода, позволяющее гарантировать отсутствие определенных типов ошибок и уязвимостей на уровне исходного кода. Применение SPARK в контексте безопасности программного обеспечения имеет решающее значение для таких секторов, как автомобильная промышленность, авиация и космическая отрасль, где ошибки кода могут привести к серьезным последствиям. NVIDIA использует свою новую программную платформу на базе SoC (система на кристалле), в которую входят ARM CPU, графический процессор, контроллер памяти и интерфейсы ввода-вывода, для создания специализированных встроенных систем.
Такие продукты как NVIDIA Jetson для встраиваемых вычислений с элементами искусственного интеллекта, NVIDIA DRIVE AGX для автономных транспортных средств и Isaac для робототехники базируются на этих технологиях. Важной особенностью стала возможность компиляции программного кода с использованием компиляторов GNAT Pro Ada и SPARK, которые обеспечивают поддержку как bare metal сред, так и операционных систем Linux и QNX. Это позволяет максимально эффективно интегрировать компоненты, написанные на SPARK, в широкий спектр программных решений NVIDIA. С внедрением SPARK происходит снижение количества уязвимостей в программном коде за счет формальной верификации, которая исключает такие проблемы как переполнение буфера, деление на ноль, обращение к неинициализированным переменным и другие распространенные ошибки программирования. Таким образом, NVIDIA не только создает программные продукты с повышенным уровнем безопасности, но и повышает их производительность, избавляясь от необходимости написания избыточного защитного кода.
Это, в свою очередь, сокращает нагрузку на процессор и улучшает отклик систем. Особое значение для NVIDIA имело соответствие международным стандартам безопасности, таким как ISO 26262, ориентированному на индустрию автомобилестроения, и IEC 61508 для общей функциональной безопасности. Компиляторы и инструменты верификации SPARK получили соответствующие квалификации и сертификаты, включая признание от TÜV SÜD — одного из ведущих мировых независимых органов по сертификации. Это гарантирует, что поставляемое программное обеспечение удовлетворяет самым строгим требованиям, предъявляемым к безопасности и надежности. Переход со стандартных языков программирования, таких как C и C++, на SPARK является серьезным вызовом для многих компаний, но NVIDIA сумела организовать плавную интеграцию благодаря высокой совместимости языков и развитым средствам взаимодействия между этими языками.
Это позволяет постепенно вводить SPARK в существующую кодовую базу без необходимости полного переписывания проектов, что существенно сокращает затраты на переход и обучение специалистов. С использованием SPARK компания NVIDIA также решила вопрос дефицита экспертов по программной безопасности, направив усилия на повышение автоматизации процесса выявления и устранения программных дефектов. Применение формальной верификации кода на ранних стадиях разработки позволяет обнаружить потенциальные ошибки до этапа тестирования, что обеспечивает значительную экономию ресурсов, снижающую общую стоимость создания продуктов и ускоряющую вывод их на рынок. Еще один важный аспект сотрудничества NVIDIA и AdaCore — поддержка разработок для графического процессора с использованием технологии CUDA. В бета-версии SPARK Ada на NVIDIA CUDA, появившейся в четвертом квартале 2020 года, предусмотрена возможность выполнения формально проверенного кода непосредственно на GPU, расширяя потенциал применения безопасного программирования в вычислительно емких задачах.
Истории успеха применений SPARK в различных индустриях подтверждают эффективность выбранного NVIDIA пути. Предприятия из автомобильного, аэрокосмического и медико-биологического сегментов уже добились заметных результатов в области повышения надежности и безопасности продуктов благодаря строгому контролю качества и автоматизированным методам верификации, предоставляемым инструментарием SPARK и Ada. В условиях возрастающих киберугроз и усложнения технологических систем переход на новые методики разработки программного обеспечения становится не просто желательным, а необходимым. Опыт NVIDIA является ярким примером того, как крупные корпорации могут успешно перестраивать свои процессы и технологии ради достижения целей высочайшей надежности и безопасности. Этот пример демонстрирует, что инвестиции в формально обоснованные языки и инструментальные средства разработки способны существенно повысить качество и конкурентоспособность конечных продуктов.
Таким образом, применение SPARK в компании NVIDIA становится не только решением текущих задач функциональной безопасности и надежности, но и точкой опоры для будущих инноваций в области встроенных систем. Это направление несет огромный потенциал для создания качественного программного обеспечения, устойчивого к кибератакам, с высокой гарантией отсутствия критических ошибок. Переход на новые языки программирования и методологии формальной верификации — это стратегический выбор, обеспечивающий лидирующие позиции на рынке и доверие конечных пользователей. Для разработчиков, инженеров и менеджеров, занимающихся безопасностью встроенного программного обеспечения, кейс NVIDIA по внедрению SPARK становится источником ценных знаний и вдохновения. Он демонстрирует, каким образом современные инструментальные средства могут помочь эффективно справляться с вызовами функциональной безопасности и кибербезопасности и одновременно снизить издержки разработки.
В условиях продолжающегося развития технологий автоматизации, автономии и искусственного интеллекта, будущее встроенного программного обеспечения тесно связано с применением формальных методов верификации и языков типа SPARK. NVIDIA своим примером прокладывает путь для других компаний, заинтересованных в создании максимально надежных и безопасных продуктов, способных достойно отвечать на вызовы цифровой эпохи.
