SPARK es un lenguaje de programación informática definido formalmente basado en el lenguaje de programación Ada , destinado al desarrollo de software de alta integridad utilizado en sistemas donde el funcionamiento predecible y altamente confiable es esencial. Facilita el desarrollo de aplicaciones que exigen seguridad, protección o integridad empresarial.
Originalmente, había tres versiones del lenguaje SPARK (SPARK83, SPARK95, SPARK2005) basadas en Ada 83, Ada 95 y Ada 2005 respectivamente.
El 30 de abril de 2014 se lanzó una cuarta versión del lenguaje SPARK, SPARK 2014, basada en Ada 2012. SPARK 2014 es un rediseño completo del lenguaje y las herramientas de verificación que lo respaldan .
El lenguaje SPARK consiste en un subconjunto bien definido del lenguaje Ada que utiliza contratos para describir la especificación de componentes en una forma que es adecuada tanto para la verificación estática como dinámica.
En SPARK83/95/2005, los contratos están codificados en comentarios de Ada y, por lo tanto, son ignorados por cualquier compilador de Ada estándar, pero son procesados por el "Examinador" de SPARK y sus herramientas asociadas.
SPARK 2014, por el contrario, utiliza la sintaxis de "aspecto" incorporada de Ada 2012 para expresar contratos, llevándolos al núcleo del lenguaje. La herramienta principal de SPARK 2014 (GNATprove) se basa en la infraestructura GNAT/GCC y reutiliza casi la totalidad del front-end de GNAT Ada 2012.
SPARK aprovecha las ventajas de Ada y trata de eliminar todas sus posibles ambigüedades y construcciones inseguras. Los programas SPARK están diseñados para ser inequívocos y su comportamiento no debe verse afectado por la elección del compilador de Ada . Estos objetivos se logran en parte omitiendo algunas de las características más problemáticas de Ada (como la ejecución de tareas paralelas sin restricciones ) y en parte introduciendo contratos que codifican las intenciones y los requisitos del diseñador de la aplicación para ciertos componentes de un programa.
La combinación de estos enfoques permite a SPARK cumplir sus objetivos de diseño, que son:
Considere la siguiente especificación del subprograma Ada:
procedimiento Incremento (X : in out Counter_Type);
En Ada puro, esto podría incrementar la variable Xen uno o mil; o podría establecer un contador global en Xy devolver el valor original del contador en X; o podría no hacer absolutamente nada X.
Con SPARK 2014, se agregan contratos al código para brindar información adicional sobre lo que realmente hace un subprograma. Por ejemplo, podemos modificar la especificación anterior para que diga:
procedimiento Incrementar (X : in out Counter_Type) con Global => null , Depende => (X => X);
Esto especifica que el Incrementprocedimiento no utiliza (ni actualiza ni lee) ninguna variable global y que el único elemento de datos utilizado para calcular el nuevo valor Xes Xél mismo.
Alternativamente, el diseñador podría especificar:
procedimiento Incrementar (X : in_out Counter_Type) con Global => (In_Out => Count), Depende => (Contar => (Contar, X), X => nulo);
Esto especifica que Incrementse utilizará la variable global Counten el mismo paquete que Increment, que el valor exportado de Countdepende de los valores importados de County X, y que el valor exportado de Xno depende de ninguna variable y se derivará solo de datos constantes.
Si se ejecuta GNATprove sobre la especificación y el cuerpo correspondiente de un subprograma, analizará el cuerpo del subprograma para construir un modelo del flujo de información. Luego, este modelo se compara con el que se ha especificado mediante las anotaciones y las discrepancias se informan al usuario.
Estas especificaciones se pueden ampliar aún más al afirmar varias propiedades que deben cumplirse cuando se llama a un subprograma ( condiciones previas ) o que se cumplirán una vez que se haya completado la ejecución del subprograma ( condiciones posteriores ). Por ejemplo, podríamos decir lo siguiente:
procedimiento Incrementar (X : in out Counter_Type) con Global => null, Depende => (X => X), Pre => X < Counter_Type'Último, Publicación => X = X'Viejo + 1;
Esto, ahora, especifica no sólo que Xse deriva de sí mismo únicamente, sino también que before Incrementse llama Xdebe ser estrictamente menor que el último valor posible de su tipo (para asegurar que el resultado nunca se desbordará ) y que after Xserá igual al valor inicial de Xmás uno.
GNATprove también puede generar un conjunto de condiciones de verificación o VC. Estas condiciones se utilizan para establecer si ciertas propiedades se cumplen para un subprograma determinado. Como mínimo, GNATprove generará VC para establecer que no se pueden producir errores de tiempo de ejecución dentro de un subprograma, como por ejemplo:
Si se agrega una poscondición o cualquier otra afirmación a un subprograma, GNATprove también generará VC que requieren que el usuario demuestre que estas propiedades se cumplen para todas las rutas posibles a través del subprograma.
En segundo plano, GNATprove utiliza el lenguaje intermedio Why3 y el generador de comprobaciones de verificaciones, y los comprobadores de teoremas CVC4 , Z3 y Alt-Ergo para descargar comprobaciones de verificaciones. También es posible utilizar otros comprobadores (incluidos los comprobadores de pruebas interactivos) a través de otros componentes del conjunto de herramientas Why3.
La primera versión de SPARK (basada en Ada 83) fue producida en la Universidad de Southampton (con el patrocinio del Ministerio de Defensa del Reino Unido) por Bernard Carré y Trevor Jennings. El nombre SPARK se derivó de SPADE Ada Kernel , en referencia al subconjunto SPADE del lenguaje de programación Pascal . [1]
Posteriormente, el lenguaje se fue ampliando y refinando progresivamente, primero por Program Validation Limited y luego por Praxis Critical Systems Limited. En 2004, Praxis Critical Systems Limited cambió su nombre a Praxis High Integrity Systems Limited. En enero de 2010, la empresa pasó a llamarse Altran Praxis .
A principios de 2009, Praxis se asoció con AdaCore y lanzó "SPARK Pro" bajo los términos de la GPL. En junio de 2009, se lanzó SPARK GPL Edition 2009, dirigido a las comunidades académicas y de software libre .
En junio de 2010, Altran-Praxis anunció que el lenguaje de programación SPARK se utilizaría en el software del proyecto lunar estadounidense CubeSat , cuya finalización está prevista para 2015.
En enero de 2013, Altran-Praxis cambió su nombre a Altran, que en abril de 2021 se convirtió en Capgemini Engineering (tras la fusión de Altran con Capgemini ).
La primera versión Pro de SPARK 2014 se anunció el 30 de abril de 2014, y fue seguida rápidamente por la edición SPARK 2014 GPL, dirigida a las comunidades FLOSS y académicas.
SPARK se ha utilizado en varios sistemas críticos de seguridad de alto perfil, que abarcan la aviación comercial ( motores a reacción de la serie Rolls-Royce Trent , el sistema ARINC ACAMS, el Lockheed Martin C130J ), la aviación militar ( EuroFighter Typhoon , Harrier GR9 , AerMacchi M346 ), la gestión del tráfico aéreo (sistema iFACTS de UK NATS), el ferrocarril (numerosas aplicaciones de señalización), la medicina (el dispositivo de asistencia ventricular LifeFlow ) y las aplicaciones espaciales (el proyecto CubeSat del Vermont Technical College ). [ cita requerida ]
SPARK también se ha utilizado en el desarrollo de sistemas seguros. Entre los usuarios se incluyen Rockwell Collins (soluciones multidominio Turnstile y SecureOne), el desarrollo del CA MULTOS original , el demostrador NSA Tokeneer, la estación de trabajo multinivel secunet, el núcleo de separación Muen y el cifrador de dispositivos de bloque Genode .
En agosto de 2010, Rod Chapman, ingeniero principal de Altran Praxis, implementó Skein , uno de los candidatos para SHA-3 , en SPARK. Al comparar el rendimiento de las implementaciones de SPARK y C y después de una cuidadosa optimización, logró que la versión de SPARK se ejecutara solo un 5 a 10% más lento que C. Una mejora posterior en la parte intermedia de Ada en GCC (implementada por Eric Botcazou de AdaCore) cerró la brecha, con el código de SPARK igualando exactamente al de C en rendimiento. [2]
NVIDIA también ha adoptado SPARK para la implementación de firmware crítico para la seguridad. [3]
En 2020, Rod Chapman volvió a implementar la biblioteca criptográfica TweetNaCl en SPARK 2014. [4] La versión SPARK de la biblioteca tiene una prueba autoactiva completa de seguridad de tipos, seguridad de memoria y algunas propiedades de corrección, y conserva algoritmos de tiempo constante en todo momento. El código SPARK también es significativamente más rápido que TweetNaCl.
.svg/1280px-Free_and_open-source_software_logo_(2009).svg.png){kind=logo}