Hola,
No entiendo la notación de la postcondición del chmod. ¿A lo que se refiere es a que el estado s' es igual a solo que en los campos saos_exec_mode y aos_activity va a tener los valores cambiados por svc y running en un caso del or y en el otro caso del or usr y running?
Saludos,
Jairo.
Perdón, leí mal. Sí, es lo que yo dije pero no era para una pregunta. Es la relación que describe más arriba, estaba mirando la parte de notación (y ahí no estaba).
Saludos,
Jairo.
Hola.
Entiendo con esto que la duda desapareció. Sino, volvé a escribir.
Saludos, Carlos
Hola, me queda una duda con respecto a este punto.
Los valores en s' necesariamente tienen que ser svc y running o usr y running? o podrían quedar iguales?
Saludos y gracias
Yo lo interpreté así, como que en s' en un lado del or tienen que ser svc y running y en el otro usr y running.
Saludos,
Jairo.
Es correcta la observación.
No entiendo bien cuál es la duda respecto a lo que está especificado formalmente en el paper. Tener en cuenta también la condición sobre el os (si es trusted o no).
Saludos, Carlos