Propiedades de seguridad y vivacidad.

Las propiedades de la ejecución de un programa de computadora, particularmente para sistemas concurrentes y distribuidos , se han formulado durante mucho tiempo dando propiedades de seguridad ("no suceden cosas malas") y propiedades de vida ("suceden cosas buenas"). ^[1]

Un ejemplo sencillo ilustrará la seguridad y la vivacidad. Un programa es totalmente correcto con respecto a una condición previa y posterior si cualquier ejecución iniciada en un estado satisfactorio termina en un estado satisfactorio . La corrección total es una conjunción de una propiedad de seguridad y una propiedad de vida: ^[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 generalmente se escribe usando la tripleta Hoare . ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle C}$ ${\displaystyle \{P\}C\{Q\}}$
• La propiedad de vida, lo "bueno", es que la ejecución que comienza en un estado satisfactorio termina. ${\displaystyle P}$

Tenga en cuenta que algo malo es discreto, ^[3] ya que ocurre en un lugar particular durante la ejecución. Una "cosa buena" no tiene por qué ser discreta, pero la propiedad de vivacidad de la terminación es discreta.

Las definiciones formales que finalmente se propusieron para las propiedades de seguridad ^[4] y las propiedades de vida ^[5] demostraron que esta descomposición no sólo 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 vida. ^[5] Además, realizar la descomposición puede ser útil, porque las definiciones formales permiten probar que se deben usar diferentes métodos para verificar las propiedades de seguridad versus para verificar las propiedades de vida. ^{[6] [7]}

Seguridad

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

Ejemplos de algo malo discreto 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 determinada termina, pero el estado final no satisface la condición posterior requerida;
• Una ejecución de dos procesos concurrentes, donde los contadores del programa para ambos procesos designan declaraciones dentro de una sección crítica ;
• Una ejecución de dos procesos concurrentes donde cada proceso está esperando a que otro cambie de estado (conocido como punto muerto ).

La ejecución de un programa se puede describir formalmente dando la secuencia infinita de estados del programa que resultan 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, denotemos 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 es válida para secuencias y iff es un prefijo de o igual . ^[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 lo malo que define esa propiedad de seguridad ocurre en algún momento . Observe que después de algo tan malo , si una ejecución adicional resulta en una ejecución , entonces tampoco satisface , ya que lo malo en también ocurre en . Consideramos que esta inferencia sobre la irremediabilidad de las cosas malas es la característica definitoria de una propiedad de seguridad. Formalizar esto en lógica de predicados da una definición formal de lo que es 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 vida prescribe cosas buenas para cada ejecución o, de manera equivalente, describe algo que debe suceder durante una ejecución. ^[1] Lo bueno no tiene por qué ser discreto: puede implicar un número infinito de pasos. Ejemplos de algo bueno utilizado para definir una propiedad de vida incluyen: ^[5]

• Terminación de una ejecución que se inició en un estado adecuado;
• No terminación de una ejecución iniciada en estado adecuado;
• Entrada eventual garantizada a una sección crítica siempre que se intente ingresar;
• Acceso justo a un recurso en presencia de discordia.

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

Producir una respuesta dentro de un límite específico de tiempo real es una propiedad de seguridad más que una propiedad de vida. Esto se debe a que se está prohibiendo algo malo : una ejecución parcial que alcanza un estado en el que aún no se ha producido la respuesta 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" dentro de una cierta cantidad de pasos o antes de una fecha límite. Una propiedad que da 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 el límite existe es una propiedad de vitalidad. Es probable que demostrar dicha propiedad de vida sea más fácil que probar la propiedad de seguridad más estricta porque demostrar la propiedad de vida no requiere el tipo de contabilidad detallada que se requiere para probar la propiedad de seguridad.

A diferencia de una propiedad de seguridad, una propiedad de vida no puede descartar ningún prefijo finito ^[8] de una ejecución (ya que tal sería "algo malo" y, por lo tanto, definiría una propiedad de seguridad). Eso lleva a definir una propiedad de vida 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 a todos , que es una ejecución de longitud infinita. ${\displaystyle \tau }$

Historia

Lamport utilizó los términos propiedad de seguridad y propiedad de vida en su artículo de 1977 ^[1] sobre la demostración de la corrección de programas multiproceso (concurrentes) . Tomó prestados los términos de la teoría de la red de Petri , que utilizaba los términos vivacidad y limitación para describir cómo podría evolucionar la asignación de las "fichas" de una red de Petri a sus "lugares"; La seguridad de la red de Petri era una forma específica de limitación . Posteriormente, Lamport desarrolló una definición formal de seguridad para un curso breve de la OTAN sobre sistemas distribuidos en Munich. ^[9] Se supone que las propiedades son invariantes en condiciones de tartamudez . 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 vida 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 del autómata Büchi para las definiciones formales de propiedades de seguridad y propiedades de vida, sino que utilizaron estas formulaciones de autómatas para mostrar que la verificación de las propiedades de seguridad requeriría una invariante y la verificación de las propiedades de vida requeriría una invariante. requieren un argumento bien fundamentado . La correspondencia entre el tipo de propiedad (seguridad versus vitalidad) con el tipo de prueba (invariancia versus fundamento) fue un fuerte argumento de que la descomposición de las propiedades en seguridad y vitalidad (a diferencia de alguna otra partición) era útil: saber el tipo de propiedad a probar dicta el tipo de prueba que se requiere. ${\displaystyle S^{\omega }}$

Referencias

1. Lamport, Leslie (marzo de 1977). "Demostrar la corrección de los programas multiproceso". Transacciones IEEE sobre ingeniería de software . SE-3 (2): 125–143. CiteSeerX  10.1.1.137.9454 . doi :10.1109/TSE.1977.229904. S2CID  9985552.
2. Maná, Zóhar; Pnueli, Amir (septiembre de 1974). "Enfoque axiomático de la corrección total de los programas". Acta Informática . 3 (3): 243–263. doi :10.1007/BF00288637. S2CID  2988073.
3. es decir, tiene una 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 conferencias 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 vivacidad". Cartas de procesamiento de información . 21 (4): 181–185. doi :10.1016/0020-0190(85)90056-0.
6. Alpern, Bowen; Schneider, Fred B. (1987). "Reconociendo la seguridad y la vivacidad". Computación distribuída . 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 cuya importancia e impacto en la teoría y/o práctica de la computación distribuida han sido evidentes durante al menos una década"), por la presentación formal La descomposición en propiedades de seguridad y vida fue crucial para futuras investigaciones sobre las propiedades de prueba 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 conferencias 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 tartamudear". Cartas de procesamiento de 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). "Reconociendo la seguridad y la vivacidad". Computación distribuída . 2 (3): 117–126. doi :10.1007/BF01782772. hdl : 1813/6567 . S2CID  9717112.