Фрама-С - Frama-C
 | |
| Разработчики) | Commissariat à l'Énergie Atomique (CEA-Список ) и Inria |
|---|---|
| Написано в | OCaml |
| Операционная система | Майкрософт Виндоус, FreeBSD, OpenBSD, Linux, Mac OS X |
| Доступно в | английский |
| Тип | Формальная проверка, Статический анализ кода |
| Лицензия | по большей части LGPL, некоторые части под Лицензии BSD |
| Интернет сайт | фрама-с |
Фрама-С[1] означает Платформа для модульного анализа C программы. Frama-C - это набор совместимых программные анализаторы за C программы. Frama-C была разработана французской Commissariat à l'Énergie Atomique et aux Énergies Alternatives (CEA-Список )[2] и Inria. Он также получил финансирование от Инициатива базовой инфраструктуры. Фрама-С, как статический анализатор, проверяет программы, не выполняя их. Несмотря на название, программа не имеет отношения к французскому проекту. Framasoft.
Архитектура
Frama-C имеет модульную архитектуру плагинов.[3] сравнимо с Eclipse (программное обеспечение) или же GIMP.
Frama-C полагается на CIL (C Промежуточный язык ) для создания абстрактное синтаксическое дерево. абстрактное синтаксическое дерево поддерживает аннотации, написанные на Язык спецификаций ANSI / ISO C (ACSL).
Несколько модулей могут управлять абстрактное синтаксическое дерево добавить Язык спецификаций ANSI / ISO C (ACSL) аннотации. Среди часто используемых[нечеткий ] плагины:
- Анализ стоимости - вычисляет значение или набор возможных значений для каждой переменной в программе. Этот плагин использует абстрактная интерпретация методы и многие другие плагины используют его результаты.
- Джесси - проверяет свойства дедуктивным способом. Джесси полагается на то, почему[4] или серверная часть Why3, чтобы можно было отправлять доказательства обязательств автоматические средства доказательства теорем как Z3, Упростить, Альт-Эрго или же интерактивные средства доказательства теорем подобно Coq или почему. Используя Джесси, реализация пузырьковой сортировки или же игрушечная система электронного голосования может быть доказано, что они удовлетворяют их соответствующим спецификациям. Он использует модель разделительной памяти, вдохновленную логика разделения.
- WP (самое слабое предварительное условие) - похожий на Джесси, проверяет свойства дедуктивным способом. В отличие от Jessie, он фокусируется на параметризации в отношении модели памяти. 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. Получено 2016-11-05.
- ^ СПИСОК CEA. «CEA LIST, Умные цифровые системы». Получено 2016-11-05.
- ^ Паскаль Куок; и другие. (Август 2009 г.). «Отчет об опыте использования OCaml для структуры статического анализа промышленной прочности». Материалы 14-й Международной конференции ACM SIGPLAN по функциональному программированию. 44 (9): 281–286. Дои:10.1145/1631687.1596591.
- ^ "Почему главная страница".
- ^ Бенджамин Монате; Жюльен Синьолес (2008). «Нарезка для защиты кода». Надежные вычисления - проблемы и приложения. Конспект лекций по информатике. 4968/2008. Дои: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.