Почему использование шаблона C++ не рекомендуется в космической/излучаемой среде?

Обратите внимание, что совместимые с пространством (стойкие к излучению, аэронавтике) вычислительные устройства очень дороги (в том числе для запуск в космос, так как их вес превышает килограммы), и что одна космическая миссия стоит, возможно, сотни миллионов евро или долларов США. Потеря миссии из-за проблем с программным обеспечением или компьютером, как правило, влечет за собой непомерно высокие затраты, поэтому неприемлема и оправдывает дорогостоящие методы и процедуры разработки, о которых вы даже не мечтаете использовать для разработки апплета для мобильного телефона, а также использование вероятностные рассуждения и инженерные подходы рекомендуются, поскольку космические лучи до сих пор являются каким-то "необычным" событием. С высокоуровневой точки зрения космические лучи и производимое ими переворачивание битов можно рассматривать как шум в некоторой абстрактной форме сигнала или входных данных. Вы можете рассматривать проблему «случайного переключения битов» как отношение сигнал/шум проблема, то рандомизированные алгоритмы могут обеспечить полезную концептуальную основу (особенно на метауровне, то есть при анализе критического для безопасности исходного кода или скомпилированного бинарного файла, а также во время критически важного времени выполнения системы в каком-либо сложном ядре или потоке планировщик), с теория информации точка зрения.

Почему использование шаблона C++ не рекомендуется в космической/радиоактивной среде?

Эта рекомендация является обобщением для C++ MISRA C правил кодирования и правил Embedded C++, а также Рекомендации DO178C, и это связано не с излучением, а со встроенными системами. Из-за ограничений по излучению и вибрации встроенное оборудование любого ракетно-космического компьютера должно быть очень небольшим (например, по экономическим причинам и причинам энергопотребления, оно более — по мощности компьютера — похоже на Raspberry Pi). системы, чем большая серверная система x86). Закаленные в космосе чипы стоят в 1000 раз дороже, чем их гражданские аналоги. И вычисление WCET на компьютерах, встроенных в космос, по-прежнему является технической проблемой (например, из-за < проблемы, связанные с href="https://en.wikipedia.org/wiki/CPU_cache" rel="noreferrer">кэшем ЦП). Следовательно, выделение кучи не одобряется в критически важные с точки зрения безопасности встроенные системы с интенсивным использованием программного обеспечения (как бы вы справились с нехваткой памяти в них? Или как бы вы доказали что у вас достаточно оперативной памяти для всех случаев реального времени выполнения?)

Помните, что в критическом мире программного обеспечения вы не только каким-то образом "гарантируете" или "обещаете" , и, конечно же, оценить (часто с некоторыми умными вероятностными рассуждениями) качество вашего собственного программного обеспечения, а также всех программных инструментов, используемых для его создания (в частности: вашего компилятора и вашего компоновщика; Boeing или Airbus не будут менять свою версию кросс-компилятора GCC, используемого для компиляции их программного обеспечения для управления полетом без предварительного письменного разрешения от например, FAA или DGAC). Большинство ваших программных инструментов должны быть так или иначе одобрены или сертифицированы.

Имейте в виду, что на практике большинство шаблонов C++ (но, конечно, не все) внутренне используют кучу. И стандартные C++ контейнеры, безусловно, подходят. Написание шаблонов, которые никогда не используют кучу, — сложное занятие. Если вы на это способны, вы можете безопасно использовать шаблоны (при условии, что вы доверяете своему компилятору C++ и его механизму расширения шаблонов, который является самой сложной частью внешнего интерфейса C++ большинства последних компиляторов C++, например, GCC или Клэнг).

Я предполагаю, что по аналогичным причинам (надежность набора инструментов) не одобряется использование многих генерации исходного кода инструменты (выполнение некоторых видов метапрограммирования, например создание кода C++ или C). Обратите внимание, например, что если вы используете bison (или RPCGEN) в некоторых важных для безопасности программах (составленных make и gcc) вам необходимо оценить (и, возможно, тщательно протестировать) не только gcc и make, но и bison. Это инженерная причина, а не научная. Обратите внимание, что некоторые встроенные системы могут использовать рандомизированные алгоритмы, в частности, для разумной работы с шумные входные сигналы (возможно, даже случайные перевороты битов из-за достаточно редких космических лучей). Доказательство, тестирование или анализ (или просто оценка) таких алгоритмов на основе случайных чисел — довольно сложная тема.

