Статический анализ программы

Анализ компьютерных программ без их выполнения

В информатике статический анализ программ ( также известный как статический анализ или статическое моделирование ) — это анализ компьютерных программ, выполняемый без их выполнения, в отличие от динамического анализа программ , который выполняется над программами во время их выполнения в интегрированной среде. ^{[1] [2]}

Термин обычно применяется к анализу, выполняемому автоматизированным инструментом, а человеческий анализ обычно называется «пониманием программы», пониманием программы или обзором кода . В последнем из них также используются проверка программного обеспечения и пошаговые руководства по программному обеспечению . В большинстве случаев анализ выполняется на некоторой версии исходного кода программы , а в других случаях — на некоторой форме ее объектного кода .

Обоснование

Сложность анализа, выполняемого инструментами, варьируется от тех, которые рассматривают только поведение отдельных операторов и деклараций, ^[3] до тех, которые включают в свой анализ полный исходный код программы. Использование информации, полученной в результате анализа, варьируется от выделения возможных ошибок кодирования (например, инструмент lint ) до формальных методов , которые математически доказывают свойства данной программы (например, ее поведение соответствует ее спецификации).

Метрики программного обеспечения и обратная разработка могут быть описаны как формы статического анализа. Выведение метрик программного обеспечения и статический анализ все чаще используются вместе, особенно при создании встроенных систем, путем определения так называемых целей качества программного обеспечения . ^[4]

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

1. Медицинское программное обеспечение : Управление по контролю за продуктами и лекарствами США (FDA) определило использование статического анализа для медицинских устройств. ^[6]
2. Ядерное программное обеспечение: В Великобритании Управление по ядерному регулированию (ONR) рекомендует использовать статический анализ в системах защиты реакторов . ^[7]
3. Авиационное программное обеспечение (в сочетании с динамическим анализом ). ^[8]
4. Автомобили и машины (функциональные характеристики безопасности являются неотъемлемой частью каждого этапа разработки автомобильной продукции, ISO 26262 , раздел 8).

Исследование, проведенное в 2012 году компанией VDC Research, показало, что 28,7% опрошенных инженеров встроенного программного обеспечения используют инструменты статического анализа, а 39,7% планируют начать использовать их в течение 2 лет. ^[9] Исследование, проведенное в 2010 году, показало, что 60% опрошенных разработчиков в европейских исследовательских проектах использовали по крайней мере свои базовые встроенные статические анализаторы IDE. Однако только около 10% использовали дополнительный другой (и, возможно, более продвинутый) инструмент анализа. ^[10]

В индустрии безопасности приложений также используется название статическое тестирование безопасности приложений (SAST). SAST является важной частью жизненных циклов разработки безопасности (SDL), таких как SDL, определенный Microsoft ^[11] , и общепринятой практикой в ​​компаниях-разработчиках программного обеспечения. ^[12]

Типы инструментов

Группа управления объектами (OMG ) опубликовала исследование, касающееся типов анализа программного обеспечения, необходимых для измерения и оценки качества программного обеспечения . В этом документе «Как предоставлять устойчивые, безопасные, эффективные и легко изменяемые ИТ-системы в соответствии с рекомендациями CISQ» описываются три уровня анализа программного обеспечения. ^[13]

Уровень единицы

Анализ, который выполняется в рамках определенной программы или подпрограммы, без привязки к контексту этой программы.

Уровень технологии

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

Системный уровень

Анализ, учитывающий взаимодействие между юнит-программами, но не ограничивающийся одной конкретной технологией или языком программирования.

Можно определить еще один уровень анализа программного обеспечения.

Уровень миссии/бизнеса

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

Формальные методы

Формальные методы — это термин, применяемый к анализу программного обеспечения (и компьютерного оборудования ), результаты которого получены исключительно посредством использования строгих математических методов. Используемые математические методы включают денотационную семантику , аксиоматическую семантику , операционную семантику и абстрактную интерпретацию .

Путем прямого сведения к проблеме остановки можно доказать, что (для любого Тьюринг-полного языка) нахождение всех возможных ошибок времени выполнения в произвольной программе (или, в более общем смысле, любого вида нарушения спецификации на конечный результат программы) неразрешимо : не существует механического метода, который всегда может правдиво ответить, может ли произвольная программа демонстрировать ошибки времени выполнения или нет. Этот результат восходит к работам Чёрча , Гёделя и Тьюринга 1930-х годов (см.: Проблема остановки и теорема Райса ). Как и во многих неразрешимых вопросах, все еще можно попытаться дать полезные приближенные решения.

Некоторые из методов реализации формального статического анализа включают в себя: ^[14]

