Output-sensitive Information flow analysis
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 compu...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-02-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5779/pdf |
| _version_ | 1797268592492806144 |
|---|---|
| author | Cristian Ene Laurent Mounier Marie-Laure Potet |
| author_facet | Cristian Ene Laurent Mounier Marie-Laure Potet |
| author_sort | Cristian Ene |
| collection | DOAJ |
| description | 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 noninterference.
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. |
| first_indexed | 2024-04-25T01:34:56Z |
| format | Article |
| id | doaj.art-d8bc2e39d78640979b9416c6cbfb4170 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:56Z |
| publishDate | 2021-02-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-d8bc2e39d78640979b9416c6cbfb41702024-03-08T10:33:16ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-02-01Volume 17, Issue 110.23638/LMCS-17(1:15)20215779Output-sensitive Information flow analysisCristian Enehttps://orcid.org/0000-0002-1357-9504Laurent MounierMarie-Laure PotetConstant-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 noninterference. 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.https://lmcs.episciences.org/5779/pdfcomputer science - cryptography and securitycomputer science - programming languages |
| spellingShingle | Cristian Ene Laurent Mounier Marie-Laure Potet Output-sensitive Information flow analysis Logical Methods in Computer Science computer science - cryptography and security computer science - programming languages |
| title | Output-sensitive Information flow analysis |
| title_full | Output-sensitive Information flow analysis |
| title_fullStr | Output-sensitive Information flow analysis |
| title_full_unstemmed | Output-sensitive Information flow analysis |
| title_short | Output-sensitive Information flow analysis |
| title_sort | output sensitive information flow analysis |
| topic | computer science - cryptography and security computer science - programming languages |
| url | https://lmcs.episciences.org/5779/pdf |
| work_keys_str_mv | AT cristianene outputsensitiveinformationflowanalysis AT laurentmounier outputsensitiveinformationflowanalysis AT marielaurepotet outputsensitiveinformationflowanalysis |