10 правил NASA для написания безопасного критического кода

Стандарты кодирования для критически важного ПО

Крупные проекты используют стандарты кодирования: структура кода, разрешенные/запрещенные фичи языка. Правил должно быть мало, они конкретны, понятны и запоминаемы.

NASA JPL фокусируется на C: мощные инструменты (статические анализаторы, модели, компиляторы, метрики). Критично там, где от кода зависят жизни: авиация, космос, АЭС.

10 правил от ведущего ученого JPL Джерарда Хольцманна. Фокус — безопасность. Применимы и к другим языкам.

Правило 1. Простой поток управления

Нет setjmp/longjmp, goto, прямой/косвенной рекурсии.

Почему: ясность кода, верифицируемость. Без рекурсии — нет циклов в графе вызовов. Все ограниченные выполнения остаются ограниченными.

Правило 2. Фиксированная верхняя граница циклов

У каждого цикла должна быть статически доказуемая фиксированная верхняя граница итераций. Если недоказуемо — нарушение.

Почему: границы циклов + нет рекурсии = нет беглого кода. Исключение: нетерминирующие циклы (планировщик) — должно быть статически доказуемо, что они не завершатся.

Правило 3. Нет динамического выделения памяти после инициализации

Никаких malloc, сборщиков мусора после старта.

Почему: непредсказуемое поведение аллокаторов, ошибки программиста (утечки, use-after-free, переполнение, запрос >доступно). Фиксированная предвыделенная память устраняет проблемы и упрощает верификацию. Стек вместо кучи.

Правило 4. Нет больших функций

Функция ≤ 60 строк (помещается на листе бумаги: 1 строка = 1 объявление/оператор).

Почему: длинные функции = плохая структура. Функция = логическая единица, понятная и верифицируемая. Многоэкранные единицы трудно понимать.

Правило 5. Минимальная плотность утверждений (assertions)

Минимум 2 ассерта на функцию в среднем. Boolean-тесты условий, которые «никогда не случаются». При срабатывании — явное восстановление. Если статический анализатор доказывает, что ассерт никогда не сработает или всегда верен — нарушение.

Почему: статистика: 1 дефект на 10–100 строк. Ассерты повышают перехват. Защитное кодирование: пред/пост-условия, параметры, возвращаемые значения, инварианты циклов. Можно отключить после тестов производительности.

Правило 6. Объявление данных на минимально возможной области видимости

Принцип сокрытия данных. Объекты объявляются в наименьшей возможной scope.

Почему: вне scope — нет доступа/испорчи. Предотвращает повторное использование переменных для несовместимых целей (сложная диагностика).

Правило 7. Проверка параметров и возвращаемых значений

Возвращаемое значение non-void функций проверяется каждым вызывающим. Валидность параметров проверяется внутри каждой функции.

Строго: даже printf, close. Допустимо явное приведение к void — программист намеренно игнорирует.

Почему: если реакция на ошибку = реакции на успех, всё равно нужно проверять (явное решение).

Правило 8. Ограниченное использование препроцессора

Только включение заголовков и определение макросов. Нет рекурсивных макросов, склеивания токенов, variadic аргументов. >1-2 условных компиляции — требуют обоснования и флага инструмента.

Почему: препроцессор мощен и неоднозначен — разрушает ясность, путает статические анализаторы. 10 директив = 1024 версии кода (2¹⁰) → взрыв тестирования.

Правило 9. Ограниченное использование указателей

Максимум 1 уровень разыменования. Никаких скрытых разыменований в typedef/макросах. Указатели на функции запрещены.

Почему: указатели легко ошибиться даже экспертам. Сложно تتبع поток данных статическим анализаторам. Указатели на функции блокируют проверки, делают доказательство отсутствия рекурсии невозможным.

Правило 10. Компиляция всего кода с первого дня

Компиляция с максимально строгими предупреждениями — ноль предупреждений. Ежедневная проверка ≥1 современным статическим анализатором — ноль предупреждений.

Почему: анализаторы доступны (в т.ч. бесплатно). Нет оправданий. Если анализатор путается — код переписывают до тривиальной валидности.