• Абстрактная интерпретация , для моделирования эффекта, который каждое утверждение оказывает на состояние абстрактной машины (т. е. она «выполняет» программное обеспечение на основе математических свойств каждого утверждения и декларации). Эта абстрактная машина чрезмерно аппроксимирует поведение системы: абстрактная система, таким образом, упрощается для анализа за счет неполноты (не каждое свойство, истинное для исходной системы, истинно для абстрактной системы). Однако, если она сделана правильно, абстрактная интерпретация является обоснованной (каждое свойство, истинное для абстрактной системы, может быть отображено в истинное свойство исходной системы). ^[15]
• Анализ потока данных — метод сбора информации о возможном наборе значений на основе решеток;
• Логика Хоара , формальная система с набором логических правил для строгого рассуждения о корректности компьютерных программ . Существует поддержка инструментов для некоторых языков программирования (например, языка программирования SPARK (подмножество Ada ) и языка моделирования Java —JML — с использованием ESC/Java и ESC/Java2 , плагина Frama-C WP ( слабейшее предварительное условие ) для языка C, расширенного с помощью ACSL ( язык спецификации ANSI/ISO C )).
• Проверка моделей рассматривает системы, которые имеют конечное состояние или могут быть сведены к конечному состоянию путем абстракции ;
• Символьное выполнение , используемое для вывода математических выражений, представляющих значения измененных переменных в определенных точках кода.

Статический анализ на основе данных

Статический анализ на основе данных использует обширные кодовые базы для вывода правил кодирования и повышения точности анализа. ^{[16] [17]} Например, можно использовать все пакеты Java с открытым исходным кодом, доступные на GitHub, чтобы изучить хорошие стратегии анализа. Вывод правил может использовать методы машинного обучения. ^[18] Также можно учиться на большом количестве прошлых исправлений и предупреждений. ^[16]

Ремедиация

Статические анализаторы выдают предупреждения. Для некоторых типов предупреждений можно разработать и реализовать автоматизированные методы исправления . Например, Логоззо и Болл предложили автоматизированные методы исправления для C# cccheck . ^[19]

Смотрите также

• Аудит кода
• Генератор документации
• Формальная семантика языков программирования
• Формальная проверка
• ФХ-87
• ИСО 26262
• ISO 9126 (теперь серия ISO 25000)
• Линт (программное обеспечение)
• Список инструментов для статического анализа кода
• Анализ формы
• Качество программного обеспечения
• Обеспечение качества программного обеспечения
• SonarQube

Ссылки