Ознакомьтесь также с Frama-Clang и CompCert и обратите внимание на следующее:

• C++11 (или последующие) это ужасно сложный язык программирования. У него нет полной формальной семантики. Людей, достаточно разбирающихся в C++, всего несколько десятков по всему миру (вероятно, большинство из них входит в его комитет по стандартизации). Я умею программировать на C++, но не могу объяснить все тонкости семантики перемещения или модель памяти. Кроме того, C++ на практике требует множества оптимизаций для эффективного использования.

• Очень сложно сделать безошибочный компилятор C++, в частности потому, что C++ практически требует сложного оптимизации, а также из-за сложности спецификации C++. Но текущие (например, недавние GCC или Clang) на практике довольно хороши, и у них мало (но все же есть) остаточных ошибок компилятора. CompCert++ для C++ еще нет, и для его создания требуется несколько миллионов евро или долларов США (но если вы можете собрать такую ​​сумму денег, свяжитесь с меня по электронной почте, например, на [email protected], мой рабочий адрес). А индустрия космического программного обеспечения чрезвычайно консервативна.

• Сложно создать хороший распределитель кучи памяти C или C++. Кодирование — это вопрос компромиссов. В шутку рассмотрите возможность адаптации этого распределителя кучи C к C++.

• подтверждение свойств безопасности (в частности, отсутствие условий гонки или неопределенное поведение (например, переполнение буфера во время выполнения) кода C++, связанного с шаблонами, по-прежнему, во 2 квартале 2019 г., немного опережая уровень развития статического анализа программ C++ код. Мой черновик технического отчета Bismon (это черновик отчета H2020, поэтому пропустите страницы для европейских бюрократов) есть несколько страниц, объясняющих это более подробно. Знайте теорему Райса.

• тестирование встроенного программного обеспечения C++ для всей системы может потребовать запуска ракеты (как Ariane 5 испытательный полет 501 или, по крайней мере, сложные и тяжелые эксперименты в лаборатории). Это очень дорого. Даже тестирование на Земле марсохода требует много денег. .

Подумайте об этом: вы пишете какое-то критичное для безопасности встроенное программное обеспечение (например, для торможения поездов, автономных транспортных средств, автономных дронов, большой нефтяной платформы или нефтеперерабатывающего завода, ракет и т. д.). Вы наивно используете стандартный контейнер С++, например. некоторые std::map<std::string,long>. Что должно произойти при нехватке памяти? Как вы «докажете» или, по крайней мере, «убедите» людей, работающих в организациях, финансирующих космическую ракету стоимостью 100 миллионов евро, что ваше встроенное программное обеспечение (включая компилятор, использованный для его создания) достаточно хорошо? Правило десятилетней давности запрещало любое динамическое выделение кучи.

Я говорю не о сложных материалах стандартной библиотеки, а о специально созданных пользовательских шаблонах.

Даже их трудно доказать или, в более общем плане, оценить их качество (и вы, вероятно, захотите использовать свои собственные распределитель внутри них). В космосе пространство кода является сильным ограничением. Таким образом, вы должны скомпилировать, например, g++ -Os -Wall или clang++ -Os -Wall. Но как вы доказали — или просто протестировали — все тонкие оптимизации, сделанные -Os (и они специфичны для вашей версии GCC или Clang)? Ваша космическая организация спросит вас об этом, поскольку любая ошибка во встроенном космическом программном обеспечении C++ может привести к сбою миссии (прочитайте еще раз о Первый полет Ariane 5 сбой - закодировано на каком-то диалекте Ады, которая в то время имела "лучшую" и "более безопасную" систему типов, чем C++17 сегодня), но не Не смейтесь слишком много над европейцами. Boeing 737 MAX с его MACS является похожий беспорядок).

