Hispanopedia Wiki
Articulo de referencia

SPARK (lenguaje de programación)

{{cite web|url=http://www.adacore.com/uploads/technical-papers/Ada2012_Rational_Introducion.pdf|title=Ada2012 Rationale|website=adacore.com|access-date=5 May 2018|url-status=liv...

Hispanopedia WikiContenido en espanolLectura gratuita

SPARK es un lenguaje de programación formalmente definido , basado en el lenguaje de programación Ada , diseñado para desarrollar software de alta integridad utilizado en sistemas donde la operación predecible y altamente confiable es esencial. Facilita el desarrollo de aplicaciones que requieren seguridad, protección o integridad empresarial. Se ha utilizado especialmente en computación en tiempo real y sistemas embebidos donde los aspectos de criticidad de seguridad o seguridad informática son primordiales. [ 2 ]

Originalmente, existían tres versiones de 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, SPARK 2014, basada en Ada 2012. SPARK 2014 supone un rediseño completo del lenguaje y es compatible con herramientas de verificación de software .

El lenguaje SPARK consiste en un subconjunto bien definido del lenguaje Ada que utiliza contratos para describir la especificación de componentes de una forma adecuada tanto para la verificación estática como dinámica. [ 3 ] SPARK también está diseñado para eliminar todas las construcciones del lenguaje que puedan causar un comportamiento impredecible. [ 4 ]

En SPARK83/95/2005, los contratos están codificados en comentarios Ada y, por lo tanto, son ignorados por cualquier compilador Ada estándar, pero son procesados ​​por SPARK Examiner y sus herramientas asociadas. Estas versiones anteriores se centran en la verificación estática de contratos. [ 3 ]

SPARK 2014, en cambio, utiliza la sintaxis de aspectos integrada de Ada 2012 para expresar contratos, incorporándolos al núcleo del lenguaje. La herramienta principal de SPARK 2014 (GNATprove) se basa en la infraestructura GNAT/GCC y reutiliza casi por completo la interfaz de usuario de GNAT Ada 2012.

Descripción general técnica

SPARK aprovecha las ventajas de Ada, procurando eliminar todas sus posibles ambigüedades y estructuras 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 paralela sin restricciones ) y, en parte, introduciendo contratos que codifican las intenciones y los requisitos del diseñador de la aplicación para ciertos componentes del programa.

La combinación de estos enfoques permite a SPARK cumplir con sus objetivos de diseño, que son:

  • solidez lógica
  • definición formal rigurosa
  • semántica simple
  • seguridad
  • poder expresivo
  • verificabilidad
  • requisitos de recursos limitados (espacio y tiempo).
  • requisitos mínimos del sistema en tiempo de ejecución

Un miembro del personal de Praxis ha dicho: "Nuestra tasa de defectos con Spark es al menos 10 veces, a veces 100 veces menor que la de aquellos creados con otros lenguajes". [ 4 ]

Ejemplos de contratos

Considere la siguiente especificación de subprograma Ada:

procedimiento Incremento (X : entrada salida Tipo_Contador);

En Ada puro, esto podría incrementar la variable Xen uno o en mil; o podría establecer algún contador global Xy devolver el valor original del contador en X; o podría no hacer nada con X.

Con SPARK 2014, se añaden contratos al código para proporcionar más información sobre lo que realmente hace un subprograma. Por ejemplo, la especificación anterior puede modificarse para decir:

procedimiento Incremento (X : entrada salida Tipo_Contador)  con Global => nulo , Depende => (X => X);

Esto especifica que el Incrementprocedimiento no utiliza ninguna variable global (ni de actualización ni de lectura) y que el único elemento de datos utilizado para calcular el nuevo valor Xes Xsolo.

Alternativamente, la especificación puede escribirse de la siguiente manera:

procedimiento Incremento (X : entrada salida Tipo_Contador)  con Global => (Entrada_Salida => Conteo), Depende => (Recuento => (Recuento, X), X => null);

Esto especifica que Incrementutilizará 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 en absoluto y se derivará únicamente de datos constantes.

Si se ejecuta GNATprove sobre la especificación y el cuerpo correspondiente de un subprograma, este analizará el cuerpo del subprograma para crear un modelo del flujo de información. Este modelo se compara con lo especificado en las anotaciones y se notifican al usuario las discrepancias.

Estas especificaciones pueden ampliarse aún más al afirmar diversas propiedades que deben cumplirse cuando se llama a un subprograma ( precondiciones ) o que se cumplirán una vez que la ejecución del subprograma haya finalizado ( postcondiciones ). Por ejemplo, si se escribe:

procedimiento Incremento (X : entrada salida Tipo_Contador)  con Global => nulo, Depende => (X => X), Pre => X < Counter_Type'Last, Post => X = X'Antiguo + 1;

Esto, ahora, especifica no solo que Xse deriva de sí mismo, sino también que antes de Incrementque se llame Xdebe ser estrictamente menor que el último valor posible de su tipo (para asegurar que el resultado nunca se desborde ) y que después Xserá igual al valor inicial de Xmás uno.

Condiciones de verificación

GNATprove también puede generar un conjunto de condiciones de verificación (CV). Estas se utilizan para determinar si se cumplen ciertas propiedades para un subprograma dado. Como mínimo, GNATprove generará CV para establecer que no pueden ocurrir errores en tiempo de ejecución dentro de un subprograma, tales como:

  • Índice de matriz fuera de rango
  • violación del rango de tipos
  • división por cero
  • desbordamiento numérico

Si se agrega una postcondición o cualquier otra aserción a un subprograma, GNATprove también generará VC que requerirán que el usuario demuestre que estas propiedades se cumplen para todas las rutas posibles a través del subprograma.

Internamente, GNATprove utiliza el lenguaje intermedio Why3 y el generador de VC [ 3 ] , así como los demostradores de teoremas CVC4 , Z3 y Alt-Ergo para descargar las VC. También es posible utilizar otros demostradores (incluidos verificadores de pruebas interactivos) mediante otros componentes del conjunto de herramientas Why3.

Historia

Los orígenes de esta tecnología se remontan a 1987, a partir de trabajos realizados en la Universidad de Southampton . [ 3 ] La primera versión de SPARK (basada en Ada 83) fue desarrollada en la universidad, con el patrocinio del Ministerio de Defensa del Reino Unido , por Bernard Carré y Trevor Jennings. El nombre SPARK deriva de SPADE Ada Kernel , en referencia al subconjunto SPADE del lenguaje de programación Pascal . [ 5 ]

Posteriormente, el lenguaje fue progresivamente ampliado y perfeccionado, 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, y el trabajo en SPARK continuó. [ 4 ] En enero de 2010, la empresa se convirtió en Altran Praxis .

A principios de 2009, Praxis se asoció con AdaCore y lanzó SPARK Pro bajo los términos de la GPL. Posteriormente, en junio de 2009, se lanzó SPARK GPL Edition 2009, dirigido a las comunidades de software libre y de código abierto (FOSS) y al ámbito académico.

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 ).

El primer lanzamiento de la versión Pro de SPARK 2014 se anunció el 30 de abril de 2014, y poco después le siguió la edición SPARK 2014 GPL, dirigida a las comunidades académicas y de software libre .

Aplicaciones industriales

SPARK se ha empleado en diversas aplicaciones industriales reales. Incorporarlo lo antes posible en el proceso de diseño suele ofrecer el resultado más favorable. [ 6 ]

SPARK se ha utilizado en varios sistemas críticos de seguridad de alto perfil, que abarcan la aviación comercial (el Sistema de Instrumentación de Límites Operacionales de Buques/Helicópteros, [ 6 ] los motores a reacción de la serie Trent de Rolls-Royce , el sistema ARINC ACAMS , el Lockheed Martin C130J [ 6 ] ), la aviación militar ( EuroFighter Typhoon , [ 3 ] Harrier GR9 , AerMacchi M346 ), la gestión del tráfico aéreo ( sistema UK NATS iFACTS [ 3 ] ), el ferrocarril (numerosas aplicaciones de señalización), el sector médico (el dispositivo de asistencia ventricular LifeFlow ) y las aplicaciones espaciales (el proyecto CubeSat del Vermont Technical College [ 7 ] ).

En cuanto a los procesos de aprobación necesarios para dichos sistemas, SPARK se ha utilizado para certificar según el estándar de defensa del Reino Unido (DEFSTAN) 00-55, [ 3 ] así como según el DO-178B Nivel A e ITSEC E6. [ 6 ]

SPARK también se ha utilizado en el desarrollo de sistemas seguros. Entre sus usuarios se incluyen Rockwell Collins (soluciones de dominio cruzado Turnstile y SecureOne), el desarrollo de la CA MULTOS original , [ 6 ] el demostrador NSA Tokeneer , [ 3 ] la estación de trabajo multinivel secunet, el núcleo de separación Muen y el cifrador de dispositivos de bloques Genode . Otro caso fue la implementación de una Autoridad de Certificación segura para la tarjeta de valor almacenado producida por Mondex International , en la que se utilizó la notación Z como precursora de la codificación en SPARK. [ 4 ]

