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

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

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

Обоснование [ править ]

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

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

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

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

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

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

Типы инструментов [ править ]

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

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

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

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

Формальные методы [ править ]

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

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

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

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

Статический анализ на основе данных [ править ]

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

Исправление [ править ]

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

См. также [ править ]

Ссылки [ править ]

^ Вичманн, бакалавр; Каннинг, А.А.; Клаттербак, ДЛ; Уинсбарроу, Луизиана; Уорд, Нью-Джерси; Марш, DWR (март 1995 г.). «Промышленный взгляд на статический анализ» (PDF) . Журнал программной инженерии . 10 (2): 69–75. дои : 10.1049/sej.1995.0010 . Архивировано из оригинала (PDF) 27 сентября 2011 г.
^ Эгеле, Мануэль; Шольте, Теодор; Кирда, Энгин; Крюгель, Кристофер (5 марта 2008 г.). «Опрос по методам и инструментам автоматизированного динамического анализа вредоносного ПО» . Обзоры вычислительной техники ACM . 44 (2): 6:1–6:42. дои : 10.1145/2089125.2089126 . ISSN 0360-0300 . S2CID 1863333 .
^ Хативада, Сакет; Тушев, Мирослав; Махмуд, Анас (01 января 2018 г.). «Семантики ровно столько: теоретико-информационный подход для локализации ошибок программного обеспечения на основе ИК» . Информационные и программные технологии . 93 : 45–57. дои : 10.1016/j.infsof.2017.08.012 .
^ «Цели качества программного обеспечения для исходного кода». Архивировано 4 июня 2015 г. в Wayback Machine (PDF). Материалы: Конференция Embedded Real Time Software and Systems 2010 , ERTS2010.org, Тулуза, Франция: Патрик Бриан, Мартен Броше, Тьерри Камбуа, Эммануэль Кутенсо, Оливье Гетта, Даниэль Менберт, Фредерик Мондо, Патрик Мунье, Лоик Нури, Филипп Спозио, Фредерик Розничная торговля.
^ Повышение безопасности программного обеспечения с помощью точного статического анализа и анализа времени выполнения. Архивировано 5 июня 2011 г. в Wayback Machine (PDF), Бенджамин Лившиц, раздел 7.3 «Статические методы обеспечения безопасности». Докторская диссертация в Стэнфорде, 2006 г.
^ FDA (08 сентября 2010 г.). «Исследование безопасности программного обеспечения инфузионных насосов в FDA» . Управление по контролю за продуктами и лекарствами. Архивировано из оригинала 1 сентября 2010 г. Проверено 9 сентября 2010 г.
^ Компьютерные системы безопасности - техническое руководство по оценке аспектов программного обеспечения цифровых компьютерных систем защиты, «Компьютерные системы безопасности» (PDF) . Архивировано из оригинала (PDF) 4 января 2013 года . Проверено 15 мая 2013 г.
^ Документ с изложением позиции CAST-9. Соображения по оценке подходов к обеспечению безопасности программного обеспечения. Архивировано 6 октября 2013 г. на Wayback Machine // FAA, Группа программного обеспечения органов сертификации (CAST), январь 2002 г.: «Верификация. Сочетание статического и динамического анализа должно быть указано заявителем/разработчиком и применено к программному обеспечению».
^ Исследования ВДК (01 февраля 2012 г.). «Автоматическое предотвращение дефектов для обеспечения качества встроенного программного обеспечения» . Исследования ВДЦ. Архивировано из оригинала 11 апреля 2012 г. Проверено 10 апреля 2012 г.
^ Прауз, Кристиан Р., Рене Райнерс и Сильвия Денчева. «Эмпирическое исследование инструментальной поддержки в сильно распределенных исследовательских проектах». Глобальная разработка программного обеспечения (ICGSE), 2010 г. 5-я Международная конференция IEEE. IEEE, 2010 г. http://ieeexplore.ieee.org/ielx5/5581168/5581493/05581551.pdf
^ М. Ховард и С. Липнер. Жизненный цикл разработки безопасности: SDL: процесс разработки явно более безопасного программного обеспечения. Майкрософт Пресс, 2006. ISBN 978-0735622142
^ Ахим Д. Брукер и Уве Содан. Развертывание статического тестирования безопасности приложений в больших масштабах. Архивировано 21 октября 2014 г. на Wayback Machine . В GI Sicherheit 2014. Конспект лекций по информатике, 228, стр. 91-101, GI, 2014.
^ «Информационный документ OMG | CISQ — Консорциум по качеству информации и программного обеспечения» (PDF) . Архивировано (PDF) из оригинала 28 декабря 2013 г. Проверено 18 октября 2013 г.
^ Виджай Д'Сильва; и др. (2008). «Обзор автоматизированных методов формальной проверки программного обеспечения» (PDF) . Транзакции в CAD. Архивировано (PDF) из оригинала 4 марта 2016 г. Проверено 11 мая 2015 г.
^ Джонс, Пол (9 февраля 2010 г.). «Подход к анализу программного обеспечения медицинского оборудования, основанный на формальных методах» . Проектирование встроенных систем. Архивировано из оригинала 10 июля 2011 года . Проверено 9 сентября 2010 г.
^ Jump up to: Перейти обратно: ^а ^б «Учимся на чужих ошибках: анализ кода на основе данных» . www.slideshare.net . 13 апреля 2015 г.
^ О, Хакджу; Ян, Хонсок; Йи, Квангын (2015). «Изучение стратегии адаптации программного анализа посредством байесовской оптимизации». Материалы Международной конференции ACM SIGPLAN 2015 по объектно-ориентированному программированию, системам, языкам и приложениям — OOPSLA 2015 . стр. 572–588. дои : 10.1145/2814270.2814309 . ISBN 9781450336895 . S2CID 13940725 .
^ Логоццо, Франческо; Болл, Томас (15 ноября 2012 г.). «Модульная и проверенная автоматическая программа восстановления» . Уведомления ACM SIGPLAN . 47 (10): 133–146. дои : 10.1145/2398857.2384626 . ISSN 0362-1340 .