Моя личная рекомендация (но, пожалуйста, не относитесь к этому слишком серьезно. В 2019 году это больше игра слов, чем что-либо еще) — рассмотреть возможность кодирования вашего встроенного программного обеспечения в Rust. Потому что он немного безопаснее, чем C++. Конечно, вам придется потратить от 5 до 10 миллионов евро (или миллионов долларов США) за 5 или 7 лет, чтобы получить хороший компилятор Rust, подходящий для космических компьютеров (опять же, пожалуйста, свяжитесь со мной как с профессионалом, если вы способны потратить эти деньги). много на бесплатном программном компиляторе Compcert/Rust). Но это всего лишь вопрос разработки программного обеспечения и управления программными проектами (читайте Мифический Месяц и Бредовые вакансии, чтобы узнать больше , помните также о принципе Дилберта: он применим как к индустрии космического программного обеспечения, так и к индустрии встроенных компиляторов. , как и все остальное).

Мое твердое и личное мнение состоит в том, что Европейская комиссия должна финансировать (например, через Horizon Europe) бесплатное программное обеспечение CompCert++ (или даже лучше, Compcert/Rust) как проект (и такой проект потребует больше более 5 лет и более 5 высококлассных, кандидатов наук). Но в возрасте 60 лет я, к сожалению, знаю, что этого не произойдет (поскольку идеология ЕС, по понятным причинам в основном вдохновленная политикой Германии, по-прежнему является иллюзией Конец истории, поэтому H2020 и Horizon Europe на практике в основном представляют собой способ оптимизации налогов для корпораций в Европе посредством Европейские налоговые гавани), и это после нескольких частных обсуждений с несколькими участниками проекта CompCert. К сожалению, я ожидаю, что DARPA или NASA с гораздо большей вероятностью будет финансировать какой-либо будущий проект CompCert/Rust (чем его финансирует ЕС).

NB. Европейская авиационная промышленность (в основном Airbus) использует гораздо больше формальных методов, чем североамериканская ( Боинг). Следовательно, некоторых (не всех) модульных тестов избегают (поскольку они заменяются формальными проверками исходного кода, возможно, с помощью таких инструментов, как Frama-C или Astrée — ни один из них не был сертифицирован для C++, только для подмножества C, запрещающего динамическое выделение памяти C и некоторые другие особенности языка C). И это разрешено DO-178C (а не предшественником DO-178B) и одобрен французским регулирующим органом, DGAC (и, я думаю, другими европейскими регулирующими органами).

Также обратите внимание, что многие конференции SIGPLAN косвенно связаны с вопросом ОП.

Аргумент против использования шаблонов в коде безопасности состоит в том, что считается, что они увеличивают сложность вашего кода без реальной пользы. Эта аргументация верна, если у вас плохие инструменты и классическое представление о безопасности. Возьмем следующий пример:

template<class T>  fun(T t){
   do_some_thing(t);
}

В классическом способе определения системы безопасности вы должны предоставить полное описание каждой функции и структуры вашего кода. Это означает, что вам не разрешено иметь какой-либо код без спецификации. Это означает, что вы должны дать полное описание функциональности шаблона в его общей форме. По понятным причинам это невозможно. Это, кстати, та же причина, по которой функциональные макросы также запрещены. Если вы измените идею таким образом, что будете описывать все фактические экземпляры этого шаблона, вы преодолеете это ограничение, но вам потребуются соответствующие инструменты, чтобы доказать, что вы действительно описали их все.

Вторая проблема вот в чем:

fun(b);

Эта линия не является автономной линией. Вам нужно найти тип b, чтобы узнать, какая функция на самом деле вызывается. Здесь помогает правильный инструментарий, понимающий шаблоны. Но в данном случае это действительно затрудняет проверку кода вручную.

Это утверждение о том, что шаблоны являются причиной уязвимости, кажется мне совершенно сюрреалистичным. По двум основным причинам:

• шаблоны «компилируются», т. е. создаются и генерируются кодом, как и любая другая функция/член, и для них нет поведения, характерного для них. Как будто их никогда не существовало;

• ни одна конструкция ни в одном языке не является ни безопасной, ни уязвимой; если ионизирующая частица изменяет один бит памяти, будь то в коде или в данных, возможно все (от отсутствия заметной проблемы до сбоя процессора). Способ защиты системы от этого — добавление возможностей аппаратного обнаружения/исправления ошибок памяти. Не изменяя код!