Hiperpropiedad

En informática , las hiperpropiedades son un formalismo para describir las propiedades de los sistemas computacionales. Las hiperpropiedades generalizan las propiedades de seguridad y vitalidad , y pueden expresar propiedades como la no interferencia y el determinismo observacional. ^[1]

Desarrollando el ejemplo de no interferencia: la no interferencia no puede representarse como una "propiedad" en el sentido formal porque no hay una prueba de inclusión que pueda aplicarse a un solo rastro de programa; la no interferencia es una afirmación sobre cómo los rastros vecinos son similares entre sí y no sirve de nada observar un rastro a la vez. Las "hiperpropiedades" son la extensión de las propiedades como predicados sobre los rastros a las propiedades como relaciones entre rastros.

Definiciones

Rastros y sistemas

Las hiperpropiedades se definen en términos de trazas de un sistema computacional. Una traza es una secuencia de estados; un sistema es un conjunto de trazas. Intuitivamente, un programa corresponde al conjunto de todas sus posibles trazas de ejecución, dadas las entradas. Formalmente, el conjunto de trazas sobre un conjunto de estados es . ${\estilo de visualización \Sigma}$ $\Phi \triángulo \Sigma ^{\omega }$

Esta representación es lo suficientemente expresiva para abarcar varios modelos computacionales, incluidos los sistemas de transición etiquetados ^[2] y las máquinas de estados . ^[3]

Hiperpropiedades

Una propiedad de traza es un conjunto de trazas. Las propiedades de seguridad y vitalidad son propiedades de traza. Formalmente, una propiedad de traza es un elemento de , donde es el operador de conjunto potencia . Una hiperpropiedad es un conjunto de propiedades de traza, es decir, un elemento de . $\mathbb {P} (\Phi)$ $\mathbb {P}$ $\mathbb {P} (\mathbb {P} (\Phi ))$

Las propiedades de traza pueden dividirse en propiedades de seguridad (intuitivamente, propiedades que garantizan que "no sucedan cosas malas") y propiedades de vitalidad ("suceden cosas buenas"), y cada propiedad de traza es la intersección de una propiedad de seguridad y una propiedad de vitalidad. ^[4] Análogamente, las hiperpropiedades pueden dividirse en hiperpropiedades de hiperseguridad e hiperpropiedades de hipervivencia , y cada hiperpropiedad es una intersección de una hiperpropiedad de seguridad y una hiperpropiedad de vitalidad. ^[5]

${\estilo de visualización k}$ -Las propiedades de seguridad son hiperpropiedades de seguridad tales que cada violación de la propiedad puede ser presenciada por un conjunto de rastros como máximo. ^[6] ${\estilo de visualización k}$

Ejemplos

Toda propiedad de seguridad puede elevarse a una hiperpropiedad de 1-seguridad que exprese la misma condición. ^[7]
${\estilo de visualización k}$ -Hiperpropiedades de seguridad:
- ${\estilo de visualización k=1}$ (ascensores de propiedades de seguridad):
  - falso , definido como el conjunto que contiene el conjunto vacío . Formalmente, . Esta hiperpropiedad no la satisface ningún sistema. ^[8] $\mathbf {falso} \triangleq \{\conjunto vacío \}$
  - true , definido como el conjunto de todas las trazas. Formalmente, . Esta hiperpropiedad la satisfacen todos los sistemas. ^[9] $\mathbf {verdadero} \triangleq \Phi$
  - Control de acceso ^[10]
- ${\estilo de visualización k=2}$ :
  - Monotonía ^[11]
  - Inyectividad ^[11]
  - Simetría , antisimetría y asimetría ^[11]
  - Determinismo observacional ^[12]
  - No interferencia
- $k=3$
  - Transitividad ^[11]
- ${\estilo de visualización k=4}$
  - Asociatividad ^[11]

Propiedades

Dado que las hiperpropiedades son exactamente los elementos del conjunto potencia , están cerradas bajo intersección y unión . $\mathbb {P} (\mathbb {P} (\Phi ))$

La topología de Vietoris inferior de una topología estándar sobre propiedades de traza produce una topología sobre el conjunto de hiperpropiedades. ^[13]

Aplicaciones

Se han desarrollado varias lógicas de programa ^[14]^[11]^{[15] para comprobar que un programa se ajusta a una hiperpropiedad.}

