TL; DR: la verificación formal rara vez toca estados “extraños” del sistema que se está modelando. La verificación formal es útil para el software, pero inútil para el hardware.
Los ataques de inyección de falla y los ataques de canal lateral no son lo mismo. El único principio común para ambas clases es que los ataques de alguna manera abusan de un estado “extraño” del sistema, que el atacante puede observar o inducir, pero que los desarrolladores del sistema no han tenido en cuenta de antemano (y que, por lo tanto, no está modelado por ellos tampoco).
- Para el canal lateral, este estado extraño es una combinación de uno de todos los estados válidos / previstos del sistema (que puede no ser observado directamente por el atacante) y el ruido / fuga inducida por ellos hacia el medio fuera del sistema, que es observado por el atacante.
- Para la inyección de fallas: es un estado completamente nuevo del sistema (instrucciones no válidas, bits invertidos en los registros, lo que sea), que es inducido por el atacante (tal vez inyectando energía en el mismo medio que utiliza el ataque del canal lateral: por ejemplo, podemos use el campo EM del chip en ejecución tanto para filtrar datos como para inyectar fallas).
Para defenderse de los ataques de canal lateral, los diseñadores del sistema deben saber cómo se filtra el estado del hardware durante las operaciones críticas y se forma un nuevo estado que puede ser observado por el atacante y revela cierta información sobre el estado original que no podría ser observado directamente Por ejemplo, el hecho de que el consumo de energía de cualquier puerta lógica se correlacione con los valores de las señales en sus entradas / salidas significa que el consumo de energía de todo el chip en el mundo real se correlaciona con el peso de Hamming de los valores en los registros y / o el Distancia de Hamming entre los valores actuales en los registros y los valores después de la ejecución de la siguiente instrucción, lo que sea. Una vez que los diseñadores del sistema son conscientes de este hecho, pueden, en primer lugar, implementar contramedidas en el hardware que reducen la relación señal / ruido en todos los canales laterales que conocen. De esta manera, los estados observables por el atacante del sistema son indistinguibles o hay demasiados de ellos para ser analizados de manera efectiva.
- Cómo configurar una computadora que básicamente se ejecuta fuera de una carpeta de red
- Teoría de gráficos: ¿Cuáles son algunas aplicaciones de la vida real en las que es necesario resolver el problema de corte máximo?
- ¿Cuál es la reputación de MS (CS) con la especialización de Cloud Computing de Texas Tech, Universidad de Lubbock en el mercado laboral de EE. UU. Ahora? ¿Qué área de investigación en computación en la nube tiene una gran demanda desde una perspectiva laboral en el mercado estadounidense de hoy?
- ¿Qué es un árbol B +?
- ¿Cómo se usan los BITS de computadora para representar las letras del alfabeto?
Para defenderse contra la inyección de fallas, los diseñadores del sistema primero deben hacer que el hardware del mundo real sea mucho más resistente a cualquier influencia que provoque fallas, y luego mejorar la detección de estados de falla “extraños” en todo el sistema, tanto en hardware como en software, e incluir estos estados “extraños” en su modelo de sus sistemas. La electrónica de grado espacial ha lidiado con eso durante décadas: al menos duplicando cada circuito crítico y tomando medidas explícitamente cuando uno de los duplicados produce una salida diferente. De esta manera, la mayoría de los estados del sistema inducidos por los atacantes ahora son contabilizados y predichos por los diseñadores del sistema, y ya no son realmente “extraños”. El sistema se da cuenta de ellos y se comporta de manera predecible.
Ahora llegando al punto principal: sistemas seguros formalmente verificados. El problema con ellos frente a los ataques de canal lateral y los ataques de inyección de fallas es que los estados “extraños” son muy difíciles de modelar, ya que el espacio físico real en el que existen es más grande que el espacio del modelo original. Incluso si tenemos la garantía perfecta de que el software y el hardware satisfacen nuestras restricciones de seguridad en cualquier momento, una partícula cargada que golpea el silicio del chip que ejecuta nuestro sistema puede romper cualquiera de nuestras suposiciones.
Digamos, una máquina de Turing en teoría existe en un espacio muy simple con pocas leyes (¡e incluso entonces el problema de detención de la máquina de Turing no puede resolverse para un programa arbitrario!), Mientras que su impedancia en el mundo real existe inmediatamente en un entorno físico real. espacio, donde:
- Consumirá energía para realizar cálculos y afectará la materia;
- Todos sus estados, incluso los que son esencialmente equivalentes en teoría, serán distinguibles debido a las fluctuaciones del medio físico que los codifica en el mundo real;
- El medio que codifica sus estados y el medio que implementa su lógica pueden verse influenciados por procesos del mundo real completamente fuera del alcance del modelo (un atacante puede, por ejemplo, “atar un nudo” en la “cinta” de la máquina de Turing, forzándolo a Un bucle infinito).
Para resolver este problema por completo, un sistema informático en su conjunto debe ser plenamente consciente del universo en el que se está ejecutando y ser consciente de su propio estado en el universo que lo rodea. Realmente dudo que este problema tenga una solución factible. Incluso un ser humano que tenga todo el poder de nuestra civilización hasta el momento probablemente no pueda protegerse de los ataques biológicos de los canales laterales y los ataques de inyección de fallas biológicas.
Finalmente, trataré de responder la pregunta original: es extremadamente difícil, si no prácticamente imposible, verificar formalmente un sistema informático completo (hardware + software) que incluya cualquier tipo de funcionalidad “rica” y “utilizable”.
Tenemos algunos sistemas operativos verificados formalmente que solo se pueden usar en entornos restringidos (y en la práctica, estos sistemas operativos realizan tareas de procesamiento muy limitadas), y tenemos algunos equipos como tarjetas inteligentes con componentes verificados formalmente en un alto nivel (RTL), pero La verdadera verificación formal del hardware no está resuelta incluso en teoría, ya que la física no tiene un modelo final del universo en el que el hardware existe inevitablemente.