En agosto de 2010, Rod Chapman, ingeniero principal de Altran Praxis, implementó Skein , uno de los candidatos a SHA-3 , en SPARK. Tras una cuidadosa optimización, logró que la versión de SPARK funcionara solo entre un 5 % y un 10 % más lento que la implementación en C. Las mejoras posteriores en el middleware de Ada en GCC (implementadas por Eric Botcazou de AdaCore) redujeron la diferencia, y el código de SPARK igualó el rendimiento del código en C exactamente. [ 2 ]

NVIDIA también ha adoptado SPARK para la implementación de firmware crítico para la seguridad . [ 8 ] [ 9 ] Al encontrar éxito en esto, la compañía agregó SPARK para proyectos adicionales relacionados con el firmware y comenzó la capacitación interna en el uso de la tecnología SPARK. [ 3 ]

En 2020, Rod Chapman reimplementó la biblioteca criptográfica TweetNaCl en SPARK 2014. [ 10 ] La versión SPARK de la biblioteca cuenta con 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. [ 3 ]

Véase también

Referencias

  1. ↑ "Ada2012 Rationale" (PDF) . adacore.com . Archivado (PDF) del original el 18 de abril de 2016 . Recuperado el 5 de mayo de 2018 .
  2. 1 2 Handy, Alex (24 de agosto de 2010). "La criptomoneda Skein derivada de Ada muestra SPARK" . SD Times . BZ Media LLC . Recuperado el 31 de agosto de 2010 .
  3. 1 2 3 4 5 6 7 8 9 10 Chapman, Roderick; Dross, Claire; Matthews, Stuart; Moy, Yannick (marzo de 2024). "Codesarrollo de programas y su prueba de corrección" . Communications of the ACM . 67 (3): 84– 94. doi : 10.1145/3624728 .
  4. 1 2 3 4 Ross, Philip E. (septiembre de 2005). "Los exterminadores" . IEEE Spectrum . 42 (9): 36– 41. doi : 10.1109/MSPEC.2005.1502527 . ISSN 0018-9235 . S2CID 26369398 .  
  5. ↑ "SPARK – El núcleo Ada SPADE (incluido RavenSPARK)" . AdaCore . Consultado el 30 de junio de 2021 .
  6. 1 2 3 4 5 Chapman, Roderick (diciembre de 2000). "Experiencia industrial con SPARK". ACM SIGAda Ada Letters . XX (4): 64– 68. doi : 10.1145/369264.369270 .
  7. ↑ Brandon, Carl S. (2013). "Software CubeSat de alta fiabilidad con SPARK/Ada" (PDF) . iCubeSat.org . Consultado el 20 de diciembre de 2025 .
  8. ↑ "Garantizando el futuro de la seguridad del software integrado" . 8 de enero de 2020.
  9. ↑ Zabrocki, Adam; Mitic, Marko (8 de agosto de 2025). "¿Cómo asegurar el envío de más de mil millones de núcleos de un ecosistema único?" (PDF) . Recuperado el 13 de agosto de 2025 .{{cite web}}: CS1 mantenimiento: estado de la URL ( enlace )
  10. ↑ "SPARKNaCl" . GitHub . 8 de octubre de 2021.

Lecturas adicionales

  • Barnes, John (2012). SPARK: El enfoque probado para software de alta integridad . Altran Praxis. ISBN 978-0-9572905-1-8Archivado del original el 14 de octubre de 2016. Consultado el 31 de diciembre de 2014 .
  • McCormick, John W.; Chapin, Peter C. (2015). Creación de aplicaciones de alta integridad con SPARK . Cambridge University Press. ISBN 978-1-107-65684-0.
  • Sitio web de la comunidad SPARK 2014
  • Sitio web de SPARK Pro
  • Sitio web de SPARK Libre (GPL) Edition archivado el 12 de febrero de 2005 en Wayback Machine.
  • Altrán
  • Corrección por construcción: Un manifiesto para el software de alta integridad. Archivado el 30 de octubre de 2012 en la Wayback Machine.
  • Club de Sistemas Críticos para la Seguridad del Reino Unido
  • Comparación con un lenguaje de especificación C (Frama C)
  • Página del proyecto Tokeneer
  • Lanzamiento público del kernel de Muen
  • Proyecto LifeFlow LVAD
  • Proyecto CubeSat de VTU