Abstract
Novel approaches for dynamic information flow monitoring are promising since they enable permissive (accepting a large subset of executions) yet sound (rejecting all unsecure executions) enforcement of non-interference. In this paper, we present a dynamic information flow monitor for a language supporting pointers. Our flow-sensitive monitor relies on prior static analysis in order to soundly enforce non-interference. We also propose a program transformation that preserves the behavior of initial programs and soundly inlines our security monitor. This program transformation enables both dynamic and static verification of non-interference.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Denning, D., Denning, P.: Certification of Programs for Secure Information Flow. Communications of the ACM 20(7), 504–513 (1977)
Goguen, J., Meseguer, J.: Security Policies and Security Models. In: IEEE Symposium on Research in Security and Privacy (1982)
Volpano, D., Irvine, C., Smith, G.: A Sound Type System for Secure Flow Analysis. Journal in Computer Security 4(2-3), 167–187 (1996)
Askarov, A., Hunt, S., Sabelfeld, A., Sands, D.: Termination-Insensitive Noninterference Leaks More Than Just a Bit. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 333–348. Springer, Heidelberg (2008)
Russo, A., Sabelfeld, A.: Dynamic vs. Static Flow-Sensitive Security Analysis. In: Computer Security Foundations Symposium, pp. 186–199. IEEE (2010)
Hunt, S., Sands, D.: On Flow-Sensitive Security Types. In: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol. 41, pp. 79–90. ACM (2006)
Le Guernic, G., Banerjee, A., Jensen, T., Schmidt, D.A.: Automata-Based Confidentiality Monitoring. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 75–89. Springer, Heidelberg (2008)
Blazy, S., Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language. Journal of Automated Reasoning 43(3), 263–288 (2009)
Leroy, X.: Formal Verification of a Realistic Compiler. Communications of the ACM 52(7), 107–115 (2009)
Sabelfeld, A., Myers, A.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003)
Austin, T., Flanagan, C.: Efficient Purely-Dynamic Information Flow Analysis. ACM Sigplan Notices 44(8), 20–31 (2009)
Assaf, M., Signoles, J., Tronel, F., Totel, E.: Program Transformation for Non-interference Verification on Programs with Pointers. Research report RR-8284, INRIA (April 2013), http://hal.inria.fr/hal-00814671
Chandra, D., Franz, M.: Fine-Grained Information Flow Analysis and Enforcement in a Java Virtual Machine. In: Twenty-Third Annual Computer Security Applications Conference, ACSAC 2007, pp. 463–475. IEEE (2007)
Ligatti, J., Bauer, L., Walker, D.: Edit Automata: Enforcement Mechanisms for Run-time Security Policies. International Journal of Information Security 4(1), 2–16 (2005)
Moore, S., Chong, S.: Static Analysis for Efficient Hybrid Information-Flow Control. In: 2011 IEEE 24th Computer Security Foundations Symposium (CSF), pp. 146–160. IEEE (2011)
Austin, T.H., Flanagan, C.: Permissive Dynamic Information Flow Analysis. In: PLAS 2010: Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, pp. 1–12. ACM (2010)
Chudnov, A., Naumann, D.: Information Flow Monitor Inlining. In: 2010 23rd IEEE Computer Security Foundations Symposium (CSF), pp. 200–214. IEEE (2010)
Magazinius, J., Russo, A., Sabelfeld, A.: On-the-fly Inlining of Dynamic Security Monitors. Computers & Security (2011)
Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A Program Analysis Perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012)
Cuoq, P., Prevosto, V., Yakobowski, B.: Frama-C’s Value Analysis Plug-in (September 2012), http://frama-c.com/download/frama-c-value-analysis.pdf
Baudin, P., Filliâtre, J.C., Hubert, T., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language (September 2012), http://frama-c.cea.fr/acsl.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Assaf, M., Signoles, J., Tronel, F., Totel, É. (2013). Program Transformation for Non-interference Verification on Programs with Pointers. In: Janczewski, L.J., Wolfe, H.B., Shenoi, S. (eds) Security and Privacy Protection in Information Processing Systems. SEC 2013. IFIP Advances in Information and Communication Technology, vol 405. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39218-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-39218-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39217-7
Online ISBN: 978-3-642-39218-4
eBook Packages: Computer ScienceComputer Science (R0)