Output-sensitive Information flow analysis - Formal Techniques for Distributed Objects, Components, and Systems Access content directly
Conference Papers Year : 2019

Output-sensitive Information flow analysis

Cristian Ene
  • Function : Author
  • PersonId : 862104
Laurent Mounier
  • Function : Author
Marie-Laure Potet
  • Function : Author

Abstract

Constant-time programming is a countermeasure to prevent cache based attacks where programs should not perform memory accesses that depend on secrets. In some cases this policy can be safely relaxed if one can prove that the program does not leak more information than the public outputs of the computation. We propose a novel approach for verifying constant-time programming based on a new information flow property, called output-sensitive non-interference. Noninterference states that a public observer cannot learn anything about the private data. Since real systems need to intentionally declassify some information, this property is too strong in practice. In order to take into account public outputs we proceed as follows: instead of using complex explicit declassification policies, we partition variables in three sets: input, output and leakage variables. Then, we propose a typing system to statically check that leakage variables do not leak more information about the secret inputs than the public normal output. The novelty of our approach is that we track the dependence of leakage variables with respect not only to the initial values of input variables (as in classical approaches for noninterference), but taking also into account the final values of output variables. We adapted this approach to LLVM IR and we developed a prototype to verify LLVM implementations.
Fichier principal
Vignette du fichier
forte19.pdf (459.27 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02303984 , version 1 (02-10-2019)

Licence

Attribution

Identifiers

Cite

Cristian Ene, Laurent Mounier, Marie-Laure Potet. Output-sensitive Information flow analysis. 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2019, Copenhagen, Denmark. pp.93-110, ⟨10.1007/978-3-030-21759-4_6⟩. ⟨hal-02303984⟩
99 View
90 Download

Altmetric

Share

Gmail Facebook X LinkedIn More