research-article

Secure slices of insecure programs

Author:

Salvador CavadiniAuthors Info & Claims

ASIACCS '08: Proceedings of the 2008 ACM symposium on Information, computer and communications security

Pages 112 - 122

https://doi.org/10.1145/1368310.1368329

Published: 18 March 2008 Publication History

Get Access

Abstract

This paper deals with the problem of protect the confidentiality of data manipulated by sequential programs. In this context, secure information flow refers to the guarantee that program executions are free of non authorized flows of secret information into public channels. There are two established means to enforce information flow policies: static analyses, that are performed at compile time and guarantee that all program executions are free of unauthorized flows; and runtime monitoring, that dynamically detects and neutralizes invalid flows for the current run.

Both approaches have their advantages and disadvantages. The main disadvantages of static information flow control (IFC) is, that it does not differentiate between secure and insecure executions of the same program, therefore whole programs are rejected in presence of possible invalid flows. On the contrary, dynamic IFC rejects insecure executions only. This analysis precision comes at the price of the execution overload that imposes the dynamic tracking of information flow.

This work presents secure slicing, a technique that statically transforms probably insecure (interfering) programs into secure (non-interfering) ones. Our approach combines static analysis of information flow and program transformation: if invalid flows are detected, instead of rejecting the whole program, we transform it to eliminate the invalid flows. This way, we alleviate drawbacks of static and dynamic approaches: neither we reject full programs nor we impose run-time overhead. The resulting program can be seen as a secure slice of the source program that can be executed without risk of information leaks.

In this work we also show that secure slices can be computed for programs that intentionally release secret information, and that the technique can be applied to real programming languages such as Java.

References

[1]

Martin Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In M. Ac, editor, POPL '99. Proceedings of the 26th ACM SIGPLAN-SIGACT on Principles of programming languages, January 20--22, 1999, San Antonio, TX, pages 147--160, New York, NY, USA, 1999. ACM Press.

Abstract

References

Cited By

Index Terms

Recommendations

Computational probabilistic noninterference

Information-flow types for homomorphic encryptions

Secure remote user access over insecure networks

Comments

Information

Published In

Sponsors

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Conference

Acceptance Rates

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Get Access

Login options

Full Access

View options

PDF

eReader

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations