¿Cómo garantiza la verificación formal un código seguro y sin errores?

No garantiza que el código esté libre de vulnerabilidad. Sin embargo, si la verificación se utiliza adecuadamente, puede aumentar la seguridad (confianza) de que la aplicación es segura.

Hablando desde una perspectiva muy amplia, hay dos aspectos de este problema:

• Verificación. Dado un modelo matemático del sistema y una especificación matemática de los requisitos, ¿el sistema cumple con las especificaciones?

• Validación. ¿Tenemos el conjunto de requisitos correcto ? ¿La especificación matemática refleja con precisión los verdaderos requisitos? ¿El modelo matemático corresponde de manera precisa y completa al código?

A veces las personas se centran solo en la verificación, pero ambas cosas importan.

En su situación, si la especificación incorpora todos los requisitos de seguridad relevantes, y si el modelo matemático corresponde correctamente al código, y si La verificación se realiza correctamente y tiene éxito, entonces podemos tener una base para una seguridad significativamente mayor de que el sistema cumplirá con nuestros requisitos de seguridad.

En el mejor de los casos, la verificación puede ser una herramienta poderosa para ayudar a garantizar la seguridad, una de las más poderosas que tenemos. Sin embargo, como con cualquier cosa, es posible hacer un mal uso de la tecnología u obtener una falsa sensación de seguridad si no se usa adecuadamente. Uno de los modos de falla más comunes es que el proceso de verificación no verifica todos los requisitos de seguridad relevantes (algunos se pasan por alto u omiten).

Decir mucho más podría requerir profundizar en los detalles del sistema, los requisitos de seguridad y la naturaleza de la verificación que se realizó, pero espero que esto le brinde una visión general.

La verificación formal no garantiza un sistema seguro. Nada garantiza un sistema seguro. Lo que puede hacer la verificación formal es proporcionar una seguridad muy alta de que algunas partes del sistema son seguras.

La verificación formal proporciona una prueba matemática de que, bajo ciertas suposiciones, un modelo del sistema tiene ciertas propiedades. Por lo tanto, si parte del sistema se ha verificado formalmente, aún quedan varias condiciones para que el sistema sea seguro:

• ¿Se cumplen los supuestos subyacentes a la verificación?
• ¿El sistema coincide con el modelo que se ha verificado?
• ¿Es correcta la prueba proporcionada por el sistema de verificación?
• ¿Son las propiedades probadas suficientes para garantizar la seguridad del sistema?

El alcance de la verificación formal puede variar mucho. Por ejemplo, desbordamientos de búfer , un tipo común de vulnerabilidad, puede detectarse con bastante facilidad: la mayoría de los idiomas son más altos que C o C ++ garantizan la ausencia de desbordamientos de búfer en el programa compilado. No obstante, puede suceder que el compilador permita que pase un código dañado, aunque los errores del compilador son mucho más raros que los errores de programa, no son imposibles. Sin embargo, los desbordamientos de búfer son de un solo tipo; La seguridad de la mayoría de los sistemas depende de mucho más que saber que no hay desbordamientos de búfer. (Lectura relacionada: ¿Por qué las computadoras no comprueban si hay contenido de memoria en algún espacio de memoria? )

Para ilustrar las limitaciones anteriores, permítame tomar un ejemplo concreto. Algunas tarjetas inteligentes ejecutan una Java Tarjeta de la máquina virtual, y ejecute solo el bytecode que ha sido verificado . El verificador de bytecode, en principio, garantiza que el código no puede mirar o sobresalir fuera de su espacio de memoria asignado. Esto evita algunas vulnerabilidades pero no todas:

