Frama-C [1] son las siglas de Framework for Modular Analysis of C programas . Frama-C es un conjunto de interoperables analizadores de programas para programas en C . Frama-C ha sido desarrollado por el Commissariat à l'Énergie Atomique et aux Énergies Alternatives ( CEA-List ) francés [2] e Inria . También ha recibido financiación de la Iniciativa de Infraestructura Central . Frama-C, como analizador estático , inspecciona programas sin ejecutarlos. A pesar de su nombre, el software no está relacionado con el proyecto francés Framasoft .
Desarrollador (es) | Commissariat à l'Énergie Atomique ( Lista CEA ) e Inria |
---|---|
Repositorio | |
Escrito en | OCaml |
Sistema operativo | Microsoft Windows , FreeBSD , OpenBSD , Linux , Mac OS X |
Disponible en | inglés |
Tipo | Verificación formal , análisis de código estático |
Licencia | principalmente LGPL , algunas partes bajo licencias BSD |
Sitio web | frama-c |
Arquitectura
Frama-C tiene una arquitectura de complementos modular [3] comparable a la de Eclipse (software) o GIMP .
Frama-C se basa en CIL ( C Intermediate Language ) para generar un árbol de sintaxis abstracto . El árbol de sintaxis abstracta admite anotaciones escritas en lenguaje de especificación ANSI / ISO C (ACSL).
Varios módulos pueden manipular el árbol de sintaxis abstracta para agregar anotaciones ANSI / ISO C Specification Language (ACSL). Entre los complementos [ vagos ] de uso frecuente se encuentran:
- Análisis de valor : calcula un valor o un conjunto de valores posibles para cada variable de un programa. Este complemento utiliza técnicas de interpretación abstracta y muchos otros complementos hacen uso de sus resultados.
- Jessie : verifica las propiedades de forma deductiva. Jessie se basa en el back-end Why [4] o Why3 para permitir que las obligaciones de prueba se envíen a probadores automáticos de teoremas como Z3, Simplify, Alt-Ergo o probadores interactivos de teoremas como Coq o Why. Usando Jessie, se puede demostrar que una implementación de clasificación de burbujas o un sistema de votación electrónica de juguete satisface sus especificaciones respectivas. Utiliza un modelo de memoria de separación inspirado en la lógica de separación .
- WP (condición previa más débil) : similar a Jessie , verifica las propiedades de manera deductiva. A diferencia de Jessie, se centra en la parametrización con respecto al modelo de memoria. WP está diseñado para cooperar con otros complementos de Frama-C, como el complemento de análisis de valor, a diferencia de Jessie que compila el programa C directamente en el lenguaje Why. WP puede utilizar opcionalmente la plataforma Why3 para invocar a muchos otros probadores automatizados e interactivos.
- Análisis de impacto : destaca los impactos de una modificación en el código fuente de C.
- Cortar : permite cortar un programa . Permite la generación de un nuevo programa en C más pequeño que conserva algunas propiedades dadas. [5]
- Código de repuesto : elimina el código inútil de un programa en C.
Otros complementos son:
- Dominadores : calcula dominadores y posdominadores de declaraciones.
- A partir del análisis : calcula las dependencias funcionales.
Características
Frama-C se puede utilizar para los siguientes propósitos:
- Para comprender el código C que no ha escrito. En particular, Frama-C permite observar un conjunto de valores, dividir el programa en programas más cortos y navegar en el programa.
- Demostrar propiedades formales del código. El uso de especificaciones escritas en lenguaje de especificación ANSI / ISO C le permite garantizar las propiedades del código para cualquier posible comportamiento. Frama-C maneja números de coma flotante. [6]
- Para hacer cumplir los estándares de codificación o las convenciones de código en el código fuente C, mediante complementos personalizados [7]
- Instrumentar el código C contra algunas fallas de seguridad [8]
Ver también
- SPARK (lenguaje de programación)
Referencias
- ^ "Frama-C" . frama-c.com . Consultado el 5 de noviembre de 2016 .
- ^ LISTA CEA. "LISTA CEA, Sistemas digitales inteligentes" . Consultado el 5 de noviembre de 2016 .
- ^ Pascal Cuoq; et al. (Agosto de 2009). "Informe de experiencia: OCaml para un marco de análisis estático de fuerza industrial". Actas de la 14ª Conferencia Internacional ACM SIGPLAN sobre Programación Funcional . 44 (9): 281-286. doi : 10.1145 / 1631687.1596591 .
- ^ "Por qué página de inicio" .
- ^ Benjamin Monate; Julien Signoles (2008). "Rebanado para la seguridad del código". Computación confiable: desafíos y aplicaciones . Apuntes de conferencias en Ciencias de la Computación. 4968/2008. doi : 10.1007 / 978-3-540-68979-9_10 . ISBN 978-3-540-68978-2.
- ^ Sylvie Boldo; Thi Minh Tuyen Nguyen (2010). "Pruebas de programas numéricos independientes del hardware" (PDF) . Actas de NFM 2010 .
- ^ David Delmas; Stéphane Duprat; Victoria Moya Lamiel; Julien Signoles. "Taster, un complemento de Frama-C para hacer cumplir los estándares de codificación" (PDF) . Software y sistemas integrados en tiempo real 2010, Toulouse, Francia .
- ^ Jonathan-Christofer Demay; Éric Totel; Frédéric Tronel (2009). "Instrumentación automática de software para la detección de ataques de datos ajenos a control". Avances recientes en la detección de intrusiones . Apuntes de conferencias en Ciencias de la Computación. 5758/2009. págs. 348–349. doi : 10.1007 / 978-3-642-04342-0_19 . ISBN 978-3-642-04341-3.
enlaces externos
- Página web oficial
- Lista de discusión de Frama-C
- Sistema de seguimiento de errores Frama-C