1. Wichmann, BA; Canning, AA; Clutterbuck, DL; Winsbarrow, LA; Ward, NJ; Marsh, DWR (март 1995). "Industrial Perspective on Static Analysis" (PDF) . Software Engineering Journal . 10 (2): 69–75. doi :10.1049/sej.1995.0010. Архивировано из оригинала (PDF) 27.09.2011.
2. Эгеле, Мануэль; Шольте, Теодор; Кирда, Энгин; Кругель, Кристофер (2008-03-05). «Обзор автоматизированных методов и инструментов динамического анализа вредоносных программ». ACM Computing Surveys . 44 (2): 6:1–6:42. doi :10.1145/2089125.2089126. ISSN  0360-0300. S2CID  1863333.
3. Хативада, Сакет; Тушев, Мирослав; Махмуд, Анас (2018-01-01). «Достаточно семантики: Информационно-теоретический подход к локализации ошибок программного обеспечения на основе IR». Информационные и программные технологии . 93 : 45–57. doi :10.1016/j.infsof.2017.08.012.
4. "Software Quality Objectives for Source Code" Архивировано 2015-06-04 в Wayback Machine (PDF). Труды: Embedded Real Time Software and Systems Conference 2010 , ERTS2010.org, Тулуза, Франция: Патрик Бриан, Мартин Броше, Тьерри Камбуа, Эммануэль Кутенсо, Оливье Гетта, Даниэль Майнберт, Фредерик Мондо, Патрик Мунье, Луик Нури, Филипп Споцио, Фредерик Ретайо.
5. Улучшение безопасности программного обеспечения с помощью точного статического и динамического анализа Архивировано 05.06.2011 на Wayback Machine (PDF), Бенджамин Лившиц, раздел 7.3 «Статические методы обеспечения безопасности». Докторская диссертация в Стэнфорде, 2006.
6. FDA (2010-09-08). "Исследование безопасности программного обеспечения инфузионных насосов в FDA". Управление по контролю за продуктами питания и лекарственными средствами. Архивировано из оригинала 2010-09-01 . Получено 2010-09-09 .
7. Компьютерные системы безопасности - техническое руководство по оценке аспектов программного обеспечения цифровых компьютерных систем защиты, "Компьютерные системы безопасности" (PDF) . Архивировано из оригинала (PDF) 4 января 2013 г. . Получено 15 мая 2013 г. .
8. Позиционный документ CAST-9. Соображения по оценке подходов к обеспечению безопасности программного обеспечения. Архивировано 06.10.2013 в Wayback Machine // FAA, Группа сертификационных органов по программному обеспечению (CAST), январь 2002 г.: «Проверка. Сочетание статического и динамического анализа должно быть указано заявителем/разработчиком и применено к программному обеспечению».
9. VDC Research (2012-02-01). "Автоматизированное предотвращение дефектов для обеспечения качества встроенного программного обеспечения". VDC Research. Архивировано из оригинала 2012-04-11 . Получено 2012-04-10 .
10. Prause, Christian R., René Reiners и Silviya Dencheva. "Эмпирическое исследование поддержки инструментов в высокораспределенных исследовательских проектах". Global Software Engineering (ICGSE), 2010 5-я Международная конференция IEEE по. IEEE, 2010 https://ieeexplore.ieee.org/Xplore/login.jsp?url=%2Fielx5%2F5581168%2F5581493%2F05581551.pdf&authDecision=-203
11. М. Ховард и С. Липнер. Жизненный цикл разработки безопасности: SDL: процесс разработки явно более безопасного программного обеспечения. Microsoft Press, 2006. ISBN 978-0735622142 
12. Ахим Д. Брукер и Уве Содан. Развертывание статического тестирования безопасности приложений в больших масштабах. Архивировано 21 октября 2014 г. на Wayback Machine . В GI Sicherheit 2014. Lecture Notes in Informatics, 228, страницы 91–101, GI, 2014.
13. "OMG Whitepaper | CISQ - Консорциум по качеству информации и программного обеспечения" (PDF) . Архивировано (PDF) из оригинала 2013-12-28 . Получено 2013-10-18 .
14. Виджай Д'Сильва и др. (2008). "Обзор автоматизированных методов формальной проверки программного обеспечения" (PDF) . Transactions On CAD. Архивировано (PDF) из оригинала 2016-03-04 . Получено 2015-05-11 .
15. Джонс, Пол (2010-02-09). "Подход к проверке на основе формальных методов для анализа программного обеспечения медицинских устройств". Проектирование встроенных систем. Архивировано из оригинала 10 июля 2011 г. Получено 2010-09-09 .
16. "Учимся на чужих ошибках: анализ кода на основе данных". www.slideshare.net . 13 апреля 2015 г.
17. Сёдерберг, Эмма; Чёрч, Люк; Хёст, Мартин (2021-06-21). «Усовершенствования удобства использования статического анализа кода на основе открытых данных и их проблемы». Оценка и анализ в программной инженерии . EASE '21. Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 272–277. doi :10.1145/3463274.3463808. ISBN 978-1-4503-9053-8.
18. О, Хакджу; Ян, Хонсок; Йи, Квангын (2015). «Изучение стратегии адаптации анализа программ с помощью байесовской оптимизации». Труды Международной конференции ACM SIGPLAN 2015 года по объектно-ориентированному программированию, системам, языкам и приложениям — OOPSLA 2015. стр. 572–588. doi :10.1145/2814270.2814309. ISBN 9781450336895. S2CID  13940725.
19. Логоццо, Франческо; Болл, Томас (15.11.2012). «Модульный и проверенный автоматический ремонт программ». ACM SIGPLAN Notices . 47 (10): 133–146. doi :10.1145/2398857.2384626. ISSN  0362-1340.

Дальнейшее чтение

• Айева, Натаниэль; Ховемейер, Дэвид; Моргенталер, Дж. Дэвид; Пеникс, Джон; Пью, Уильям (2008). «Использование статического анализа для поиска ошибок». IEEE Software . 25 (5): 22–29. CiteSeerX  10.1.1.187.8985 . doi :10.1109/MS.2008.130. S2CID  20646690.
• Брайан Чесс, Джейкоб Уэст (Fortify Software) (2007). Безопасное программирование со статическим анализом . Addison-Wesley. ISBN 978-0-321-42477-8.
• Флемминг Нильсон; Ханне Р. Нильсон; Крис Ханкин (2004-12-10). Принципы анализа программ (ред. 1999 (исправлено в 2004 г.)). Springer. ISBN 978-3-540-65410-0.
• «Абстрактная интерпретация и статический анализ», Международная зимняя школа по семантике и приложениям 2003 г., Дэвид А. Шмидт