Propiedades de seguridad y vitalidad

Las propiedades de la ejecución de un programa informático (en particular para sistemas concurrentes y distribuidos ) se han formulado desde hace mucho tiempo proporcionando propiedades de seguridad ("no suceden cosas malas") y propiedades de vitalidad ("sí suceden cosas buenas"). ^[1]

Un programa es totalmente correcto con respecto a una condición previa y una condición posterior si cualquier ejecución iniciada en un estado que satisface termina en un estado que satisface . La corrección total es una conjunción de una propiedad de seguridad y una propiedad de vitalidad: ^[2] ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle P}$ ${\displaystyle Q}$

• La propiedad de seguridad prohíbe estas "cosas malas": ejecuciones que comienzan en un estado satisfactorio y terminan en un estado final que no satisface . Para un programa , esta propiedad de seguridad se escribe generalmente utilizando la tripleta de Hoare . ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle C}$ ${\displaystyle \{P\}C\{Q\}}$
• La propiedad de vitalidad, lo "bueno", es que la ejecución que comienza en un estado que satisface termina. ${\displaystyle P}$

Tenga en cuenta que una cosa mala es discreta, ^[3] ya que sucede en un lugar particular durante la ejecución. Una "cosa buena" no necesita ser discreta, pero la propiedad de vitalidad de la terminación es discreta.

Las definiciones formales que se propusieron finalmente para las propiedades de seguridad ^[4] y las propiedades de vitalidad ^[5] demostraron que esta descomposición no solo es intuitivamente atractiva sino que también es completa: todas las propiedades de una ejecución son una conjunción de propiedades de seguridad y vitalidad. ^[5] Además, realizar la descomposición puede ser útil, porque las definiciones formales permiten una prueba de que se deben utilizar métodos diferentes para verificar las propiedades de seguridad frente a las propiedades de vitalidad. ^{[6] [7]}

Seguridad

Una propiedad de seguridad prohíbe que ocurran cosas malas discretas durante una ejecución. ^[1] Por lo tanto, una propiedad de seguridad caracteriza lo que está permitido al indicar lo que está prohibido. El requisito de que la cosa mala sea discreta significa que una cosa mala que ocurra durante la ejecución necesariamente ocurre en algún punto identificable. ^[5]

Algunos ejemplos de una cosa mala discreta que podría usarse para definir una propiedad de seguridad incluyen: ^[5]

• Una ejecución que comienza en un estado que satisface una condición previa dada termina, pero el estado final no satisface la condición posterior requerida;
• Una ejecución de dos procesos concurrentes, donde los contadores de programa para ambos procesos designan declaraciones dentro de una sección crítica ;
• Una ejecución de dos procesos simultáneos donde cada proceso está esperando que otro cambie de estado (conocido como bloqueo ).

La ejecución de un programa se puede describir formalmente dando la secuencia infinita de estados del programa que resulta a medida que avanza la ejecución, donde el último estado de un programa que termina se repite infinitamente. Para un programa de interés, sea el conjunto de posibles estados del programa, el conjunto de secuencias finitas de estados del programa y el conjunto de secuencias infinitas de estados del programa. La relación se cumple para secuencias y si y solo si es un prefijo de o es igual a . ^[5] ${\displaystyle S}$ ${\displaystyle S^{*}}$ ${\displaystyle S^{\omega }}$ ${\displaystyle \sigma \leq \tau }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$

Una propiedad de un programa es el conjunto de ejecuciones permitidas.

La característica esencial de una propiedad de seguridad es: si alguna ejecución no satisface entonces la cosa mala que define a esa propiedad de seguridad ocurre en algún punto en . Nótese que después de tal cosa mala , si una ejecución posterior da como resultado una ejecución , entonces tampoco satisface , ya que la cosa mala en también ocurre en . Tomamos esta inferencia sobre la irremediabilidad de las cosas malas como la característica definitoria de ser una propiedad de seguridad. Formalizar esto en lógica de predicados da una definición formal de ser una propiedad de seguridad. ^[5] ${\displaystyle SP}$ ${\displaystyle \sigma }$ ${\displaystyle SP}$ ${\displaystyle \sigma }$ ${\displaystyle \sigma ^{\prime }}$ ${\displaystyle \sigma ^{\prime }}$ ${\displaystyle SP}$ ${\displaystyle \sigma }$ ${\displaystyle \sigma ^{\prime }}$ ${\displaystyle SP}$ ${\displaystyle SP}$

${\displaystyle \forall \sigma \in S^{\omega }:\sigma \notin SP\implies (\exists \beta \leq \sigma :(\forall \tau \in S^{\omega }:\beta \tau \notin SP))}$

Esta definición formal de propiedades de seguridad implica que si una ejecución satisface una propiedad de seguridad, entonces cada prefijo de (con el último estado repetido) también satisface . ${\displaystyle \sigma }$ ${\displaystyle SP}$ ${\displaystyle \sigma }$ ${\displaystyle SP}$

Vivacidad

Una propiedad de vivacidad prescribe cosas buenas para cada ejecución o, equivalentemente, describe algo que debe suceder durante una ejecución. ^[1] La cosa buena no necesita ser discreta, puede implicar una cantidad infinita de pasos. Algunos ejemplos de una cosa buena utilizada para definir una propiedad de vivacidad incluyen: ^[5]

• Terminación de una ejecución iniciada en un estado adecuado;
• No terminación de una ejecución iniciada en un estado adecuado;
• Se garantiza el ingreso eventual a una sección crítica cuando se intenta ingresar;
• Acceso justo a un recurso en presencia de contención.

Lo bueno en el primer ejemplo es discreto pero en los demás no.

La producción de una respuesta dentro de un límite de tiempo real especificado es una propiedad de seguridad más que de actividad. Esto se debe a que se está prohibiendo algo discreto y malo : una ejecución parcial que alcanza un estado en el que la respuesta aún no se ha producido y el valor del reloj (una variable de estado) viola el límite. La libertad de interbloqueo es una propiedad de seguridad: lo "malo" es un interbloqueo (que es discreto).

La mayoría de las veces, saber que un programa finalmente hace algo "bueno" no es satisfactorio; queremos saber que el programa realiza lo "bueno" en un cierto número de pasos o antes de una fecha límite. Una propiedad que otorga un límite específico a lo "bueno" es una propiedad de seguridad (como se señaló anteriormente), mientras que la propiedad más débil que simplemente afirma que existe el límite es una propiedad de vitalidad. Es probable que probar una propiedad de vitalidad de este tipo sea más fácil que probar la propiedad de seguridad más estricta porque probar la propiedad de vitalidad no requiere el tipo de contabilidad detallada que se requiere para probar la propiedad de seguridad.

Para diferenciarse de una propiedad de seguridad, una propiedad de vitalidad no puede descartar ningún prefijo finito ^[8] de una ejecución (ya que tal cosa sería algo "malo" y, por lo tanto, definiría una propiedad de seguridad). Esto lleva a definir una propiedad de vitalidad como una propiedad que no descarta ningún prefijo finito. ^[5] ${\displaystyle LP}$ ${\displaystyle \alpha \in S^{*}}$ ${\displaystyle \alpha }$ ${\displaystyle LP}$

${\displaystyle \forall \alpha \in S^{*}:(\exists \tau \in S^{\omega }:\alpha \tau \in LP)}$

Esta definición no restringe que algo bueno sea discreto: lo bueno puede involucrar todo , que es una ejecución de longitud infinita. ${\displaystyle \tau }$

Historia

Lamport utilizó los términos propiedad de seguridad y propiedad de vitalidad en su artículo de 1977 ^[1] sobre la prueba de la corrección de programas multiproceso (concurrentes) . Tomó prestados los términos de la teoría de redes de Petri , que utilizaba los términos vitalidad y acotación para describir cómo podía evolucionar la asignación de los "tokens" de una red de Petri a sus "lugares"; la seguridad de la red de Petri era una forma específica de acotación . Posteriormente, Lamport desarrolló una definición formal de seguridad para un curso breve de la OTAN sobre sistemas distribuidos en Múnich. ^[9] Supuso que las propiedades son invariantes bajo tartamudeo . La definición formal de seguridad dada anteriormente aparece en un artículo de Alpern y Schneider; ^[5] la conexión entre las dos formalizaciones de las propiedades de seguridad aparece en un artículo de Alpern, Demers y Schneider. ^[10]

