Какие языки используются для безопасного программного обеспечения?
Я исследую разработку программного обеспечения, критически важного для безопасности, и, в частности, что влияет на выбор языка программирования.
Пожалуйста, объясните подробно, какие языки обычно используются и почему.
16 ответов
Ada и SPARK (это диалект Ada с некоторыми крючками для статической проверки) используются в аэрокосмических кругах для создания высоконадежного программного обеспечения, такого как системы авионики. Существует нечто вроде экосистемы инструментов проверки кода для этих языков, хотя эта технология также существует и для других основных языков.
Erlang был разработан с нуля для написания высоконадежного телекоммуникационного кода. Он предназначен для облегчения разделения проблем для устранения ошибок (т.е. подсистема, генерирующая ошибку, отличается от подсистемы, которая обрабатывает ошибку). Он также может быть подвергнут формальным доказательствам, хотя эта возможность на самом деле не далеко ушла от исследовательских кругов.
Функциональные языки, такие как Haskell, могут подвергаться формальным проверкам автоматизированными системами из-за декларативной природы языка. Это позволяет содержать код с побочными эффектами в монадических функциях. Для формального доказательства корректности можно предположить, что остальная часть кода не делает ничего, кроме указанного.
Однако эти языки являются сборщиком мусора, а сборка мусора прозрачна для кода, поэтому об этом нельзя рассуждать. Языки сборки мусора обычно недостаточно предсказуемы для жестких приложений реального времени, хотя в настоящее время ведутся исследования в области инкрементных сборщиков мусора с ограниченным временем.
Eiffel и его потомки имеют встроенную поддержку метода, называемого Design By Contract, который обеспечивает надежный механизм времени выполнения для включения предварительных и последующих проверок для инвариантов. В то время как Eiffel никогда не завоевывал популярность, разработка высоконадежного программного обеспечения, как правило, состоит из написания проверок и обработчиков для режимов отказа заранее, прежде чем они на самом деле пишут функциональность.
Хотя C и C++ не были специально разработаны для этого типа приложений, они широко используются для встроенного и критически важного для безопасности программного обеспечения по нескольким причинам. Основные свойства заметки: контроль над управлением памятью (что позволяет избежать необходимости, например, сбора мусора), простые, хорошо отлаженные библиотеки времени выполнения ядра и поддержка зрелых инструментов. Многие из используемых в настоящее время цепочек инструментов для встраиваемых разработок были впервые разработаны в 1980-х и 1990-х годах, когда это была текущая технология, и исходили из культуры Unix, которая была распространена в то время, поэтому эти инструменты остаются популярными для такого рода работ.
Хотя код ручного управления памятью необходимо тщательно проверять во избежание ошибок, он позволяет в определенной степени контролировать время отклика приложения, которое недоступно для языков, зависящих от сборки мусора. Базовые библиотеки времени исполнения языков C и C++ относительно просты, зрелы и хорошо понятны, поэтому они являются одними из самых стабильных платформ. Большинство, если не все инструменты статического анализа, используемые для Ada, также поддерживают C и C++, и есть много других таких инструментов, доступных для C. Существует также несколько широко используемых цепочек инструментов на основе C/C++; большинство цепочек инструментов, используемых для Ada, также выпускаются в версиях, которые поддерживают C и / или C++.
Формальные методы, такие как аксиоматическая семантика (PDF), Z-нотация или связывание последовательных процессов, позволяют математически проверять программную логику и часто используются при разработке критически важного для безопасности программного обеспечения, где приложение достаточно просто для их применения (обычно это встроенные системы управления), Например, один из моих бывших лекторов сделал формальное доказательство правильности системы сигнализации для немецкой железнодорожной сети.
Основным недостатком формальных методов является их тенденция к экспоненциальному росту сложности в отношении доказываемой базовой системы. Это означает, что существует значительный риск ошибок в доказательстве, поэтому они практически ограничены достаточно простыми приложениями. Формальные методы достаточно широко используются для проверки правильности аппаратного обеспечения, поскольку ошибки в оборудовании очень дороги, особенно в продуктах массового рынка. Со времени ошибки Pentium FDIV формальные методы привлекли большое внимание и использовались для проверки правильности FPU на всех процессорах Intel начиная с Pentium Pro.
Многие другие языки были использованы для разработки высоконадежного программного обеспечения. Много исследований было сделано на эту тему. Можно разумно утверждать, что методология важнее, чем платформа, хотя существуют такие принципы, как простота, выбор и контроль зависимостей, которые могут препятствовать использованию определенных платформ.
Как отмечали различные другие, некоторые платформы O/S имеют функции для обеспечения надежности и предсказуемого поведения, такие как сторожевые таймеры и гарантированное время отклика на прерывание. Простота также является сильным фактором надежности, и многие системы RT преднамеренно сохраняются очень простыми и компактными. QNX (единственная такая операционная система, с которой я знаком, когда-то работавшая с конкретной системой дозирования на ее основе), очень мала и может поместиться на одной дискете. По тем же причинам люди, которые делают OpenBSD - которая известна своей надежной безопасностью и тщательным аудитом кода - также стараются изо всех сил сохранять систему простой.
РЕДАКТИРОВАТЬ: Эта публикация имеет несколько ссылок на хорошие статьи о безопасности программного обеспечения, в частности здесь и здесь. Реквизиты С. Лотту и Адаму Дэвису за источник. История с THERAC-25 - это классическая работа в этой области.
Для C++, Стандарт кодирования C++ в "Joint Strike Fighter" (F-35) является хорошим чтением:
Я полагаю, что Ада все еще используется в некоторых правительственных проектах, которые критически важны для безопасности и / или миссии. Я никогда не использовал этот язык, но он в моем списке "учиться" вместе с Эйфелевой. Eiffel предлагает Design By Contract, что должно повысить надежность и безопасность.
Во-первых, программное обеспечение, критически важное для безопасности, придерживается тех же принципов, что и классические области механики и электротехники. Избыточность, отказоустойчивость и отказоустойчивость.
Помимо этого, и как упоминалось в предыдущем постере (и по какой-то причине было отвергнуто), единственным наиболее важным фактором в достижении этого является то, что ваша команда должна иметь четкое понимание всего, что происходит. Само собой разумеется, что хороший дизайн программного обеспечения с вашей стороны является ключевым. Но это также подразумевает доступный, зрелый, хорошо поддерживаемый язык, для которого доступно много общих знаний и опытных разработчиков.
Многие авторы уже прокомментировали, что ОС является ключевым элементом в этом отношении, и это очень верно, поскольку она должна быть детерминированной (см. QNX или VxWorks). Это исключает большинство интерпретируемых языков, которые делают что-то за кадром для вас.
ADA возможна, но там меньше инструментов и поддержки, и что более важно, звездные люди не так легко доступны.
C++ возможен, но только если вы строго соблюдаете подмножество. В этом отношении это инструмент дьявола, обещающий облегчить нашу жизнь, но часто делающий слишком много,
С идеальным. Он очень зрелый, быстрый, имеет разнообразный набор инструментов и поддержки, многие опытные разработчики, кроссплатформенные и чрезвычайно гибкие, могут работать близко к аппаратному обеспечению.
Я развивался во всем, от разговоров до рубина, и ценю и наслаждаюсь всем, что могут предложить более высокие языки. Но когда я занимаюсь разработкой критических систем, я кусаю пулю и держусь C. В моем опыте (защита и многие медицинские приборы класса II и III) меньше - больше.
Я бы подобрал Хаскель, если это безопасность над всем остальным. Я предлагаю haskell, потому что он имеет очень жесткую статическую проверку типов и способствует программированию, когда вы создаете детали таким образом, что их очень легко тестировать.
Но тогда мне было бы наплевать на язык. Вы можете получить гораздо большую безопасность, не ставя на компромиссы, если ваш проект в целом находится в рабочем состоянии и работает без сроков. В целом, как при наличии всех основных управления проектами на месте. Возможно, я бы сконцентрировался на всестороннем тестировании, чтобы убедиться, что все работает так, как должно, тестах, которые охватывают все ключевые случаи + еще
Язык и ОС важны, но так же важен и дизайн. Постарайтесь, чтобы все было просто, просто офигительно.
Я бы начал с минимального количества информации о состоянии (данных времени выполнения), чтобы минимизировать вероятность того, что она станет непоследовательной. Затем, если вы хотите иметь избыточность с целью обеспечения отказоустойчивости, убедитесь, что у вас есть надежные способы восстановления после несогласованности данных. Избыточность без способа восстановления после несоответствия просто напрашивается на неприятности.
Всегда используйте запасной вариант, когда запрошенные действия не завершаются в разумные сроки. Как говорится в авиадиспетчерской службе, неподтвержденное разрешение не является разрешением.
Не бойтесь методов опроса. Они просты и надежны, даже если могут потратить несколько циклов. Избегайте обработки, которая основана исключительно на событиях или уведомлениях, потому что они могут быть легко отброшены, дублированы или искажены. Как дополнение к опросу, они в порядке.
Мой друг по проекту APOLLO однажды заметил, что он знал, что они становятся серьезными, когда решили полагаться на опрос, а не на события, даже если компьютер работал ужасно медленно.
PS Я только что прочитал стандарты C++ Air Vehicle. Они в порядке, но, похоже, предполагают, что будет много классов, данных, указателей и динамического выделения памяти. Это именно то, чего не должно быть больше, чем абсолютно необходимо. Должна быть структура данных царя с большой косой.
ОС важнее языка. Используйте ядро реального времени, такое как VxWorks или QNX. Мы посмотрели на обоих для управления промышленными роботами и решили пойти с VxWorks. Мы используем C для фактического контроля робота.
Для действительно критически важного программного обеспечения, такого как системы автоматического выбора самолетов, необходимо, чтобы несколько процессоров работали независимо друг от друга для перекрестной проверки результатов.
Среды реального времени обычно предъявляют "критические к безопасности" требования. Для такого рода вещей вы можете взглянуть на VxWorks, популярную операционную систему реального времени. В настоящее время он используется во многих различных областях, таких как самолеты Boeing, внутренние устройства BMW iDrive, контроллеры RAID и различные космические корабли. ( Проверьте это.)
Разработка платформы VxWorks может быть выполнена с помощью нескольких инструментов, среди которых Eclipse, Workbench, SCORE и другие. Поддерживаются C, C++, Ada и Fortran (да, Fortran), а также некоторые другие.
Вот несколько обновлений для некоторых инструментов, которые я еще не обсуждал, с которыми я играл в последнее время, и которые довольно хороши.
Инфраструктура компилятора 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, и компилятор Just-In-Time для X86, X86-64, PowerPC 32/64 процессоры и эмиттер для MSIL.
VCC;
VCC - это инструмент, который подтверждает правильность аннотированных параллельных программ на Си или находит в них проблемы. VCC расширяет C дизайном за счет функций контракта, таких как предварительные и постусловия, а также инварианты типов. Аннотированные программы переводятся в логические формулы с помощью инструмента Boogie, который передает их в автоматизированный SMT-решатель Z3 для проверки их правильности.
VCC использует недавно выпущенную Common Compiler Infrastructure.
Оба эти инструмента, LLVM или VCC, предназначены для поддержки нескольких языков и архитектур, и я считаю, что их использование в коде связано с контрактом и другими формальными методами проверки.
WPF (не MS Framework:), это хорошее место для начала, если вы пытаетесь оценить некоторые из последних исследований и инструментов в области проверки программ.
Однако WG23 является основным ресурсом для довольно актуальных и специфических критических деталей языка разработки систем. Они охватывают все, от Ada, C, C++, Java, C#, сценариев и т. Д. И, по крайней мере, имеют приличный набор справочных и руководящих указаний по обновлению информации о недостатках и уязвимостях, характерных для конкретного языка.
Поскольку вы не предоставляете платформу, я бы сказал C/C++. На большинстве платформ реального времени вы все равно относительно ограничены в своих возможностях.
Недостатки стремления С позволить вам выстрелить себе в ногу компенсируется количеством инструментов для проверки кода, а также стабильностью и прямым сопоставлением кода с аппаратными возможностями платформы. Кроме того, в случае чего-либо критического, вы не сможете полагаться на стороннее программное обеспечение, которое не подвергалось всестороннему анализу - в том числе большинству библиотек - даже многим из тех, которые предоставляются поставщиками оборудования.
Поскольку все будет вашей ответственностью, вам нужен стабильный компилятор, предсказуемое поведение и точное сопоставление с оборудованием.
В настоящее время разрабатывается новый критический для безопасности стандарт для Java - JSR 302: технология безопасности, критическая для Java.
Безопасность-критическая Java (SCJ) основана на подмножестве RTSJ. Цель состоит в том, чтобы создать структуру, подходящую для разработки и анализа критических для безопасности программ сертификации критических для безопасности (DO-178B, уровень A и другие критические для безопасности стандарты).
SCJ, например, удаляет кучу, которая все еще присутствует в RTSJ, он также определяет 3 уровня соответствия, которым может соответствовать реализация приложения и виртуальной машины, уровни соответствия определяются для облегчения сертификации различных сложных приложений.
Ресурсы:
Язык, который навязывает осторожные шаблоны, может помочь, но вы можете навязывать осторожные шаблоны, используя любой язык, даже ассемблер. Каждое предположение о каждом значении нуждается в коде, который проверяет это предположение. Например, всегда проверяйте делитель на ноль перед делением.
Чем больше вы можете доверять повторно используемым компонентам, тем легче будет выполнить задачу, но повторно используемые компоненты редко сертифицируются для критического использования и не помогут вам пройти процессы нормативной безопасности. Вы должны использовать крошечное ядро ОС и затем создавать крошечные модули, которые тестируются модульно со случайным вводом. Такой язык, как Эйфель, может помочь, но серебряной пули нет.
На http://www.dwheeler.com/ есть много хороших ссылок ("высоконадежное программное обеспечение").
Для автомобильных деталей, см. Стандарт MISRA C. С, но вы не можете использовать более двух уровней указателей и тому подобное.
У adahome.com есть хорошая информация об Аде. Мне понравился этот учебник по C++ для Ada: http://adahome.com/Ammo/cpp2ada.html
Для тяжелого реального времени Том Хокинс сделал несколько интересных вещей на Haskell. См.: ImProve (язык включает SMT-решатель для проверки условий проверки) и Atom (EDSL для жесткого параллельного программирования в реальном времени без использования реальных потоков или задач).
Любой программный продукт может пройти сертификацию DO-178b с использованием любого инструмента, но вопрос в том, насколько сложным он будет. Если компилятор не сертифицирован, вам может потребоваться продемонстрировать, что ваш код отслеживается на уровне сборки. Поэтому полезно, чтобы ваш компилятор был сертифицирован. Мы использовали C в наших проектах, но должны были проверить на уровне сборки и использовать стандарт кода, который включал отключение оптимизатора, ограниченное использование стека, ограниченное использование прерываний, прозрачные сертифицируемые библиотеки и т. Д. План PSAC выглядит более достижимым.
По мере увеличения числа приложений код сборки становится менее жизнеспособным выбором. Процессор ARM просто предлагает C++, но если вы спросите такие компании, как Kiel, его инструмент сертифицирован, они вернутся с "а?" И не забывайте, что инструменты верификации также должны быть сертифицированы. Попробуйте проверить тестовую программу LabView.
Я не знаю, на каком языке я бы использовал, но я знаю, на каком языке я бы не стал:
ПРИМЕЧАНИЕ ПО ПОДДЕРЖКЕ JAVA. ПРОГРАММНЫЙ ПРОДУКТ МОЖЕТ СОДЕРЖАТЬ ПОДДЕРЖКУ ДЛЯ ПРОГРАММ, НАПИСАННЫХ В ЯВА. Технология Java не является отказоустойчивой и не предназначена, ПРОИЗВЕДЁНА, или предназначенным для использования или перепродаж КАК НА РЕЖИМ РЕАЛЬНОГО ВРЕМЕНИ В ОПАСНЫХ УСЛОВИЯХ ТРЕБУЮЩИХ БЕЗОТКАЗНОЙ РАБОТЫ, например, в ФУНКЦИОНИРОВАНИЯ ЯДЕРНЫХ УСТАНОВОК, AIRCRAFT СУДЫ ИЛИ СИСТЕМЫ СВЯЗИ, AIR УПРАВЛЕНИЕ ДВИЖЕНИЕМ, НЕПОСРЕДСТВЕННЫЕ МАШИНЫ ПОДДЕРЖКИ ЖИЗНИ ИЛИ СИСТЕМЫ ОРУЖИЯ, В КОТОРЫХ ОТКАЗ ТЕХНОЛОГИИ JAVA МОЖЕТ НАПРАВЛЯТЬСЯ ПРЯМОЙ СМЕРТИ, ЛИЧНОЙ ТРАВМОЙ, ИЛИ ОСТРОМ ФИЗИЧЕСКОГО ИЛИ ОКРУЖАЮЩЕЙ СРЕДЫ.