Impossibility of Precise and Sound Termination-Sensitive Security Enforcements - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2018

Impossibility of Precise and Sound Termination-Sensitive Security Enforcements

Minh Ngo
  • Fonction : Auteur
  • PersonId : 1029079
Tamara Rezk
  • Fonction : Auteur
  • PersonId : 949476
  • IdRef : 136831605

Résumé

An information flow policy is termination-sensitive if it imposes that the termination behavior of programs is not influenced by confidential input. Termination-sensitivity can be statically or dynamically enforced. On one hand, existing static enforcement mechanisms for termination-sensitive policies are typically quite conservative and impose strong constraints on programs like absence of while loops whose guard depends on confidential information. On the other hand, dynamic mechanisms can enforce termination-sensitive policies in a less conservative way. Secure Multi-Execution (SME) [1], one of such mechanisms, was even claimed to be sound and precise in the sense that the enforcement mechanism will not modify the observable behavior of programs that comply with the termination-sensitive policy. However, termination-sensitivity is a subtle policy, that has been formalized in different ways. A key aspect is whether the policy talks about actual termination, or observable termination. This paper proves that termination-sensitive policies that talk about actual termination are not enforceable in a sound and precise way. For static enforcements, the result follows directly from a reduction of the decidability of the problem to the halting problem. However, for dynamic mechanisms the insight is more involved and requires a diagonalization argument. In particular, our result contradicts the claim made about SME. We correct these claims by showing that SME enforces a subtly different policy that we call indirect termination-sensitive noninterference and that talks about observable termination instead of actual termination. We construct a variant of SME that is sound and precise for indirect termination-sensitive noninterference. Finally, we also show that static methods can be adapted to enforce indirect termination-sensitive information flow policies (but obviously not precisely) by constructing a sound type system for an indirect termination-sensitive policy.

Dates et versions

hal-01928669 , version 1 (20-11-2018)

Identifiants

Citer

Minh Ngo, Frank Piessens, Tamara Rezk. Impossibility of Precise and Sound Termination-Sensitive Security Enforcements. SP 2018 - IEEE Symposium on Security and Privacy, May 2018, San Francisco, United States. pp.496-513, ⟨10.1109/SP.2018.00048⟩. ⟨hal-01928669⟩
48 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More