WikiDer > Набор инструментов для статического анализа программного обеспечения MALPAS

MALPAS Software Static Analysis Toolset
Набор инструментов для статического анализа программного обеспечения MALPAS
Разработчики)Аткинс
Операционная системаWindows
ТипСтатический анализ программы
ЛицензияПроприетарный
Интернет сайтwww.malpas-global.com - не работает с 16.09.20

МАЛЬПАС представляет собой набор программных инструментов, который предоставляет средства исследования и доказательства правильности программного обеспечения путем применения строгой формы статический анализ программы. Инструмент использует ориентированные графы и регулярная алгебра для представления анализируемой программы. Используя автоматизированные инструменты MALPAS, аналитик может описать структуру программы, классифицировать использование данных и предоставить информационные отношения между входными и выходными данными. Он также поддерживает формальное доказательство что код соответствует его спецификации.

МАЛПАС был использован для подтверждения правильности безопасность критически важна применения в ядерной,[1] аэрокосмический[2] и оборона[3] отрасли. Он также использовался для предоставления компилятор валидация в атомной отрасли на Sizewell B.[4] Были проанализированы следующие языки: Ада, C, PLM и Ассемблер Intel.

MALPAS хорошо подходит для независимого статического анализа, требуемого британской Руководитель по охране труда и технике безопасности руководство по компьютерным системам защиты ядерных реакторов благодаря строгости и гибкости при работе со многими языками программирования.[5]

Технический обзор

Набор инструментов MALPAS включает пять специальных инструментов анализа, которые обращаются к различным свойствам программы. Входные данные для анализаторов должны быть написаны на промежуточном языке MALPAS (IL); это может быть написано от руки или создано с помощью инструмента автоматического перевода из исходного исходного кода. Автоматические переводчики существуют для распространенных языков программирования высокого уровня, таких как Ада, C и Паскаль, а также языки ассемблера, такие как Intel 80 * 86, PowerPC и 68000. Текст IL вводится в MALPAS через программу «IL Reader», которая создает ориентированный граф и связанная семантика для анализируемой программы. График сокращается с использованием ряда методов сокращения графа.

Набор инструментов MALPAS состоит из 5 анализаторов:[6]

  1. Анализатор потока управления. Это исследует структуру программы, определяя ключевые особенности: точки входа / выхода, циклы, ветви и недостижимый код. Он предоставляет сводный отчет, обращающий внимание на нежелательные конструкции и указание на сложность структуры программы.
  2. Анализатор использования данных. Это разделяет переменные и параметры, используемые программой, на отдельные классы в зависимости от их использования. (т.е. данные, которые считываются перед записью, данные, которые записываются без чтения, или данные, которые записываются дважды без промежуточного чтения). Отчет может идентифицировать ошибки, такие как неинициализированные данные и выходные данные функций, записанные не на всех путях.
  3. Анализатор информационных потоков. Это определяет зависимости данных и ветвей для каждой выходной переменной или параметра. Нежелательные или неожиданные зависимости могут быть выявлены для всех путей прохождения кода. Также предоставляется информация о неиспользуемых переменных и повторяющихся утверждениях.
  4. Семантический анализатор (также известный как символическая казнь). Это выявляет точные функциональные отношения между всеми входами и выходами по всем семантически возможным путям прохождения кода.
  5. Анализатор соответствия. Это сравнивает математическое поведение кода с его формальной спецификацией IL, детализируя, где одно отличается от другого. Спецификация IL записывается как Предварительные условия и Постусловия, а также необязательные утверждения кода. Анализ соответствия может использоваться для получения очень высокого уровня уверенности в функциональной правильности кода по отношению к его спецификации.

История

Оригинальное исследование и первые поколения набора инструментов были созданы британским Королевские сигналы и радиолокационная станция (RSRE) в Малверне, Англия (отсюда и название MALvern Programming Analysis Suite). Он широко использовался в области гражданского ядерного оружия и оружия в 1980-х годах, когда его поддержали Rex, Thompson and Partners, которые создали Группу пользователей MALPAS, первым председателем которой был Дэвид Х. Смит (ныне Frazer-Nash) и затем впоследствии компания Advantage Technical Consulting (куплена Аткинс в 2008).

Первой крупномасштабной задачей статического анализа была система защиты первичного реактора Sizewell B электростанция. Это была первая атомная электростанция Великобритании, в которой использовалась компьютерная система защиты в качестве первой линии защиты от катастрофического отказа. В дополнение к этому, CEZ в Чешской Республике использовали MALPAS для повышения доверия к системе защиты реактора в Темелинская АЭС. В 1995 г. королевские воздушные силы заказал независимый анализ Локхид Мартин C130Jпрограммное обеспечение авионики России признано критически важным для безопасности. MALPAS использовался для анализа этого программного обеспечения, помимо программного обеспечения Mission Computer, которое было написано на Spark Ada и проверено с помощью набора инструментов Spark.[7]

Рекомендации

  1. ^ Программируемая защита на АЭС Великобритании: 10 лет спустя, Д. Пави, British Energy. http://entrac.iaea.org/I-and-C/TM_VTT_2005_11/IAEA_papers/051124_Thursday/IAEA_paper_Pavey.pdf
  2. ^ Статический анализ кода в программном обеспечении C-130J Hercules, критически важном для безопасности, Eur Ing K J Harrison, бакалавр наук CPhys MinstP CEng MRAeS MBCS; Aerosystems International, Великобритания. «Архивная копия» (PDF). Архивировано из оригинал (PDF) на 2011-09-27. Получено 2011-03-18.CS1 maint: заархивированная копия как заголовок (связь)
  3. ^ Анализ боеприпасы программное обеспечение с использованием инструментов MALPAS, Hayman, K, Defense Sci. & Technol. Орган., Солсбери, С.А. http://www.dsto.defence.gov.au/publications/scientific_record.php?record=9074
  4. ^ Формальная демонстрация эквивалентности исходного кода и содержимого PROM, Proceedings of the IMA Conference on Mathematics of Dependable Systems, Oxford University Press, 1995, pp225248D J Pavey and L A. Winsborrow
  5. ^ Компьютерные системы безопасности - техническое руководство по оценке программных аспектов цифровых компьютерных систем защиты, «Архивная копия». Архивировано из оригинал на 2012-10-16. Получено 2011-03-18.CS1 maint: заархивированная копия как заголовок (связь)
  6. ^ Промышленный взгляд на статический анализ. Software Engineering Journal, март 1995: 69–75 Вичманн, Б. А., А. А. Каннинг, Д. Л. Клаттербак, Л. А. Уинсбарроу, Н. Дж. Уорд и Д. В. Р. Марш. http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf
  7. ^ Статический анализ кода в программном обеспечении C-130J Hercules, критически важном для безопасности «Архивная копия» (PDF). Архивировано из оригинал (PDF) на 2011-09-27. Получено 2011-03-18.CS1 maint: заархивированная копия как заголовок (связь)