Дальнейшее чтение [ править ]

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

[1] Вичманн, бакалавр; Каннинг, А.А.; Клаттербак, ДЛ; Уинсбарроу, Луизиана; Уорд, Нью-Джерси; Марш, DWR (март 1995 г.). «Промышленный взгляд на статический анализ» (PDF) . Журнал программной инженерии . 10 (2): 69–75. дои : 10.1049/sej.1995.0010 . Архивировано из оригинала (PDF) 27 сентября 2011 г.

[2] Эгеле, Мануэль; Шольте, Теодор; Кирда, Энгин; Крюгель, Кристофер (5 марта 2008 г.). «Опрос по методам и инструментам автоматизированного динамического анализа вредоносного ПО» . Обзоры вычислительной техники ACM . 44 (2): 6:1–6:42. дои : 10.1145/2089125.2089126 . ISSN 0360-0300 . S2CID 1863333 .

[3] Хативада, Сакет; Тушев, Мирослав; Махмуд, Анас (01 января 2018 г.). «Семантики ровно столько: теоретико-информационный подход для локализации ошибок программного обеспечения на основе ИК» . Информационные и программные технологии . 93 : 45–57. дои : 10.1016/j.infsof.2017.08.012 .

[4] «Цели качества программного обеспечения для исходного кода». Архивировано 4 июня 2015 г. в Wayback Machine (PDF). Материалы: Конференция Embedded Real Time Software and Systems 2010 , ERTS2010.org, Тулуза, Франция: Патрик Бриан, Мартен Броше, Тьерри Камбуа, Эммануэль Кутенсо, Оливье Гетта, Даниэль Менберт, Фредерик Мондо, Патрик Мунье, Лоик Нури, Филипп Спозио, Фредерик Розничная торговля.

[5] Повышение безопасности программного обеспечения с помощью точного статического анализа и анализа времени выполнения. Архивировано 5 июня 2011 г. в Wayback Machine (PDF), Бенджамин Лившиц, раздел 7.3 «Статические методы обеспечения безопасности». Докторская диссертация в Стэнфорде, 2006 г.

[6] FDA (08 сентября 2010 г.). «Исследование безопасности программного обеспечения инфузионных насосов в FDA» . Управление по контролю за продуктами и лекарствами. Архивировано из оригинала 1 сентября 2010 г. Проверено 9 сентября 2010 г.

[7] Компьютерные системы безопасности - техническое руководство по оценке аспектов программного обеспечения цифровых компьютерных систем защиты, «Компьютерные системы безопасности» (PDF) . Архивировано из оригинала (PDF) 4 января 2013 года . Проверено 15 мая 2013 г.

[8] Документ с изложением позиции CAST-9. Соображения по оценке подходов к обеспечению безопасности программного обеспечения. Архивировано 6 октября 2013 г. на Wayback Machine // FAA, Группа программного обеспечения органов сертификации (CAST), январь 2002 г.: «Верификация. Сочетание статического и динамического анализа должно быть указано заявителем/разработчиком и применено к программному обеспечению».

[9] Исследования ВДК (01 февраля 2012 г.). «Автоматическое предотвращение дефектов для обеспечения качества встроенного программного обеспечения» . Исследования ВДЦ. Архивировано из оригинала 11 апреля 2012 г. Проверено 10 апреля 2012 г.

[10] Прауз, Кристиан Р., Рене Райнерс и Сильвия Денчева. «Эмпирическое исследование инструментальной поддержки в сильно распределенных исследовательских проектах». Глобальная разработка программного обеспечения (ICGSE), 2010 г. 5-я Международная конференция IEEE. IEEE, 2010 г. http://ieeexplore.ieee.org/ielx5/5581168/5581493/05581551.pdf

[11] М. Ховард и С. Липнер. Жизненный цикл разработки безопасности: SDL: процесс разработки явно более безопасного программного обеспечения. Майкрософт Пресс, 2006. ISBN 978-0735622142

[12] Ахим Д. Брукер и Уве Содан. Развертывание статического тестирования безопасности приложений в больших масштабах. Архивировано 21 октября 2014 г. на Wayback Machine . В GI Sicherheit 2014. Конспект лекций по информатике, 228, стр. 91-101, GI, 2014.

[13] «Информационный документ OMG | CISQ — Консорциум по качеству информации и программного обеспечения» (PDF) . Архивировано (PDF) из оригинала 28 декабря 2013 г. Проверено 18 октября 2013 г.

[14] Виджай Д'Сильва; и др. (2008). «Обзор автоматизированных методов формальной проверки программного обеспечения» (PDF) . Транзакции в CAD. Архивировано (PDF) из оригинала 4 марта 2016 г. Проверено 11 мая 2015 г.

[15] Джонс, Пол (9 февраля 2010 г.). «Подход к анализу программного обеспечения медицинского оборудования, основанный на формальных методах» . Проектирование встроенных систем. Архивировано из оригинала 10 июля 2011 года . Проверено 9 сентября 2010 г.

[dewes-16] Jump up to: Перейти обратно: ^а ^б «Учимся на чужих ошибках: анализ кода на основе данных» . www.slideshare.net . 13 апреля 2015 г.

[OhYang2015-17] О, Хакджу; Ян, Хонсок; Йи, Квангын (2015). «Изучение стратегии адаптации программного анализа посредством байесовской оптимизации». Материалы Международной конференции ACM SIGPLAN 2015 по объектно-ориентированному программированию, системам, языкам и приложениям — OOPSLA 2015 . стр. 572–588. дои : 10.1145/2814270.2814309 . ISBN 9781450336895 . S2CID 13940725 .

[18] Логоццо, Франческо; Болл, Томас (15 ноября 2012 г.). «Модульная и проверенная автоматическая программа восстановления» . Уведомления ACM SIGPLAN . 47 (10): 133–146. дои : 10.1145/2398857.2384626 . ISSN 0362-1340 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]