An Accurate Type System for Information Flow in Presence of Arrays
International audience Secure information flow analysis aims to check that the execution of a program does not reveal information about secret data manipulated by this program. In this paper, we consider programs dealing with arrays; unlike most of existing works, we will not assume that arrays are...
Main Authors: | , |
---|---|
Other Authors: | , , , , , |
Format: | Conference Object |
Language: | English |
Published: |
HAL CCSD
2011
|
Subjects: | |
Online Access: | https://inria.hal.science/hal-01583316 https://inria.hal.science/hal-01583316/document https://inria.hal.science/hal-01583316/file/978-3-642-21461-5_10_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_10 |
id |
ftccsdartic:oai:HAL:hal-01583316v1 |
---|---|
record_format |
openpolar |
spelling |
ftccsdartic:oai:HAL:hal-01583316v1 2023-12-17T10:32:08+01:00 An Accurate Type System for Information Flow in Presence of Arrays Fratani, Séverine Talbot, Jean-Marc Laboratoire d'informatique Fondamentale de Marseille - UMR 6166 (LIF) Université de la Méditerranée - Aix-Marseille 2-Université de Provence - Aix-Marseille 1-Centre National de la Recherche Scientifique (CNRS) Roberto Bruni Juergen Dingel TC 6 WG 6.1 Reykjavik,, Iceland 2011-06-06 https://inria.hal.science/hal-01583316 https://inria.hal.science/hal-01583316/document https://inria.hal.science/hal-01583316/file/978-3-642-21461-5_10_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_10 en eng HAL CCSD Springer info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_10 hal-01583316 https://inria.hal.science/hal-01583316 https://inria.hal.science/hal-01583316/document https://inria.hal.science/hal-01583316/file/978-3-642-21461-5_10_Chapter.pdf doi:10.1007/978-3-642-21461-5_10 http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://inria.hal.science/hal-01583316 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. pp.153-167, ⟨10.1007/978-3-642-21461-5_10⟩ [INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] info:eu-repo/semantics/conferenceObject Conference papers 2011 ftccsdartic https://doi.org/10.1007/978-3-642-21461-5_10 2023-11-19T01:31:25Z International audience Secure information flow analysis aims to check that the execution of a program does not reveal information about secret data manipulated by this program. In this paper, we consider programs dealing with arrays; unlike most of existing works, we will not assume that arrays are homogeneous in terms of security levels. Some part of an array can be declared as secret whereas another part is public. Based on a pre-computed approximation of integer variables (serving as indices for arrays), we devise a type system such that typed programs do not leak unauthorized information. Soundness of our type system is proved by a non-interference theorem. Conference Object Iceland Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) 153 167 |
institution |
Open Polar |
collection |
Archive ouverte HAL (Hyper Article en Ligne, CCSD - Centre pour la Communication Scientifique Directe) |
op_collection_id |
ftccsdartic |
language |
English |
topic |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
spellingShingle |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] Fratani, Séverine Talbot, Jean-Marc An Accurate Type System for Information Flow in Presence of Arrays |
topic_facet |
[INFO]Computer Science [cs] [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI] |
description |
International audience Secure information flow analysis aims to check that the execution of a program does not reveal information about secret data manipulated by this program. In this paper, we consider programs dealing with arrays; unlike most of existing works, we will not assume that arrays are homogeneous in terms of security levels. Some part of an array can be declared as secret whereas another part is public. Based on a pre-computed approximation of integer variables (serving as indices for arrays), we devise a type system such that typed programs do not leak unauthorized information. Soundness of our type system is proved by a non-interference theorem. |
author2 |
Laboratoire d'informatique Fondamentale de Marseille - UMR 6166 (LIF) Université de la Méditerranée - Aix-Marseille 2-Université de Provence - Aix-Marseille 1-Centre National de la Recherche Scientifique (CNRS) Roberto Bruni Juergen Dingel TC 6 WG 6.1 |
format |
Conference Object |
author |
Fratani, Séverine Talbot, Jean-Marc |
author_facet |
Fratani, Séverine Talbot, Jean-Marc |
author_sort |
Fratani, Séverine |
title |
An Accurate Type System for Information Flow in Presence of Arrays |
title_short |
An Accurate Type System for Information Flow in Presence of Arrays |
title_full |
An Accurate Type System for Information Flow in Presence of Arrays |
title_fullStr |
An Accurate Type System for Information Flow in Presence of Arrays |
title_full_unstemmed |
An Accurate Type System for Information Flow in Presence of Arrays |
title_sort |
accurate type system for information flow in presence of arrays |
publisher |
HAL CCSD |
publishDate |
2011 |
url |
https://inria.hal.science/hal-01583316 https://inria.hal.science/hal-01583316/document https://inria.hal.science/hal-01583316/file/978-3-642-21461-5_10_Chapter.pdf https://doi.org/10.1007/978-3-642-21461-5_10 |
op_coverage |
Reykjavik,, Iceland |
genre |
Iceland |
genre_facet |
Iceland |
op_source |
Lecture Notes in Computer Science 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE) https://inria.hal.science/hal-01583316 13th Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 31th International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Jun 2011, Reykjavik,, Iceland. pp.153-167, ⟨10.1007/978-3-642-21461-5_10⟩ |
op_relation |
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-21461-5_10 hal-01583316 https://inria.hal.science/hal-01583316 https://inria.hal.science/hal-01583316/document https://inria.hal.science/hal-01583316/file/978-3-642-21461-5_10_Chapter.pdf doi:10.1007/978-3-642-21461-5_10 |
op_rights |
http://creativecommons.org/licenses/by/ info:eu-repo/semantics/OpenAccess |
op_doi |
https://doi.org/10.1007/978-3-642-21461-5_10 |
container_start_page |
153 |
op_container_end_page |
167 |
_version_ |
1785585656259411968 |