A sound analysis for secure information flow using abstract memory graph

Dorina Ghindici 1 Isabelle Simplot-Ryl 1 Jean-Marc Talbot 2
1 POPS - System and Networking for Portable Objects Proved to be Safe
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe, IRCICA
2 LIF - Laboratoire d'informatique Fondamentale de Marseille - UMR 6166
Abstract : In this paper we present a flow-sensitive analysis for secure informa- tion flow for Java bytecode. Our approach consists of computing, at all program points, an abstract memory graph (AMG) which tracks how input values of a method may influence its outputs. This computation subsumes a points-to anal- ysis (reflecting how objects depend on each other) by addressing dependencies arising from data of primitive types and from the control flow of the program. Our graph construction is proved to be sound for both intra-procedural and inter- procedural analysis by establishing a non-interference theorem stating that if an output value is unrelated to an input one in the AMG then the output remains un- changed when the input is modified. In contrast with many type-based informa- tion flow techniques, our approach does not require security levels to be known during the computation of the graph: security aspects of information flow are checked by labeling ”a posteriori” the AMG with security levels.
Type de document :
Communication dans un congrès
Farhad Arbab and Marjan Sirjani. Proc. 3rd IPM International Conference on Fundamentals of Software Engineering, FSEN 2009, Revised Selected papers, 2010, Kish Island, Persian Gulf, Iran, Iran. Springer, 5961, pp.355--370, 2010, Lectures Notes in Computer Science. 〈10.1007/978-3-642-11623-0_21〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00544943
Contributeur : Isabelle Simplot-Ryl <>
Soumis le : jeudi 9 décembre 2010 - 11:44:35
Dernière modification le : vendredi 9 mars 2018 - 11:24:45

Identifiants

Collections

INRIA | UNIV-LILLE3 | UNIV-AMU | LIF | LIS-LAB

Citation

Dorina Ghindici, Isabelle Simplot-Ryl, Jean-Marc Talbot. A sound analysis for secure information flow using abstract memory graph. Farhad Arbab and Marjan Sirjani. Proc. 3rd IPM International Conference on Fundamentals of Software Engineering, FSEN 2009, Revised Selected papers, 2010, Kish Island, Persian Gulf, Iran, Iran. Springer, 5961, pp.355--370, 2010, Lectures Notes in Computer Science. 〈10.1007/978-3-642-11623-0_21〉. 〈inria-00544943〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

86

Contact


archive-ouverte@inria.fr