Abstract
This paper presents an approach to enforce information flow policies using a three-valued type-based analysis on a core imperative language. Our analysis aims first at reducing false positives generated by static analysis, and second at preparing for instrumentation. False positives arise in the analysis of real computing systems when some information is missing at compile time, for example the name of a file, and consequently, its security level. The key idea of our approach is to distinguish between negative and may responses. Instead of rejecting in the latter cases, we type instructions with an additional type, unknown, indicating uncertainty, possibly preparing for a light instrumentation. During the static analysis step, the may responses are identified and annotated with the unknown security type, while the positive and negative responses are treated as is usually done. This work is done in preparation of a hybrid security enforcement mechanismWe prove that our type system is sound by showing that it satisfies non-interference. The novelty is the handling of three security types, but we also treat variables and channels in a special way. Programs interact via communication channels. Secrecy levels are associated to channels rather than to variables whose security levels change according to the information they store.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Volpano, D., Irvine, C., Smith, G.: A sound type system for secure ow analysis. Journal of Computer Security 4(2-3), 167–187 (1996)
Hunt, S., Sands, D.: On flow-sensitive security types. In: Proceedings of the ACM Symposium on Principles of Programming Languages (January 2006)
Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: Proceedings of the IEEE Computer Security Foundations Symposium (2010)
Denning, D.E.: A lattice model of secure information flow. Communications of the ACM 19, 236–243 (1976)
Smith, G.: Principles of secure information flow analysis. In: Malware Detection, vol. 27, pp. 291–307. Springer (2007)
O’Neill, K.R., Clarkson, M.R., Chong, S.: Information-flow security for interactive programs. In: Proceedings of the IEEE Computer Security Foundations Workshop (July 2006)
Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Informatica 42(4-5), 291–347 (2005)
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)
Denning, D.E., Denning, P.J.: Certi cation of programs for secure information flow. Communications of the ACM 20, 504–513 (1977)
Smith, G.: A new type system for secure information flow. In: Proceedings of the IEEE Workshop on Computer Security Foundations, pp. 115–125 (2001)
Pottier, F., Simonet, V.: Information flow inference for ML. ACM Transactions on Programming Languages and Systems 25, 117–158 (2003)
Myers, A.C.: J ow: Practical mostly-static information flow control. In: Proceedings of the ACM Symposium on Principles of Programming Languages (1999)
Banerjee, A., Naumann, D.A.: Secure information flow and pointer con nement in a java-like language. In: Proceedings of the IEEE Computer Security Foundations Workshop (2002)
Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the IEEE Workshop on Computer Security Foundations (2004)
Terauchi, T., Aiken, A.: Secure Information Flow as a Safety Problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005)
Sabelfeld, A., Sands, D.: A per model of secure information flow in sequential programs. Higher-Order and Symbolic Computation 14(1), 59–91 (2001)
Barthe, G., Prensa Nieto, L.: Secure information flow for a concurrent language with scheduling. Journal of Computer Security 15, 647–689 (2007)
Sabelfeld, A., Sands, D.: Probabilistic noninterference for multi-threaded programs. In: Proceedings of the IEEE Workshop on Computer Security Foundations (2000)
Smith, G.: Probabilistic noninterference through weak probabilistic bisimulation. In: Proceedings of the IEEE Computer Security Foundations Workshop (June-July 2003)
Smith, G.: Improved typings for probabilistic noninterference in a multi-threaded language. Journal of Computer Security 14(6), 591–623 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Desharnais, J., Kanyabwero, E.P., Tawbi, N. (2012). Enforcing Information Flow Policies by a Three-Valued Analysis. In: Kotenko, I., Skormin, V. (eds) Computer Network Security. MMM-ACNS 2012. Lecture Notes in Computer Science, vol 7531. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33704-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-33704-8_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33703-1
Online ISBN: 978-3-642-33704-8
eBook Packages: Computer ScienceComputer Science (R0)