• La verificación solo garantiza sus propiedades si el intérprete de bytecode se comporta de acuerdo con su especificación. Además, si el hardware no ejecuta el intérprete correctamente, todas las apuestas están desactivadas (por ejemplo, una forma de atacar a una tarjeta inteligente es causar una falla de energía que hace que se omitan algunas instrucciones).
• Si hay un error que permite cargar el código sin pasar por el verificador, es posible que el código de la tarjeta no tenga las propiedades garantizadas por la verificación.
• El propio verificador puede tener errores y permitir que se cargue un código incorrecto.
• Incluso si el código de las aplicaciones en la tarjeta no accede directamente a la memoria de otras aplicaciones, aún puede espiarlas o perturbarlas de otras maneras. Por ejemplo, puede explotar un canal lateral como el tiempo para deducir las propiedades de otro código que se ejecuta en el mismo dispositivo.
  Además, la seguridad del sistema puede depender de otras cosas además del aislamiento entre las aplicaciones en la tarjeta. Por ejemplo, el sistema de autenticación puede permitir que un atacante tome el control de la tarjeta, puede haber una vulnerabilidad a nivel de protocolo que le permita interrumpir las comunicaciones, etc.

En un sistema de alta seguridad, la verificación formal puede ayudar de dos maneras:

• Comprobando que el código coincide con su especificación. Esto requiere un modelo formal del entorno de ejecución (hardware, compilador o intérprete, biblioteca estándar, ...) y mucho trabajo.
• Probando que la especificación tiene ciertas propiedades deseables. Esto requiere una formalización de la especificación, una elección juiciosa de propiedades y mucho trabajo.

Los Criterios comunes para las evaluaciones de seguridad definen varios niveles de seguridad . Solo el nivel de seguridad más alto (EAL7) requiere una verificación formal. Este no es el único requisito: la verificación formal no excluye la evaluación de otros aspectos del sistema, incluida la documentación, las pruebas de penetración, etc.

La verificación formal realmente solo funciona en casos extremadamente restringidos en los que un sistema puede modelarse como una serie de transformaciones con dominios, rangos y reglas claramente definidas que definen el comportamiento de una función. En muchos casos, esto significa que usted ' al tratar con un sistema que es la realización de software de un modelo matemático, o que (relativamente :-)) es fácil derivar un modelo del comportamiento de los sistemas (circuitos digitales de una complejidad significativamente menor que una CPU de propósito general)

Trabajé en algunos de los precursores de esto en los años 80, donde el esfuerzo consistía en generar 'código comprobable'. Un sistema que recuerdo se llamó Adele y operó en programas escritos en (uggh) Ada. Como anécdota, solíamos bromear con el hecho de que usar Adele significaba que se demoraba 10 veces más en escribir, corría 10 veces más lentamente y solo se colapsaba un 10% más. Tal vez quiera mirar los escritos de Bertrand Meyer en Eiffel, dijo pensamiento significativo y esfuerzo en cómo un lenguaje podría proporcionar verificaciones de verificación internas a través de condiciones previas, condiciones posteriores, invariantes y un montón de otras cosas que ya he olvidado ...

Verificación comprueba si el sistema tiene una propiedad específica. Las propiedades pueden expresarse en varias notaciones y lógicas. Especificar estas propiedades es difícil. Entonces, si un diseñador puede expresar su idea de seguridad en una notación formal adecuada para la verificación, y se ha comprobado que el software satisface la propiedad, entonces sí, es seguro. En la vida real, es casi un objetivo imposible verificar propiedades no triviales en software real que se ejecuta en hardware de propósito general

Cualquier vulnerabilidad es un término demasiado amplio, ya que la verificación formal (en efecto, la prueba automatizada de que un algoritmo / sistema posee propiedades específicas) está orientada hacia amenazas específicas: se filtran datos confidenciales, se filtra información externa a través de las defensas, fugas de memoria, errores de asignación, desbordamientos de pila, etc. Para obtener una vista previa del trabajo actual a este respecto, por ejemplo, puede Visite Instituto de Ingeniería de Software en Carnegie-Mellon Uni.

La verificación formal solo verifica la conformidad de la codificación con las especificaciones dadas. Si una especificación en sí misma es incorrecta / incorrecta, entonces una verificación eventual evidentemente carece de valor. Para obtener información sobre la verificación formal, ver, por ejemplo, enlace y enlace

Cualquier modelo no puede garantizar un código seguro y sin errores. Sólo las pruebas continuas pueden darle seguridad temporal. Terminar un código no significa que seguirá siendo seguro, por lo que se requieren más pruebas continuas contra nuevas vulnerabilidades.