Abstract
Hunt and Sands (POPL’06) studied a flow sensitive type (FST) system for multi-level security, parametric in the choice of lattice of security levels. Choosing the powerset of program variables as the security lattice yields a system which was shown to be equivalent to Amtoft and Banerjee’s Hoare-style independence logic (SAS’04). Moreover, using the powerset lattice, it was shown how to derive a principal type from which all other types (for all choices of lattice) can be simply derived.Both of these earlier works gave “algorithmic” formulations of the type system/program logic, but both algorithms are of exponential complexity due to the iterative typing of While loops. Later work by Hunt and Sands (ESOP’08) adapted the FST system to provide an erasure type system which determines whether some input is correctly erased at a designated time. This type system is inherently exponential, requiring a double typing of the erasure-labelled input command. In this paper we start by developing the FST work in two key ways: (1) We specialise the FST system to a form which only derives principal types; the resulting type system has a simple algorithmic reading, yielding principal security types in polynomial time. (2) We show how the FST system can be simply extended to check for various degrees of termination sensitivity (the original FST system is completely termination insensitive, while the erasure type system is fully termination sensitive). We go on to demonstrate the power of these techniques by combining them to develop a type system which is shown to correctly implement erasure typing in polynomial time. Principality is used in an essential way to reduce type derivation size from exponential to linear.
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
Amtoft, T., Banerjee, A.: Information flow analysis in logical form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 100–115. Springer, Heidelberg (2004)
Amtoft, T., Banerjee, A.: A logic for information flow analysis with an application to forward slicing of simple imperative programs. Science of Computer Programming 64(1), 3–28 (2007)
Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: POPL 2006: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 91–102. ACM, New York (2006)
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)
Andrews, G.R., Reitman, R.P.: An axiomatic approach to information flow in programs. TOPLAS 2(1), 56–75 (1980)
Banâtre, J.-P., Bryce, C.: Information flow control in a parallel language framework. In: Proc. IEEE Computer Security Foundations Workshop, pp. 39–52 (June 1993)
Banâtre, J.-P., Bryce, C.: A security proof system for networks of communicating processes. Research Report RR-2042, INRIA (1993)
Banâtre, J.-P., Bryce, C., Le Métayer, D.: Compile-time detection of information flow in sequential programs. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 55–73. Springer, Heidelberg (1994)
Bergeretti, J.-F., Carré, B.: Information-flow and data-flow analysis of while-programs. ACM TOPLAS 7(1), 37–61 (1985)
Boudol, G., Castellani, I.: Noninterference for concurrent programs. In: Yu, Y., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 382–395. Springer, Heidelberg (2001)
Boudol, G.: On typing information flow. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 366–380. Springer, Heidelberg (2005)
Chapman, R., Hilton, A.: Enforcing security and safety models with an information flow analysis tool. Ada Lett. XXIV(4), 39–46 (2004)
Clark, D., Hankin, C., Hunt, S.: Information flow for Algol-like languages. Journal of Computer Languages 28(1), 3–28 (2002)
Chong, S., Myers, A.C.: End-to-end enforcement of erasure and declassification. In: CSF, pp. 98–111. IEEE Computer Society, Los Alamitos (2008)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Comm. of the ACM 20(7), 504–513 (1977)
Deng, Z., Smith, G.: Type inference and informative error reporting for secure information flow. In: ACM-SE 44: Proceedings of the 44th annual Southeast regional conference, pp. 543–548. ACM, New York (2006)
Demange, D., Sands, D.: All Secrets Great and Small. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 207–221. Springer, Heidelberg (2009)
Hammer, C.: Experiences with pdg-based ifc. In: Second International Symposium Engineering Secure Software and Systems, pp. 44–60 (2010)
Horwitz, S., Reps, T.W., Binkley, D.: Interprocedural slicing using dependence graphs. ACM TOPLAS 12(1), 26–60 (1990)
Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL 2006, Proceedings of the 33rd Annual. ACM SIGPLAN - SIGACT. Symposium. on Principles of Programming Languages (January 2006)
Hunt, S., Sands, D.: Just forget it - the semantics and enforcement of information erasure. In: Gairing, M. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 239–253. Springer, Heidelberg (2008)
Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. International Journal of Information Security 8(6), 399–422 (2009)
Moggi, E.: Computational lambda-calculus and monads. In: Proc. IEEE Symp. on Logic in Computer Science, pp. 14–23 (1989)
Prosser, R.T.: Applications of boolean matrices to the analysis of flow diagrams. In: IRE-AIEE-ACM 1959 (Eastern): Papers presented at the December 1-3, 1959, eastern joint IRE-AIEE-ACM computer conference, pp. 133–138. ACM, New York (1959)
Pottier, F., Simonet, V.: Information flow inference for ML. ACM TOPLAS 25(1), 117–158 (2003)
Smith, G.: A new type system for secure information flow. In: Proc. IEEE Computer Security Foundations Workshop, June 2001, pp. 115–125 (2001)
Volpano, D., Smith, G.: A type-based approach to program security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 607–621. Springer, Heidelberg (1997)
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. J. Computer Security 4(3), 167–187 (1996)
Weiser, M.: Program slicing. IEEE Transactions on Software Engineering 10(4), 352–357 (1984)
Wells, J.B.: The essence of principal typings. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 913–925. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hunt, S., Sands, D. (2011). From Exponential to Polynomial-Time Security Typing via Principal Types. In: Barthe, G. (eds) Programming Languages and Systems. ESOP 2011. Lecture Notes in Computer Science, vol 6602. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19718-5_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-19718-5_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19717-8
Online ISBN: 978-3-642-19718-5
eBook Packages: Computer ScienceComputer Science (R0)