Statically checking confidentiality via dynamic labels

ABSTRACT

This paper presents a new approach for verifying confidentiality for programs, based on abstract interpretation. The framework is formally developed and proved correct in the theorem prover PVS. We use dynamic labeling functions to abstractly interpret a simple programming language via modification of security levels of variables. Our approach is sound and compositional and results in an algorithm for statically checking confidentiality.

REFERENCES

• 1: Ádám Darvas, Reiner Hähnle, and Dave Sands. A theorem proving approach to analysis of secure information flow. In Roberto Gorrieri, editor, Workshop on Issues in the Theory of Security, WITS. IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS, 2003.
• 2: Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt. The KeY tool. Software and System Modeling, 2003. To appear.
• 3: Marco Avvenuti , Cinzia Bernardeschi , Nicoletta De Francesco, Java bytecode verification for secure information flow, ACM SIGPLAN Notices, v.38 n.12, December 2003 [doi>10.1145/966051.966055]
• 4: Anindya Banerjee , David A. Naumann, Stack-based access control and secure information flow, Journal of Functional Programming, v.15 n.2, p.131-177, March 2005 [doi>10.1017/S0956796804005453]
• 5: Giles Barthe, Amitabh Basu, and Tamara Rezk. Security Types Preserving Compilation. In VMCAI'04 Proceedings, LNCS. Springer, Berlin, 2004.
• 6: K. J. Biba. Integrity considerations for secure computer systems. Technical Report MTR-3153, MITRE Corp., 1977.
• 7: Zhiqun Chen, Java Card Technology for Smart Cards: Architecture and Programmer's Guide, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 8: David R. Cok and Joseph R. Kiniry. ESC/Java2: Uniting ESC/Java and JML. Technical Report NIII-R0413, Nijmegen Institute for Computer and Information Sciences, 2004. available at http://www.cs.ru.nl/research/reports/info/NIII-R0413.html.
• 9: David R. Cok and Joseph R. Kiniry. ESC/Java2: Uniting ESC/Java and JML. In Proceedings of CASSIS: Construction and Analysis of Safe, Secure and Interoperable Smart devices, LNCS. Springer-Verlag, to appear. See the associated technical rapport {8}.

INDEX TERMS

Keywords:
(Higher Order) theorem proving, abstract interpretation, confidentiality, formal verification, static analysis