article

Instruction-level security typing by abstract interpretation

Authors:

Nicoletta Francesco,

Luca MartiniAuthors Info & Claims

International Journal of Information Security, Volume 6, Issue 2-3

Pages 85 - 106

Published: 01 March 2007 Publication History

Abstract

We present a method based on abstract interpretation to check secure information flow in programs with dynamic structures where input and output channels are associated with security levels. In the concrete operational semantics each value is annotated by a security level dynamically taking into account both the explicit and the implicit information flows. We define a collecting semantics which associates with each program point the set of concrete states of the machine when the point is reached. The abstract domains are obtained from the concrete ones by keeping the security levels and forgetting the actual values. Using this framework, we define an abstract semantics, called instruction-level security typing, that allows us to certify a larger set of programs with respect to the typing approaches to check secure information flow. An efficient implementation is shown, operating a fixpoint iteration similar to that of the Java bytecode verification.

References

[1]

Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A core calculus of dependency. In: 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Proceedings, January 20---22, 1999, San Antonio, pp. 147---160. ACM, New York (1999)

Digital Library

[2]

Amtoft, T., Banerjee, A.: Information flow analysis in logical form. In: Giacobazzi, R. (ed.) SAS 2004 (11th Static Analysis Symposium), Verona, Italy, August 2004, Vol. 3148 of Lecture Notes in Computer Science, pp. 100---115. Springer, Berlin (2004)

[3]

Avvenuti M., Bernardeschi C. and De Francesco N. (2003). Java bytecode verification for secure information flow. ACM SIGPLAN Notices 38(12): 20---27

Digital Library

[4]

