Набор инструментов для статического анализа программного обеспечения MALPAS
| Разработчик(и) | Аткинс |
|---|---|
| Операционная система | Окна |
| Тип | Статический анализ программы |
| Лицензия | Собственный |
| Веб-сайт | www |
MALPAS — это набор программных инструментов, который предоставляет средства исследования и доказательства правильности программного обеспечения путем применения строгой формы статического анализа программы . Инструмент использует ориентированные графы и обычную алгебру для представления анализируемой программы. Используя автоматизированные инструменты MALPAS, аналитик может описать структуру программы, классифицировать использование данных и предоставить информационные связи между входными и выходными данными. Он также поддерживает формальное доказательство того, что код соответствует спецификации.
MALPAS использовался для подтверждения правильности критически важных для безопасности приложений в ядерной, [1] аэрокосмический [2] и защита [3] отрасли. Он также использовался для обеспечения корректности компилятора в атомной промышленности на Sizewell B. [4] Языки, которые были проанализированы, включают: Ada , C , PLM и Intel Assembler .
MALPAS хорошо подходит для независимого статического анализа, требуемого Исполнительным руководством Великобритании по охране труда и технике безопасности для компьютерных систем защиты ядерных реакторов, благодаря своей строгости и гибкости в работе со многими языками программирования. [5]
Технический обзор [ править ]
Набор инструментов MALPAS включает пять конкретных инструментов анализа, которые учитывают различные свойства программы. Входные данные для анализаторов должны быть написаны на промежуточном языке MALPAS (IL); он может быть написан от руки или создан с помощью инструмента автоматического перевода из исходного исходного кода. Существуют автоматические трансляторы для распространенных языков программирования высокого уровня, таких как Ada , C и Pascal , а также языков ассемблера, таких как Intel 80*86 , PowerPC и 68000 . Текст IL вводится в MALPAS через «IL Reader», который создает ориентированный граф и соответствующую семантику для анализируемой программы. Граф сокращается с использованием ряда методов сокращения графа.
Набор инструментов MALPAS состоит из 5 анализаторов: [6]
- Анализатор потока управления. При этом исследуется структура программы, определяются ключевые особенности: точки входа/выхода, циклы, ветки и недостижимый код. Он предоставляет сводный отчет, обращающий внимание на нежелательные конструкции и указывающий на сложность структуры программы.
- Анализатор использования данных. Это разделяет переменные и параметры, используемые программой, на отдельные классы в зависимости от их использования. (т. е. данные, которые считываются перед записью, данные, которые записываются без чтения, или данные, которые записываются дважды без промежуточного чтения). В отчете могут быть выявлены такие ошибки, как неинициализированные данные и выходные данные функций, записанные не на всех путях.
- Анализатор информационных потоков . Это определяет зависимости данных и ветвей для каждой выходной переменной или параметра. Нежелательные или неожиданные зависимости могут быть обнаружены на всех этапах кода. Также предоставляется информация о неиспользуемых переменных и избыточных операторах.
- Семантический анализатор (также известный как символическое выполнение ). Это раскрывает точную функциональную связь между всеми входными и выходными данными на всех семантически возможных путях прохождения кода.
- Анализатор соответствия. При этом математическое поведение кода сравнивается с его формальной спецификацией IL, подробно описывая, где одно отличается от другого. Спецификация IL записана в виде предусловий и постусловий , а также необязательных утверждений кода. Анализ соответствия можно использовать для достижения очень высокого уровня уверенности в функциональной корректности кода по отношению к его спецификации.
История [ править ]
Первоначальное исследование и первые поколения набора инструментов были созданы британским Королевским институтом сигналов и радиолокации (RSRE) в Малверне, Англия (отсюда и название — MALvern Programming Analysis Suite). Он широко использовался в гражданской ядерной и оружейной сфере в 1980-х годах, когда его поддержали компания «Рекс, Томпсон и партнеры», которые создали группу пользователей MALPAS, первым председателем которой был Дэвид Х. Смит (ныне из Frazer-Nash) и затем компания Advantage Технический консалтинг (купленная Аткинсом в 2008 году).
Первая крупномасштабная задача статического анализа была связана с системой защиты реактора первого контура Сайзуэлл Б. электростанции Это была первая атомная электростанция в Великобритании, на которой в качестве первой линии защиты от катастрофического отказа использовалась компьютерная система защиты. Кроме того, компания CEZ в Чешской Республике использовала MALPAS для повышения уверенности в системе защиты реактора на АЭС Темелин . Великобритании В 1995 году Королевские ВВС заказали независимый анализ программного обеспечения авионики Lockheed Martin C130J , которое было оценено как критически важное для безопасности. MALPAS использовался для анализа этого программного обеспечения, кроме программного обеспечения Mission Computer, которое было написано на Spark Ada и проверено с помощью Spark Toolset. [7] MALPAS в настоящее время используется для независимой оценки программного обеспечения системы защиты реактора, которая будет контролировать два ядерных реактора в Хинкли-Пойнт-С. [8]
Ссылки [ править ]
- ^ Программируемая защита на АЭС Великобритании: 10 лет спустя, Д. Пейви, British Energy. http://entrac.iaea.org/I-and-C/TM_VTT_2005_11/IAEA_papers/051124_Thursday/IAEA_paper_Pavey.pdf
- ^ «Статический анализ кода критически важного для безопасности программного обеспечения C-130J Hercules, Eur Ing KJ Harrison, BSc CPhys MinstP CEng MRAeS MBCS; Aerosystems International, Великобритания» (PDF) . Архивировано из оригинала (PDF) 27 сентября 2011 г. Проверено 18 марта 2011 г.
- ^ Анализ программного обеспечения боеприпасов с использованием инструментов MALPAS, Hayman, K, Defense Sci. и Технол. Орган., Солсбери, ЮАР. http://www.dsto.defence.gov.au/publications/scientific_record.php?record=9074
- ^ Формальная демонстрация эквивалентности исходного кода и содержимого PROM, Труды конференции IMA по математике надежных систем, Oxford University Press, 1995, стр. 225248D Дж. Пейви и Л. А. Уинсборроу.
- ^ «Компьютерные системы безопасности – техническое руководство по оценке программных аспектов цифровых компьютерных систем защиты» . Архивировано из оригинала 4 июля 2011 г.
- ^ Промышленный взгляд на статический анализ. Журнал Software Engineering, март 1995 г.: 69–75. Вихманн, Б.А., А.А. Каннинг, Д.Л. Клаттербак, Л.А. Уинсбарроу, Н.Дж. Уорд и Д.В.Р. Марш. http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf
- ^ Статический анализ кода критически важного для безопасности программного обеспечения C-130J Hercules «Архивная копия» (PDF) . Архивировано из оригинала (PDF) 27 сентября 2011 г. Проверено 18 марта 2011 г.
{{cite web}}: CS1 maint: архивная копия в заголовке ( ссылка ) - ^ https://www.newcivilengineer.com/latest/atkins-wins-hinkley-point-c-safety-contract-27-04-2020/