Какие языки используются для программного обеспечения, критически важного для безопасности?[закрыто]
https://stackoverflow.com/questions/243387
-
04-07-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianВопрос
Я изучаю разработку критически важного для безопасности программного обеспечения и, в частности, то, как выбор языка программирования влияет на такую разработку.
Пожалуйста, подробно объясните, какие языки обычно используются и почему.
Решение
Ada и ИСКРА (который является диалектом Ada с некоторыми зацепками для статической проверки) используются в аэрокосмических кругах для создания высоконадежного программного обеспечения, такого как системы авионики.В этом есть что-то от экосистема инструментов проверки кода для этих языков, хотя эта технология также существует для а также другие популярные языки.
Эрланг был разработанный с нуля для высокая надежность записи телекоммуникационный код.Он предназначен для облегчения разделения задач по восстановлению после ошибок (т. е.подсистема, генерирующая ошибку, отличается от подсистемы, которая обрабатывает ошибку).Это также может быть подвергнуто формальным доказательствам, хотя на самом деле эта возможность не вышла далеко за пределы исследовательских кругов.
Функциональные языки такие , как Хаскелл могут быть подвергнуты формальным проверкам с помощью автоматизированных систем благодаря декларативный характер о языке.Это позволяет содержать код с побочными эффектами в монадических функциях.Для формального доказательства корректности можно предположить, что остальная часть кода не делает ничего, кроме того, что указано.
Однако эти языки являются сборщиками мусора, и сборка мусора прозрачна для кода, поэтому о ней нельзя рассуждать таким образом.Языки, собирающие мусор, обычно недостаточно предсказуемы для жестких приложений реального времени, хотя в настоящее время проводится множество исследований в области инкрементных сборщиков мусора с ограниченным временем.
Эйфелева башня и его потомки имеют встроенную поддержку техники, называемой Проектирование По Контракту который обеспечивает надежный механизм выполнения для включения предварительных и последующих проверок на инварианты. Хотя Eiffel никогда по-настоящему не прижился, разработка высоконадежного программного обеспечения, как правило, заключается в написании проверок и обработчиков режимов сбоев заранее, прежде чем фактически писать функциональность.
Хотя C и C++ не будучи специально разработанными для такого типа приложений, они широко используются для встраиваемого и критически важного для безопасности программного обеспечения по нескольким причинам.Основными свойствами note являются контроль над управлением памятью (что позволяет, например, избежать необходимости собирать мусор), простые, хорошо отлаженные библиотеки ядра во время выполнения и развитая инструментальная поддержка.Многие цепочки инструментов встроенной разработки, используемые сегодня, были впервые разработаны в 1980-х и 1990-х годах, когда это была современная технология, и происходят из культуры Unix, которая была распространена в то время, поэтому эти инструменты остаются популярными для такого рода работы.
Хотя код ручного управления памятью должен быть тщательно проверен во избежание ошибок, он обеспечивает определенную степень контроля над временем отклика приложения, недоступную для языков, зависящих от вывоз мусора. Тот самый основные библиотеки времени выполнения языки C и C ++ относительно просты, проработаны и хорошо понятны, поэтому они являются одними из самых стабильных доступных платформ.Большинство, если не все инструменты статического анализа, используемые для Ada, также поддерживают C и C ++, и существует множество другие подобные инструменты, доступные для C.Есть такие также несколько широко использованный C/C++ основанный инструмент цепи;большинство цепочек инструментов, используемых для Ada, также выпускаются в версиях, поддерживающих C и / или C ++.
Формальные методы такие , как Аксиоматическая Семантика (PDF), Обозначение Z или Передача информации о Последовательных процессах позволяют математически выверять логику программы и часто используются при разработке критически важного для безопасности программного обеспечения, где приложение достаточно простое для их применения (обычно это встроенные системы управления).Например, один из моих бывших преподавателей провел формальное доказательство корректности системы сигнализации для немецкой железнодорожной сети.
Основным недостатком формальных методов является их тенденция к экспоненциальному усложнению по отношению к доказываемой базовой системе.Это означает, что существует значительный риск ошибок в доказательстве, поэтому они практически ограничены довольно простыми приложениями.Формальные методы довольно широко используются для проверки корректности аппаратного обеспечения, поскольку исправление аппаратных ошибок обходится очень дорого, особенно в продуктах массового спроса.С тех пор, как Ошибка Pentium FDIV, формальные методы привлекли довольно много внимания и были используется для проверки корректности FPU на всех процессорах Intel, начиная с Pentium Pro.
Многие другие языки использовались для разработки высоконадежного программного обеспечения. На эту тему было проведено много исследований. Можно разумно утверждать , что методология важнее платформы хотя существуют такие принципы, как простота, выбор и контроль зависимостей, которые могут запрещать использование определенных платформ.
Как отмечали другие, некоторые операционные платформы имеют функции, повышающие надежность и предсказуемость поведения, такие как таймеры сторожевого таймера и гарантированное время отклика на прерывание.Простота также является сильным фактором надежности, и многие системы RT намеренно делаются очень простыми и компактными. QNX (единственный такой O / S, с которым я знаком, поскольку когда-то работал с система дозирования бетона на его основе) очень мал и поместится на одной дискете.По тем же причинам люди, которые делают OpenBSD - который известен своей надежной безопасностью и тщательным аудитом кода - также прилагают все усилия, чтобы упростить систему.
Редактировать: Это сообщение содержит несколько ссылок на хорошие статьи о критически важном программном обеспечении, в частности Здесь и Здесь.Спасибо С.Лотту и Адаму Дэвису за источник.История о том, как THERAC-25 это своего рода классическая работа в этой области.
Другие советы
Для C ++ хорошо подходит стандарт кодирования Joint Strike Fighter (F-35) на C ++:
Я верю Ada все еще используется в некоторых правительственных проектах, имеющих решающее значение для безопасности и / или миссии.Я никогда не пользовался этим языком, но он есть в моем списке "для изучения", наряду с Eiffel.Eiffel предлагает дизайн по контракту, который должен повысить надежность и безопасность.
Во-первых, критически важное для безопасности программное обеспечение придерживается тех же принципов, которые вы могли бы видеть в классических областях машиностроения и электротехники.Резервирование, отказоустойчивость и безотказность.
В качестве отступления, и как упоминалось на предыдущем постере (и по какой-то причине он был отклонен), единственным наиболее важным фактором в достижении этой цели является то, чтобы ваша команда имела четкое представление обо всем, что происходит.Само собой разумеется, что хороший дизайн программного обеспечения с вашей стороны является ключевым фактором.Но это также подразумевает наличие доступного, зрелого, хорошо поддерживаемого языка, для которого доступно много общих знаний и опытных разработчиков.
Многие постеры уже прокомментировали, что операционная система является ключевым элементом в этом отношении, что очень верно, поскольку она должна быть детерминированной (см. QNX или VxWorks).Это исключает большинство интерпретируемых языков, которые делают что-то за вас за кулисами.
ADA - это возможность, но там меньше инструментов и поддержки, и, что более важно, звездные сотрудники не так легко доступны.
C ++ - это возможность, но только в том случае, если вы строго применяете подмножество.В этом отношении это инструмент дьявола, обещающий облегчить нашу жизнь, но часто делающий слишком много,
C - это идеально.Он очень зрелый, быстрый, обладает разнообразным набором инструментов и поддержки, многими опытными разработчиками, кроссплатформенный и чрезвычайно гибкий, может работать близко к аппаратному обеспечению.
Я развивался во всем, от smalltalk до ruby, и ценю и наслаждаюсь всем, что могут предложить более высокие языки.Но когда я занимаюсь разработкой критически важных систем, я стискиваю зубы и придерживаюсь C.По моему опыту (защита и многие медицинские приборы класса II и III), чем меньше, тем лучше.
Я бы взял haskell, если бы это было безопаснее всего остального.Я предлагаю haskell, потому что в нем очень жесткая статическая проверка типов и он продвигает программирование, при котором вы создаете детали таким образом, что их очень легко протестировать.
Но тогда я бы не слишком заботился о языке.Вы можете добиться гораздо большей безопасности без таких значительных компромиссов, если будете поддерживать свой проект в целом в надлежащем состоянии и работать без ограничений в сроки.В целом, как и при наличии всех базовых принципов управления проектами.Возможно, я бы сосредоточился на обширном тестировании, чтобы убедиться, что все работает так, как должно, тестах, которые охватывают все угловые случаи и многое другое.
Язык и операционная система важны, но так же важен и дизайн.Постарайтесь, чтобы все было предельно просто.
Я бы начал с того, что у меня был минимум информации о состоянии (данные во время выполнения), чтобы свести к минимуму вероятность того, что она станет непоследовательной.Затем, если вы хотите иметь избыточность в целях обеспечения отказоустойчивости, убедитесь, что у вас есть надежные способы восстановления данных, которые становятся несогласованными.Избыточность без способа устранения несоответствия просто напрашивается на неприятности.
Всегда имейте запасной вариант на случай, если запрошенные действия не будут выполнены в разумные сроки.Как говорят в управлении воздушного движения, неподтвержденный допуск - это отсутствие допуска.
Не бойтесь методов опроса.Они просты и надежны, даже если могут потратить впустую несколько циклов.Избегайте обработки, которая зависит исключительно от событий или уведомлений, поскольку они могут быть легко удалены, продублированы или неправильно упорядочены.Как дополнение к опросу, они хороши.
Мой друг из проекта APOLLO однажды заметил, что он знал, что они настроены серьезно, когда решили полагаться на опросы, а не на события, даже несмотря на то, что компьютер был ужасно медленным.
P.S.Я только что ознакомился со стандартами C ++ для воздушных судов.С ними все в порядке, но они, похоже, предполагают, что будет много классов, данных, указателей и динамического выделения памяти.Это именно то, чего не должно быть больше, чем абсолютно необходимо.Там должен быть царь структуры данных с большой косой.
Операционная система важнее языка.Используйте ядро реального времени, такое как VxWorks или QNX.Мы рассмотрели оба варианта управления промышленными роботами и решили выбрать VxWorks.Мы используем C для фактического управления роботом.
Для действительно важного программного обеспечения, такого как системы автоматической посадки самолетов, требуется, чтобы несколько процессоров работали независимо для перекрестной проверки результатов.
Среды реального времени обычно предъявляют "критические к безопасности" требования.Для такого рода вещей вы могли бы посмотреть на VxWorks, популярная операционная система реального времени.В настоящее время он используется во многих различных областях, таких как самолеты Boeing, внутренние устройства BMW iDrive, RAID-контроллеры и различные космические аппараты.(Зацени это.)
Разработка для платформы VxWorks может осуществляться с помощью нескольких инструментов, среди которых Затмение, Верстак, ОЦЕНКА, и другие.Поддерживаются C, C ++, Ada и Fortran (да, Fortran), а также некоторые другие.
Поскольку вы не предоставляете платформу, я бы сказал C / C ++.В любом случае, на большинстве платформ реального времени ваши возможности относительно ограничены.
Недостатки C, склонные позволять вам стрелять себе в ногу, компенсируются количеством инструментов для проверки кода, а также стабильностью и прямым сопоставлением кода с аппаратными возможностями платформы.Кроме того, в случае чего-либо критического вы не сможете полагаться на стороннее программное обеспечение, которое не прошло тщательного анализа - к ним относится большинство библиотек, даже многие из тех, что предоставляются поставщиками оборудования.
Поскольку вы будете нести ответственность за все, вам нужен стабильный компилятор, предсказуемое поведение и близкое соответствие аппаратному обеспечению.
Вот несколько обновлений для некоторых инструментов, которые я еще не видел обсуждаемыми, с которыми я играл в последнее время, и которые довольно хороши.
Инфраструктура компилятора LLVM, краткое рекламное объявление на их главной странице (включает интерфейсы для C и C ++.Интерфейсы для Java, Scheme и других языков находятся в разработке);
Инфраструктура компилятора - LLVM также представляет собой набор исходного кода, который реализует язык и стратегию компиляции.Основными компонентами инфраструктуры LLVM являются интерфейс C & C ++ на основе GCC, платформа оптимизации времени соединения с растущим набором глобальных и межпроцедурных анализов и преобразования, статические серверные части для X86, X86-64, PowerPC 32/64, ARM, Архитектуры Thumb, IA-64, Alpha, SPARC, MIPS и CellSPU, серверная часть, которая генерирует переносимый код на C, и компилятор "точно в срок" для X86, X86-64, Процессоры PowerPC 32/64 и эмиттер для MSIL.
VCC;
VCC - это инструмент, который проверяет правильность аннотированных параллельных программ на C или находит в них проблемы.VCC расширяет C функциями проектирования по контракту, такими как предварительные и постусловия, а также инварианты типа .Аннотированные программы преобразуются в логические формулы с помощью инструмента Boogie, который передает их автоматизированному SMT-решателю Z3 для проверки их достоверности.
VCC использует недавно выпущенный Общая инфраструктура компилятора.
Оба этих инструмента, LLVM или VCC, предназначены для поддержки нескольких языков и архитектур, я действительно думаю, что они способствуют росту кодирования по контракту и других формальных методов проверки.
WPF (не MS framework :), это хорошее место для начала, если вы пытаетесь оценить некоторые недавние исследования и инструменты в области проверки программы.
WG23 однако является основным ресурсом для довольно актуальных и специфичных сведения о языке разработки критически важных систем.Они охватывают все, начиная с Ada, C, C ++, Java, C #, скриптинга и т.д...и иметь, по крайней мере, приличный набор ссылок и рекомендаций по обновлению информации о специфичных для языка недостатках и уязвимостях.
Есть много хороших ссылок на http://www.dwheeler.com ("программное обеспечение с высокой степенью надежности").
Сведения об автомобилестроении см. в стандарте MISRA C.C но вы не можете использовать более двух уровней указателей и некоторые другие подобные вещи.
adahome.com имеет хорошую информацию об Аде.Мне понравился этот учебник по C ++ для Ada: http://adahome.com/Ammo/cpp2ada.html
Для работы в режиме реального времени Том Хокинс сделал несколько интересных вещей на Haskell.Видишь:ImProve (язык включает решатель SMT для проверки условий проверки) и Atom (EDSL для жесткого параллельного программирования в реальном времени без использования реальных потоков или задач).
Язык, который навязывает тщательные шаблоны, может помочь, но вы можете навязать тщательные шаблоны, используя любой язык, даже ассемблер.Каждое предположение о каждом значении нуждается в коде, который проверяет это предположение.Например, всегда проверяйте делитель на ноль перед делением.
Чем больше вы можете доверять многоразовым компонентам, тем проще задача, но многоразовые компоненты редко сертифицируются для критического использования и не помогут вам пройти нормативные процедуры обеспечения безопасности.Вы должны использовать крошечное ядро операционной системы, а затем создавать крошечные модули, которые проходят модульное тестирование со случайным вводом.Такой язык, как Eiffel, мог бы помочь, но здесь нет серебряной пули.
Любой программный продукт может пройти сертификацию DO-178b с использованием любого инструмента, но вопрос в том, насколько это будет сложно.Если компилятор не сертифицирован, вам, возможно, потребуется продемонстрировать, что ваш код отслеживается на уровне ассемблера.Поэтому полезно, чтобы ваш компилятор был сертифицирован.Мы использовали C в наших проектах, но должны были проверять на уровне сборки и использовать стандарт кода, который включал отключение оптимизатора, ограниченное использование стека, ограниченное использование прерываний, прозрачные сертифицируемые библиотеки и т.д.ADA - это не pixie dust, но благодаря ей план PSAC выглядит более достижимым.
По мере увеличения размеров приложений ассемблерный код становится менее приемлемым выбором.Процессор ARM просто предлагает C ++, но если вы спросите такие компании, как Kiel it, сертифицирован ли их инструмент, они ответят "да?" И не забывайте, что инструменты verificaton также должны быть сертифицированы.Попробуйте проверить тестовую программу LabVIEW.
Новый критичный стандарт безопасности для Java в настоящее время находится в разработке - JSR 302:Технология Java, критически важная для безопасности.
Тот самый Java, критически важная для безопасности (SCJ) основан на подмножестве RTSJ.Цель состоит в том, чтобы создать структуру, подходящую для разработки и анализа программ, критичных к безопасности, для сертификации по критериям безопасности (DO-178B, уровень A и другие стандарты, критичные к безопасности).
SCJ, например, удаляет кучу, которая все еще присутствует в RTSJ, он также определяет 3 уровня соответствия, которым могут соответствовать как приложение, так и реализация виртуальной машины, уровни соответствия определены для облегчения сертификации различных сложных приложений.
Ресурсы:
Я не знаю, какой язык я бы использовал, но я точно знаю, какой язык я бы не стал использовать:
ПРИМЕЧАНИЕ О ПОДДЕРЖКЕ JAVA.ПРОГРАММНЫЙ ПРОДУКТ МОЖЕТ СОДЕРЖАТЬ ПОДДЕРЖКУ ПРОГРАММ, НАПИСАННЫХ НА JAVA.ТЕХНОЛОГИЯ JAVA НЕ ЯВЛЯЕТСЯ ОТКАЗОУСТОЙЧИВОЙ И НЕ РАЗРАБОТАНА, НЕ ИЗГОТОВЛЕНА И НЕ ПРЕДНАЗНАЧЕНА ДЛЯ ИСПОЛЬЗОВАНИЯ Или ПЕРЕПРОДАЖИ В КАЧЕСТВЕ ОБОРУДОВАНИЯ ОПЕРАТИВНОГО УПРАВЛЕНИЯ ВО ВЗРЫВООПАСНЫХ СРЕДАХ, ТРЕБУЮЩИХ БЕЗОТКАЗНОЙ РАБОТЫ, ТАКИХ КАК ЭКСПЛУАТАЦИЯ ЯДЕРНЫХ УСТАНОВОК, АВИАЦИОННЫХ СИСТЕМ НАВИГАЦИИ ИЛИ СВЯЗИ, УПРАВЛЕНИЯ ВОЗДУШНЫМ ДВИЖЕНИЕМ, МАШИН НЕПОСРЕДСТВЕННОГО ЖИЗНЕОБЕСПЕЧЕНИЯ ИЛИ СИСТЕМ ВООРУЖЕНИЯ, В КОТОРЫХ ОТКАЗ ТЕХНОЛОГИИ JAVA МОЖЕТ ПРИВЕСТИ НЕПОСРЕДСТВЕННО К СМЕРТИ, ТРАВМАМ ПЕРСОНАЛА ИЛИ СЕРЬЕЗНОМУ ФИЗИЧЕСКОМУ УЩЕРБУ Или ОКРУЖАЮЩЕЙ СРЕДЕ.
HAL / S используется для космического челнока.