Alpern y Schneider ^[5] dan la definición formal de vivacidad, acompañada de una prueba de que todas las propiedades pueden construirse utilizando propiedades de seguridad y propiedades de vivacidad. Esa prueba se inspiró en la idea de Gordon Plotkin de que las propiedades de seguridad corresponden a conjuntos cerrados y las propiedades de vivacidad corresponden a conjuntos densos en una topología natural en el conjunto de secuencias infinitas de estados de programa. ^[11] Posteriormente, Alpern y Schneider ^[12] no solo dieron una caracterización de autómata Büchi para las definiciones formales de propiedades de seguridad y propiedades de vivacidad, sino que utilizaron estas formulaciones de autómatas para mostrar que la verificación de propiedades de seguridad requeriría un invariante y la verificación de propiedades de vivacidad requeriría un argumento de fundamento . La correspondencia entre el tipo de propiedad (seguridad vs. vivacidad) con el tipo de prueba (invariancia vs. fundamento) fue un argumento sólido de que la descomposición de propiedades en seguridad y vivacidad (a diferencia de alguna otra partición) era útil: conocer el tipo de propiedad a probar dictaba el tipo de prueba que se requiere. ${\displaystyle S^{\omega }}$

Referencias

1. Lamport, Leslie (marzo de 1977). "Demostración de la corrección de programas multiproceso". IEEE Transactions on Software Engineering . SE-3 (2): 125–143. CiteSeerX  10.1.1.137.9454 . doi :10.1109/TSE.1977.229904. S2CID  9985552.
2. Manna, Zohar; Pnueli, Amir (septiembre de 1974). "Enfoque axiomático para la corrección total de los programas". Acta Informatica . 3 (3): 243–263. doi :10.1007/BF00288637. S2CID  2988073.
3. es decir, tiene duración finita
4. Alford, Mack W.; Lamport, Leslie ; Mullery, Geoff P. (3 de abril de 1984). "Conceptos básicos". Sistemas distribuidos: métodos y herramientas para la especificación, un curso avanzado . Apuntes de clase sobre informática. Vol. 190. Múnich, Alemania: Springer Verlag . págs. 7–43. ISBN. 3-540-15216-4.
5. Alpern, Bowen; Schneider, Fred B. (1985). "Definición de vitalidad". Cartas de procesamiento de la información . 21 (4): 181–185. doi :10.1016/0020-0190(85)90056-0.
6. Alpern, Bowen; Schneider, Fred B. (1987). "Reconocimiento de la seguridad y la vitalidad". Computación distribuida . 2 (3): 117–126. doi :10.1007/BF01782772. hdl : 1813/6567 . S2CID  9717112.
7. El artículo ^[5] recibió el Premio Dijkstra 2018 ("por artículos destacados sobre los principios de la computación distribuida cuyo significado e impacto en la teoría y/o práctica de la computación distribuida han sido evidentes durante al menos una década"), porque la descomposición formal en propiedades de seguridad y vitalidad fue crucial para futuras investigaciones para probar las propiedades de los programas.
8. denota el conjunto de secuencias finitas de estados del programa y el conjunto de secuencias infinitas de estados del programa. ${\displaystyle S^{*}}$ ${\displaystyle S^{\omega }}$
9. Alford, Mack W.; Lamport, Leslie ; Mullery, Geoff P. (3 de abril de 1984). "Conceptos básicos". Sistemas distribuidos: métodos y herramientas para la especificación, un curso avanzado . Apuntes de clase sobre informática. Vol. 190. Múnich, Alemania: Springer Verlag . págs. 7–43. ISBN. 3-540-15216-4.
10. Alpern, Bowen; Demers, Alan J.; Schneider, Fred B. (noviembre de 1986). "Seguridad sin tartamudeo". Cartas de procesamiento de la información . 23 (4): 177–180. doi :10.1016/0020-0190(86)90132-8. hdl : 1813/6548 .
11. Comunicación privada de Plotkin a Schneider.
12. Alpern, Bowen; Schneider, Fred B. (1987). "Reconocimiento de la seguridad y la vitalidad". Computación distribuida . 2 (3): 117–126. doi :10.1007/BF01782772. hdl : 1813/6567 . S2CID  9717112.