Фрама-С

Фрама-С
Разработчик(и)	Комиссия по атомной энергии ( CEA-List ) и Инрия
Репозиторий	мерзавец .frame-c .с /паб /frame-c ;
Написано в	OCaml
Операционная система	Microsoft Windows , FreeBSD , OpenBSD , Linux , Mac OS X
Доступно в	Английский
Тип	Формальная проверка , Статический анализ кода
Лицензия	в основном LGPL , некоторые части под лицензиями BSD
Веб-сайт	кадр-с .с

Фрама-С ^[1] расшифровывается как Framework for Modular Analysis of C-programs . Frama-C — набор совместимых анализаторов программ на языке C. Frama-C был разработан Французским комиссариатом по атомной энергии и альтернативным источникам энергии ( CEA-List ). ^[2] и Инрия . Он также получил финансирование от Core Infrastructure Initiative . Frama-C, как статический анализатор , проверяет программы, не выполняя их. Несмотря на свое название, программа не имеет отношения к французскому проекту Framasoft .

Архитектура

Frama-C имеет модульную архитектуру плагинов. ^[3] сравнимо с Eclipse (программное обеспечение) или GIMP .

Frama-C использует CIL ( промежуточный язык C ) для создания абстрактного синтаксического дерева .Дерево абстрактного синтаксиса поддерживает аннотации, написанные на языке спецификации ANSI/ISO C (ACSL).

Некоторые модули могут манипулировать абстрактным синтаксическим деревом для добавления аннотаций языка спецификации ANSI/ISO C (ACSL). Среди часто используемых ^{[ нечеткий ]} плагины:

Анализ значений – вычисляет значение или набор возможных значений для каждой переменной в программе. Этот плагин использует методы абстрактной интерпретации , и многие другие плагины используют его результаты.
Джесси – проверяет свойства дедуктивным способом. Джесси полагается на «Почему» ^[4] или серверную частьWhy3, чтобы обеспечить отправку обязательств по доказательству в автоматические средства доказательства теорем, такие как Z3, Simplify, Alt-Ergo , или интерактивные средства доказательства теорем, такие как Coq илиWhy. Используя Джесси, можно доказать, что реализация пузырьковой сортировки или игрушечной системы электронного голосования удовлетворяет соответствующим спецификациям. Он использует модель памяти разделения, основанную на логике разделения .
WP (Weakest Precondition) — аналогично Джесси , проверяет свойства дедуктивным способом. В отличие от Джесси, он фокусируется на параметризации модели памяти. WP предназначен для взаимодействия с другими плагинами Frama-C, такими как плагин анализа значений, в отличие от Jessie, который компилирует программу C непосредственно в языкWhy. WP может дополнительно использовать платформуWhy3 для запуска многих других автоматических и интерактивных средств проверки.
Анализ воздействия – подчеркивает влияние модификации исходного кода C.
Нарезка – позволяет нарезать программу . Это позволяет создавать новую программу на C меньшего размера, сохраняющую некоторые заданные свойства. ^[5]
Запасной код — удаляет ненужный код из программы на языке C.

Другие плагины:

Доминаторы – вычисляет доминаторы и постдоминаторы утверждений.
Из анализа – вычисляет функциональные зависимости.

Функции

Frama-C может использоваться для следующих целей:

Чтобы понять код C, который вы не писали. В частности, Frama-C позволяет наблюдать набор значений, разбивать программу на более короткие программы и перемещаться по программе.
Доказать формальные свойства кода. Использование спецификаций, написанных на языке спецификаций ANSI/ISO C, позволяет гарантировать свойства кода для любого возможного поведения. Frama-C обрабатывает числа с плавающей запятой. ^[6]
Для обеспечения соблюдения стандартов кодирования или соглашений о кодировании в исходном коде C с помощью пользовательских плагинов. ^[7]
Чтобы защитить код C от некоторых недостатков безопасности ^[8]

См. также

СПАРК (язык программирования)

Ссылки

^ «Фрама-С» . frama-c.com . Проверено 5 ноября 2016 г.
^ СПИСОК ЦЭА. «CEA LIST, Умные цифровые системы» . Проверено 5 ноября 2016 г.
^ Паскаль Куок; и др. (август 2009 г.). «Отчет об опыте: OCaml для промышленной среды статического анализа». Уведомления ACM SIGPLAN . 44 (9): 281–286. дои : 10.1145/1631687.1596591 .
^ «Почему домашняя страница» .
^ Бенджамин Монате; Жюльен Синьоль (2008). «Нарезка для безопасности кода». Доверенные вычисления – проблемы и приложения . Конспекты лекций по информатике. Том. 4968/2008. стр. 133–142. дои : 10.1007/978-3-540-68979-9_10 . ISBN 978-3-540-68978-2 .
^ Сильви Больдо ; Ти Минь Туен Нгуен (2010). «Аппаратно-независимые доказательства числовых программ» (PDF) . Материалы НФМ 2010 .
^ Дэвид Дельмас; Стефан Дюпра; Виктория Моя Ламиел; Жюльен Синьоль. «Taster, плагин Frama-C для обеспечения соблюдения стандартов кодирования» (PDF) . Встраиваемое программное обеспечение и системы реального времени 2010, Тулуза, Франция .
^ Джонатан-Кристофер Демэй; Эрик Тотель; Фредерик Тронель (2009). «Автоматическое программное обеспечение для обнаружения атак, не связанных с управляющими данными». Последние достижения в области обнаружения вторжений . Конспекты лекций по информатике. Том. 5758/2009. стр. 348–349. дои : 10.1007/978-3-642-04342-0_19 . ISBN 978-3-642-04341-3 .

Внешние ссылки

Официальный сайт
Список обсуждений Frama-C. Архивировано 30 декабря 2008 г. на Wayback Machine.
Система отслеживания ошибок Frama-C

[1] «Фрама-С» . frama-c.com . Проверено 5 ноября 2016 г.

[2] СПИСОК ЦЭА. «CEA LIST, Умные цифровые системы» . Проверено 5 ноября 2016 г.

[3] Паскаль Куок; и др. (август 2009 г.). «Отчет об опыте: OCaml для промышленной среды статического анализа». Уведомления ACM SIGPLAN . 44 (9): 281–286. дои : 10.1145/1631687.1596591 .

[4] «Почему домашняя страница» .

[5] Бенджамин Монате; Жюльен Синьоль (2008). «Нарезка для безопасности кода». Доверенные вычисления – проблемы и приложения . Конспекты лекций по информатике. Том. 4968/2008. стр. 133–142. дои : 10.1007/978-3-540-68979-9_10 . ISBN 978-3-540-68978-2 .

[6] Сильви Больдо ; Ти Минь Туен Нгуен (2010). «Аппаратно-независимые доказательства числовых программ» (PDF) . Материалы НФМ 2010 .

[7] Дэвид Дельмас; Стефан Дюпра; Виктория Моя Ламиел; Жюльен Синьоль. «Taster, плагин Frama-C для обеспечения соблюдения стандартов кодирования» (PDF) . Встраиваемое программное обеспечение и системы реального времени 2010, Тулуза, Франция .

[8] Джонатан-Кристофер Демэй; Эрик Тотель; Фредерик Тронель (2009). «Автоматическое программное обеспечение для обнаружения атак, не связанных с управляющими данными». Последние достижения в области обнаружения вторжений . Конспекты лекций по информатике. Том. 5758/2009. стр. 348–349. дои : 10.1007/978-3-642-04342-0_19 . ISBN 978-3-642-04341-3 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]