Abstract
The termination insensitive secure information flow problem can be reduced to solving a safety problem via a simple program transformation. Barthe, D’Argenio, and Rezk coined the term “self-composition” to describe this reduction. This paper generalizes the self-compositional approach with a form of information downgrading recently proposed by Li and Zdancewic. We also identify a problem with applying the self-compositional approach in practice, and we present a solution to this problem that makes use of more traditional type-based approaches. The result is a framework that combines the best of both worlds, i.e., better than traditional type-based approaches and better than the self-compositional approach.
This research was supported in part by NASA Grant No. NNA04CI57A; NSF Grant Nos. CCR-0234689, CCR-0085949, and CCR-0326577. The information presented here does not necessarily reflect the position or the policy of the Government and no official endorsement should be inferred.
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
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21, 5–19 (2003)
McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: SP 1994: Proceedings of the 1994 IEEE Symposium on Security and Privacy, Washington, DC, USA, p. 79. IEEE Computer Society, Los Alamitos (1994)
Darvas, Á., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Gorrieri, R. (ed.) Workshop on Issues in the Theory of Security, WITS, IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS (2003)
Barthe, G., D’Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Computer Security Fundation Workshop (CSFW 17). IEEE Press, Los Alamitos (2004)
Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, pp. 1–3 (2002)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, pp. 58–70 (2002)
Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 158–172. Springer, Heidelberg (2002)
Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: Proceedings of the 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Long Beach, California, pp. 132–144 (2005)
Li, P., Zdancewic, S.: Downgrading policies and relaxed noninterference. In: Proceedings of the 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Long Beach, California, pp. 158–170 (2005)
Zdancewic, S., Myers, A.C.: Robust declassification. In: CSFW 2001: Proceedings of the 14th IEEE Workshop on Computer Security Foundations, pp. 15–23. IEEE Computer Society, Los Alamitos (2001)
Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 174–191. Springer, Heidelberg (2004)
Giacobazzi, R., Mastroeni, I.: Abstract non-interference: parameterizing non-interference by abstract interpretation. In: Proceedings of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Venice, Italy, pp. 186–197 (2004)
Terauchi, T., Aiken, A.: Secure information flow as a safety problem. University of California, Berkeley UCB//CSD-05-1396 (Technical report)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Terauchi, T., Aiken, A. (2005). Secure Information Flow as a Safety Problem. In: Hankin, C., Siveroni, I. (eds) Static Analysis. SAS 2005. Lecture Notes in Computer Science, vol 3672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11547662_24
Download citation
DOI: https://doi.org/10.1007/11547662_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28584-7
Online ISBN: 978-3-540-31971-9
eBook Packages: Computer ScienceComputer Science (R0)