NVIDIA начала отказываться от C в критичных модулях ради безопасности — Tproger

От
admin
-
0
16

Вместо этого компания сделала ставку на SPARK

NVIDIA совместно с AdaCore опубликовала кейс, который показывает: компания активно внедряет формально верифицированный код на языке SPARK вместо традиционного C в критически важных модулях.

Причина — невозможность гарантировать безопасность через тестирование.

Тестировать безопасность невозможно. Нельзя понять, когда ты действительно закончилДэниел Рорервице-президент NVIDIA по безопасности ПО

Почему C больше не устраивает

На фоне усиления киберугроз, в NVIDIA начали пересматривать подходы к разработке и верификации ПО.

Тестирование, считают в компании, не может гарантировать безопасность — оно дает понимание качества функциональности, но не защищенности. Поэтому ставка была сделана на доказуемость поведения кода — через формальную верификацию.

Что такое SPARK и как его внедрили

SPARK — это строго типизированный, безопасный для памяти подмножество языка Ada, предназначенный для написания кода, который можно формально верифицировать. Такие программы можно математически доказать на предмет корректности, отсутствия ошибок и уязвимостей — задолго до запуска.

Почему GenAI не поможет IT-бизнесу без базы знанийtproger.ru

Читать также:
S.T.A.L.K.E.R. 2: Heart of Chornobyl получила уже третий патч за неделю

Еще в 2018 году NVIDIA провела proof-of-concept: две низкоуровневые, чувствительные к безопасности C-программы были переписаны на SPARK за три месяца. Итоги оказались настолько успешными, что спустя несколько лет:

  • в SPARK пишутся целые модули коммерческих продуктов NVIDIA;
  • обучено более 50 разработчиков;
  • верификация значительно упростила процессы аудита и укрепила доверие клиентов.

«Мы не просто запустили инструмент поиска багов — мы формально верифицировали этот код. Это сильно повышает доверие со стороны клиентов», — отмечается в кейсе.

Возражения скептиков развеялись

Переход с C на SPARK изначально вызывал сомнения внутри компании. Однако практический опыт показал:

  • производительность не упала: «разницы с C не заметили», — признались разработчики;
  • формальная верификация сократила затраты на аудиты;
  • некоторые изначальные критики стали активными сторонниками подхода.

Что дальше

Хотя SPARK пока используется точечно, его уже применяют в чувствительных к безопасности частях — там, где традиционные языки и методы верификации не дают нужного уровня уверенности. NVIDIA делает ставку на переход от тестов к доказательствам.

Стоил ли переход того?По-моему, ерунда. Усложнение того, что усложнять не надоОтличный подход. Могут себе позволить

ЭТО МОЖЕТ БЫТЬ ИНТЕРЕСНОЕЩЕ ОТ АВТОРА