Banerjee, A., Naumann, D.: Secure information flow and pointer confinement in a Java-like language. In: 15th IEEE Security Foundations Workshop (CSFW'02) Proceedings. IEEE, 2002

[5]

Barbuti R., Bernardeschi C. and De Francesco N. (2002). Abstract interpretation of operational semantics for secure information flow. Inform. Process. Lett. 83(2): 101---108

Digital Library

[6]

Barbuti, R., Bernardeschi, C., De Francesco N.: Checking security of Java bytecode by abstract interpretation. In: SAC '02: Proceedings of the 2002 ACM symposium on Applied computing, March 10---14, 2002, Madrid, Spain, pp. 229---236. ACM New York (2002)

Digital Library

[7]

Barbuti R., Bernardeschi C. and De Francesco N. (2004). Analyzing information flow properties in assembly code by abstract interpretation. Comput. J. 47(1): 25---45

[8]

Barthe, G., Rezk, T.: Non-interference for a JVM-like language. In: TLDI '05: Proceedings of the 2005 ACM SIGPLAN international workshop on types in languages design and implementation, pp. 103---112, New York, NY, USA, 2005. ACM, New York

Digital Library

[9]

Bernardeschi, C., De Francesco, N.: Combining abstract interpretation and model checking for analysing security properties of Java bytecode. In: Cortesi, A. (ed.) Third International Workshop on Verification, Model Checking and Abstract Interpretation Proceedings, VMCAI 2002, Venice, January 21---22, 2002, Proceedings, Vol. 2294 of Lecture Notes in Computer Science, pp. 1---15. Springer, Berlin (2002)

[10]

Bernardeschi C., De Francesco N. and Lettieri G. (2002). An abstract semantics tool for secure information flow of stack-based assembly programs. Microprocess. Microsyst. 26(8): 391---398

[11]

Bieber, P., Cazin, J., Girard, P., Lanet, J.-L., Wiels, V., Zanon, G.: Checking secure interactions of smart card applets. In: ESORICS 2000 Proceedings (2000)

[12]

Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer'S Guide. Addison-Wesley Longman Publishing, (2000)

[13]

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Proceedings, pp. 238---252, Los Angeles, (1977)

[14]

Cousot P. and Cousot R. (1992). Abstract interpretation frameworks. J. Logic Comput. 2: 511---547

[15]

Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretations. In: ACM (ed) Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '92), Albuquerque, New Mexico, January 1992, pp. 83---94. ACM, New York (1992)

[16]

De Francesco, N., Martini, L.: Abstract interpretation to check secure information flow in programs with input---output security annotations. In: Dimitrakos, T., Martinelli, F., Ryan, P. Y., Schneider, S., (eds) Formal Aspects in Security and Trust: Third International Workshop, FAST 2005, Newcastle upon Tyne, UK, July 18---19, 2005, Revised Selected Papers, Lecture Notes in Computer Science, pp. 63---80. Springer, Berlin (2006)

[17]

De Francesco N., Santone A. and Tesei L. (2003). Abstract interpretation and model checking for checking secure information flow in concurrent systems. Fundam. Inf. 54(2---3): 195---211

[18]

Denning D.E. (1976). A lattice model of secure information flow. Commun. ACM 19(5): 236---243

Digital Library

[19]

Denning D.E. and Denning P.J. (1977). Certification of programs for secure information flow. Commun ACM 20(7): 504---513

Digital Library

[20]

Donnely C. and Stallman R. (1995). Bison, the YACC-compatible parser generator. Free Software Foundation, November

[21]

Giacobazzi, R., Mastroeni, I.: Abstract non-interference: parameterizing non-interference by abstract interpretation. In: Jones, N. D., Leroy, X. (eds.) Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL '04), Venice, Italy, January 14---16, 2004, pp. 186---197, ACM, New York (2004)

[22]

Heintze, N., Riecke, J. G.: The SLam calculus: programming with secrecy and integrity. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 19---21, 1998, San Diego, CA, USA, pp. 365---377. ACM, New York (1998)

[23]

Hunt, S., Sands, D.: On flow-sensitive security types. In: Morrisett, J. G., Jones, S. L. P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11---13, 2006, pp. 79---90. ACM, New York (2006)

[24]

Jacobs, B., Pieters, W., Warnier, M.: Statically checking confidentiality via dynamic labels. In: Workshop on Issues in the Theory of Security proceedings, Long Beach, CA, United States, January 20, 2005. ACM, New York (2005)

Digital Library

[25]

Jones N.D., Nielson F. (1995) Abstract interpretation: a semantic based tool for program analysis. In: Abramsky, S., Gabbay, D.M.,Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, Vol.4, 527---636. Oxford University Press, Oxford (1995)

[26]

Joshi R. and Leino K.M. (2000). A semantic approach to secure information flow. Sci. Comput. Programm. 37(1---3): 113---138

[27]

Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the 1st Annual ACM Symposium on Principles of Programming Languages, Boston, Massachusetts, October 1973, pp. 194---206 (1973)

Digital Library

[28]

Kobayashi, N., Shirane, K.: Type-based information flow analysis for low-level languages. In: Informal Proceedings of the 3rd Asian Workshop on Programming Languages and Systems (APLAS'02) (2002)

[29]

Lampson B.W. (1973). A note on the confinement problem. Commun. ACM 16(10): 613---615

Digital Library

[30]

Leroy X. (2003). Java bytecode verification: algorithms and formalizations. J. Automat. Reason. 30(3---4): 235---269

[31]

Lindholm, T., Yellin, F.: Java Virtual Machine Specification, 2nd edn. Addison-Wesley Longman Publishing (1999)

[32]

Mizuno M. and Schmidt D.A. (1992). A security flow control algorithm and its denotational semantics correctness proof. Formal Aspects Comput. 4: 727---754

[33]

Myers, A.C.: Jflow: practical mostly-static information flow control. In: 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Proceedings, January 20---22, 1999, San Antonio, TX, pp. 228---241. ACM, New York (1999)

Digital Library

[34]

Myers, A.C., Liskov, B.: A decentralized model for information flow control. In: SOSP '97: Proceedings of the sixteenth ACM symposium on Operating systems principles, pp. 129---142. ACM, New York (1997)

Digital Library

[35]

A guide to understanding Discretionary Access Control in trusted systems. Technical Report NCSC-TG-003 Version 1, National Computer Security Center, 1987

[36]

Paxson, V.: Flex, a fast scanner generator, version 2.5, March 1995

[37]

Pottier, F., Conchon, S.: Information flow inference for free. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18---21, 2000, SIGPLAN Notices 35(9), pp. 46---57 (2000)

Digital Library

[38]

Pottier, F., Simonet, V.: Information flow inference for ML. In 29th ACM Symposium on Principles of Programming Languages Proceedings, Portland, January 16---18, 2002, pp. 319---330 (2002)

Digital Library

[39]

Sabelfeld A. and Myers A.C. (2003). Language-based information-flow security. IEEE J. Select. Areas Commun. 21(1): 5---19

Digital Library

[40]

Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 19---21, 1998, San Diego, pp. 1---10. ACM, New York (1998)

[41]

Volpano D., Smith G. and Irvine C. (1996). A sound type system for secure flow analysis. J. Comput. Secur. 4(3): 167---187

Digital Library

[42]

Zanotti, M.: Security typings by abstract interpretation. In: Static Analysis, 9th International Symposium, SAS 2002, Madrid, Spain, September 17---20, 2002, Proceedrings, Vol. 2477 of Lecture Notes in Computer Science, pp. 360---375, Springer, Berlin (2002)

[43]

Zdancewic, S., Myers, A.C.: Secure information flow via linear continuations. Higher Order Symbol. Comput. 15(2---3), 209---234, Kluwer, Dordrecht (2002)

Cited By

Sun CZhai EChen ZMa J(2011)A multi-compositional enforcement on information flow securityProceedings of the 13th international conference on Information and communications security10.5555/2075719.2075757(345-359)Online publication date: 23-Nov-2011
https://dl.acm.org/doi/10.5555/2075719.2075757
Sun CZhai EChen ZMa J(2011)A Multi-compositional Enforcement on Information Flow SecurityInformation and Communications Security10.1007/978-3-642-25243-3_28(345-359)Online publication date: 23-Nov-2011
https://dl.acm.org/doi/10.1007/978-3-642-25243-3_28
Alba-Castro MAlpuente MEscobar S(2009)Abstract certification of global non-interference in rewriting logicProceedings of the 8th international conference on Formal methods for components and objects10.5555/1939101.1939112(105-124)Online publication date: 4-Nov-2009
https://dl.acm.org/doi/10.5555/1939101.1939112

Index Terms

Instruction-level security typing by abstract interpretation

Recommendations

Checking security of Java bytecode by abstract interpretation
SAC '02: Proceedings of the 2002 ACM symposium on Applied computing

We present a method to certify a subset of the Java bytecode, with respect to security. The method is based on abstract interpretation of the operational semantics of the language. We define a concrete small-step enhanced semantics of the language, able ...
Trace-Based Abstract Interpretation of Operational Semantics

We present trace-based abstract interpretation, a unification of several lines of research on applying Cousot-Cousot-style abstract interpretation a.i. to operational semantics definitions (such as flowchart, big-step, and small-step semantics) that ...
Instruction-level security analysis for information flow in stack-based assembly languages

We propose a method to analyze secure information flow in stack-based assembly languages, communicating with the external environment by means of input and output channels. The method computes for each instruction a security level for each memory ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image International Journal of Information Security

International Journal of Information Security Volume 6, Issue 2-3

March 2007

129 pages

ISSN:1615-5262

EISSN:1615-5270

Issue’s Table of Contents

Copyright © Copyright © 2007 Springer-Verlag.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 March 2007

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sun CZhai EChen ZMa J(2011)A multi-compositional enforcement on information flow securityProceedings of the 13th international conference on Information and communications security10.5555/2075719.2075757(345-359)Online publication date: 23-Nov-2011
https://dl.acm.org/doi/10.5555/2075719.2075757
Sun CZhai EChen ZMa J(2011)A Multi-compositional Enforcement on Information Flow SecurityInformation and Communications Security10.1007/978-3-642-25243-3_28(345-359)Online publication date: 23-Nov-2011
https://dl.acm.org/doi/10.1007/978-3-642-25243-3_28
Alba-Castro MAlpuente MEscobar S(2009)Abstract certification of global non-interference in rewriting logicProceedings of the 8th international conference on Formal methods for components and objects10.5555/1939101.1939112(105-124)Online publication date: 4-Nov-2009
https://dl.acm.org/doi/10.5555/1939101.1939112

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents