Астре (статический анализ) - Википедия - Astrée (static analysis)
Astrée ("Ааналитик statique de logiciels тemps-реэль еmbarqués "[1]) это статический анализатор на основе абстрактная интерпретация. Он анализирует программы, написанные на язык программирования C и выводит исчерпывающий список возможных ошибок времени выполнения и утверждение нарушения. Охватываемые классы дефектов включают деления на ноль, переполнение буфера, разыменования ноль или же висячие указатели, гонки данных, тупиковые ситуации и т. д. Astrée включает статический taint checker и помогает найти уязвимости кибербезопасности, Такие как Призрак.
Инструмент адаптирован к критически важному для безопасности встроенному коду: специальные методы анализа используются для общих теория управления конструкции (конечные автоматы, цифровые фильтры, ограничители скорости ...) и плавающая точка числа.
Параллельный код анализируется с помощью семантики звукового чередования, которая учитывает параллельные потоки исполнения, их приоритеты и механизмы синхронизации. Астре поддерживает ARINC 653, OSEK и АВТОСАР модели исполнения и могут быть адаптированы к дополнительным спецификациям ОС. На многоядерные процессоры размещение потоков в ядрах и использование мьютексные блокировки и спин-блокировки принимаются во внимание.
Astrée была разработана в Патрик Кузо группа в École Normale Supérieure, совместная группа с CNRS, и продается AbsInt GmbH. Он используется в оборонной / аэрокосмической, промышленной, электронной и автомобильной промышленности. Одним из основных промышленных пользователей является Airbus.[2]
Astrée - коммерческий продукт, доступный от AbsInt Angewandte Informatik.
Смотрите также
Библиография
- Бруно Бланше, Патрик Кузо, Радия Кузо, Жером Фере, Лоран Моборн, Антуан Мине, Давид Моннио и Ксавье Риваль. Разработка и внедрение специального анализатора статических программ для критически важного для безопасности встроенного программного обеспечения реального времени, пригласил главу. В Суть вычислений: сложность, анализ, трансформация. Очерки, посвященные Нилу Д. Джонсу, Т. Могенсен, Д.А. Шмидт и И. Садборо (редакторы). Том 2566 конспектов лекций по информатике, стр. 85–108, Springer. Дои:10.1007/3-540-36377-7_5
- Бруно Бланше, Патрик Кузо, Радия Кузо, Жером Фере, Лоран Моборн, Антуан Мине, Давид Моннио и Ксавье Риваль, Статический анализатор для крупного программного обеспечения, критически важного для безопасности., В PLDI 2003 - Конференция ACM SIGPLAN SIGSOFT по проектированию и реализации языков программирования, Конференция по исследованиям федеративных вычислений 2003 г., 7–14 июня 2003 г., Сан-Диего, Калифорния, США, стр. 196–207, ACM. Дои:10.1145/781131.781153
- Дэвид Дельмас и Жан Суйрис. Astrée: от исследований к промышленности., Proc. 14-й Международный симпозиум по статическому анализу, SAS 2007, Г. Филе и Х. Риис-Нильсон (редакторы), Kongens Lyngby, Дания, 22–24 августа 2007 г., LNCS 4634, стр. 437–451
- Арно Дж. Венет и Майкл Р. Лоури. 2010. Статический анализ для обеспечения безопасности программного обеспечения: надежность, масштабируемость и адаптивность. В материалах семинара FSE / SDP о будущем исследований в области программной инженерии (FoSER '10). ACM, Нью-Йорк, Нью-Йорк, США, 393-396. Дои:10.1145/1882362.1882442
- Жан-Луи Буланже. Статический анализ программного обеспечения: абстрактная интерпретация. ISBN 978-1-84821-320-3. Вайли.
- Даниэль Кестнер, Стефан Вильгельм, Стефана Ненова, Патрик Кузо, Радия Кузо, Жером Фере, Лоран Моборн, Антуан Мине, Ксавье Риваль. Астре: Доказательство отсутствия ошибок времени выполнения. Конгресс по встроенному ПО и системам реального времени ERTS², Тулуза, 2010 г.
- А. Мине, Л. Моборн, X. Соперник, Ж. Ферет, П. Кузо, Д. Кестнер, С. Вильгельм, К. Фердинанд. Вывод статического анализа на новый уровень: доказательство отсутствия ошибок времени выполнения и гонок данных с помощью Astrée. В ERTS 2016: Встроенное программное обеспечение и системы реального времени, 8-й Европейский Конгресс, январь 2016 г., Тулуза, Франция.
- Д. Кестнер, Л. Моборн, Н. Графе, К. Фердинанд. Расширенный статический анализ звука для обнаружения программных дефектов, связанных с безопасностью. 8-й Международный журнал о достижениях в области безопасности, ISSN 1942-2636, т. 11, вып. 1 & 2, 149-159, IARIA, 2018.
- Д. Кестнер, Б. Шмидт, М. Шлундт, Л. Моборн, С. Вильгельм, К. Фердинанд. Проанализируйте это! Звуковой статический анализ для проверки интеграции крупномасштабного автомобильного программного обеспечения. Технический доклад SAE 2019-01-1246, Всемирный конгресс SAE 2019, Детройт, апрель 2019 г. Дои:10.4271/2019-01-1246