Se han desarrollado HyperLTL ^[14] y algunos algoritmos de verificación de modelos ^[16]^{[17] para comprobar que un sistema de estados finitos se ajusta a una hiperpropiedad.}

Referencias

Notas

^ Clarkson y Schneider 2010, pág. 1.
^ Clarkson & Schneider 2010, p. 23: "Un sistema de transición etiquetado [...] puede codificarse como un conjunto de trazas".
^ Clarkson & Schneider 2010, p. 25: "Una máquina de estados M [...] puede codificarse como un conjunto de trazas".
^ Alpern, Bowen; Schneider, Fred B. (7 de octubre de 1985). "Definición de vitalidad". Information Processing Letters . 21 (4): 181–185. doi :10.1016/0020-0190(85)90056-0. ISSN 0020-0190.
^ Clarkson y Schneider 2010, pág. 21.
^ Finkbeiner, Bernd; Haas, Lennart; Torfah, Hazem (junio de 2019). "Representaciones canónicas de hiperpropiedades de k-Safety". 2019 IEEE 32nd Computer Security Foundations Symposium (CSF) . págs. 17–1714. doi :10.1109/CSF.2019.00009. ISBN 978-1-7281-1407-1. Número de identificación S2C: 201848133.
^ Clarkson & Schneider 2010, p. 11: "Las propiedades de seguridad se elevan a hiperpropiedades de seguridad".
^ Clarkson & Schneider 2010, p. 15: "La hiperpropiedad falsa, definida como \{\emptyset\}, es hiperseguridad pero no hipervivacidad".
^ Clarkson y Schneider 2010, pág. 44.
^ Clarkson y Schneider 2010.
^ abcdef Sousa y Dillig 2016.
^ Clarkson & Schneider 2010, p. 13: "el determinismo observacional OD (2.6) no puede expresarse como una propiedad de 2-seguridad, pero es una hiperpropiedad de 2-seguridad".
^ Clarkson y Schneider 2010, pág. 19.
^ ab D'Osualdo; Farzan; Dreyer (2022). "Probar la hiperseguridad compositivamente". Actas de la ACM sobre lenguajes de programación . 6 (OOPSLA2): 289–314. arXiv : 2209.07448 . doi :10.1145/3563298. S2CID 252284134.
^ Dardinier, Thibault; Müller, Peter (24 de enero de 2023). "Lógica hiperhoare: (des)prueba de hiperpropiedades de programas (versión extendida)". arXiv : 2301.10037 [cs.LO].
^ Finkbeiner, Bernd; Rabe, Markus N.; Sánchez, César (2015). "Algoritmos para la comprobación de modelos HyperLTL y HyperCTL $$^*$$". En Kroening, Daniel; Păsăreanu, Corina S. (eds.). Verificación asistida por ordenador . Apuntes de clase en informática. Vol. 9206. Cham: Springer International Publishing. págs. 30–48. doi : 10.1007/978-3-319-21690-4_3 . ISBN 978-3-319-21690-4.
^ Hsu, Tzu-Han; Sánchez, César; Bonakdarpour, Borzoo (2021). "Bounded Model Checking for Hyperproperties". En Groote, Jan Friso; Larsen, Kim Guldstrand (eds.). Herramientas y algoritmos para la construcción y análisis de sistemas . Apuntes de clase en informática. Vol. 12651. Cham: Springer International Publishing. págs. 94–112. doi :10.1007/978-3-030-72016-2_6. ISBN 978-3-030-72016-2. Número de pieza 7979203 .

Fuentes

Clarkson, Michael R.; Schneider, Fred B. (20 de septiembre de 2010). Sabelfeld, Andrei (ed.). "Hiperpropiedades". Revista de seguridad informática . 18 (6): 1157–1210. doi :10.3233/JCS-2009-0393. S2CID 218604768.
Sousa, Marcelo; Dillig, Isil (2 de junio de 2016). "Lógica cartesiana de hoare para verificar propiedades de k-seguridad". Actas de la 37.ª Conferencia ACM SIGPLAN sobre diseño e implementación de lenguajes de programación . PLDI '16. Nueva York, NY, EE. UU.: Association for Computing Machinery. págs. 57–69. doi :10.1145/2908080.2908092. ISBN . 978-1-4503-4261-2. Número de identificación del sujeto 17433405.