skip to main content
10.1145/1040294.1040304acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article

Non-interference for a JVM-like language

Published: 10 January 2005 Publication History

Abstract

We define an information flow type system for a sequential JVM-like language that includes classes, objects, and exceptions. Furthermore, we show that it enforces non-interference. Our work provides, to our best knowledge, the first analysis that has been shown to guarantee non-interference for a realistic low level language.

References

[1]
A. Banerjee and D. Naumann. Stack-based access control for secure information flow. Journal of Functional Programming, 200x. Special Issue on Language-Based Security. To appear.]]
[2]
G. Barthe, A. Basu, and T. Rezk. Security types preserving compilation. In B. Steffen and G. Levi, editors, Proceedings of VMCAI'04, volume 2934 of Lecture Notes in Computer Science, pages 2--15. Springer-Verlag, 2004.]]
[3]
C. Bernardeschi and N. De Francesco. Combining Abstract Interpretation and Model Checking for analysing Security Properties of Java Bytecode. In A. Cortesi, editor, Proceedings of VMCAI'02, volume 2294 of Lecture Notes in Computer Science, pages 1--15, 2002.]]
[4]
P. Bieber, J. Cazin, V. Wiels, G. Zanon, P. Girard, and J.-L. Lanet. Checking Secure Interactions of Smart Card Applets: Extended version. Journal of Computer Security, 10:369--398, 2002.]]
[5]
E. Bonelli, A. Compagnoni, and R. Medel. SIFTAL: A Typed Assembly Language for Secure Information Flow Analysis, 2004. Manuscript.]]
[6]
A. Coglio. Simple verification technique for complex Java bytecode subroutines. Concurrency and Computation: Practice and Experience, 16(7):647--670, 2004.]]
[7]
Coq Development Team. The Coq Proof Assistant User's Guide. Versio 8.0, January 2004.]]
[8]
S. N. Freund and J. C. Mitchell. A Type System for the Java Bytecode Language and Verifier. Journal of Automated Reasoning, 30(3-4):271--321, December 2003.]]
[9]
S. Genaim and F. Spoto. Information Flow Analysis for Java Bytecode. In R. Cousot, editor, Proceedings of VMCAI'05, volume 3xxx of Lecture Notes in Computer Science. Springer-Verlag, 2005. To appear.]]
[10]
G. A. Kildall. A unified approach to global program optimization. In Proceedings of POPL'73, pages 194--206. ACM Press, 1973.]]
[11]
X. Leroy. Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning, 30(3-4):235--269, December 2003.]]
[12]
G. Morrisett, D. Walker, K. Crary, and N. Glew. From system F to typed assembly language. In Proceedings of POPL'98, pages 85--97. ACM Press, 1998.]]
[13]
A. C. Myers. Jflow: Practical mostly-static information flow control. In Proceedings of POPL'99, pages 228--241. ACM Press, 1999.]]
[14]
D. Naumann. Machine-checked correctness of a secure information flow analyzer (preliminary report). Technical Report CS-2004-10, Stevens Institute of Technology, March 2003.]]
[15]
F. Pottier and V. Simonet. Information flow inference for ML. ACM Transactions of Programming Languages and Systems, 25(1):117--158, January 2003.]]
[16]
A. Sabelfeld and A. Myers. Language-Based Information-Flow Security. IEEE Journal of Selected Areas in Comunications, 21:5--19, January 2003.]]
[17]
R. Stärk, J. Schmid, and E. Börger. Java and the Java Virtual Machine - Definition, Verification, Validation. Springer-Verlag, 2001.]]
[18]
M. Strecker. Formal analysis of an information flow type system for MicroJava (extended version). Technical report, Technische Universität München, July 2003.]]
[19]
S. Zdancewic and A. Myers. Secure information flow and CPS. In D. Sands, editor, Proceedings of ESOP'01, volume 2028 of Lecture Notes in Computer Science, pages 46--61. Springer-Verlag, 2001.]]
[20]
S. Zwandewic. Challenges in information flow security. In R. Giacobazzi, editor, Informal proceedings of PLID'04, 2004.]]

Cited By

View all
  • (2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
  • (2022)SNITCH: A Platform for Information Flow ControlIntegrated Formal Methods10.1007/978-3-031-07727-2_24(365-368)Online publication date: 1-Jun-2022
  • (2021)A permission-dependent type system for secure information flow analysisJournal of Computer Security10.3233/JCS-20003629:2(161-228)Online publication date: 1-Jan-2021
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
TLDI '05: Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation
January 2005
122 pages
ISBN:1581139993
DOI:10.1145/1040294
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 January 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. confidentiality
  2. low level languages
  3. type systems

Qualifiers

  • Article

Conference

TLDI05
Sponsor:

Acceptance Rates

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)5
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
  • (2022)SNITCH: A Platform for Information Flow ControlIntegrated Formal Methods10.1007/978-3-031-07727-2_24(365-368)Online publication date: 1-Jun-2022
  • (2021)A permission-dependent type system for secure information flow analysisJournal of Computer Security10.3233/JCS-20003629:2(161-228)Online publication date: 1-Jan-2021
  • (2021)Mechanized Type Safety for Gradual Information Flow2021 IEEE Security and Privacy Workshops (SPW)10.1109/SPW53761.2021.00033(194-206)Online publication date: May-2021
  • (2021)Hybrid Information Flow Control for Low-Level CodeSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_9(141-159)Online publication date: 3-Dec-2021
  • (2020)SCFMSPProceedings of the 15th International Conference on Availability, Reliability and Security10.1145/3407023.3407050(1-10)Online publication date: 25-Aug-2020
  • (2018)A Permission-Dependent Type System for Secure Information Flow Analysis2018 IEEE 31st Computer Security Foundations Symposium (CSF)10.1109/CSF.2018.00023(218-232)Online publication date: Jul-2018
  • (2018)Combining Symbolic and Numerical Domains for Information Leakage AnalysisTransactions on Computational Science XXXI10.1007/978-3-662-56499-8_6(98-135)Online publication date: 28-Jan-2018
  • (2016)A Posteriori Taint-Tracking for Demonstrating Non-interference in Expressive Low-Level Languages2016 IEEE Security and Privacy Workshops (SPW)10.1109/SPW.2016.58(179-184)Online publication date: May-2016
  • (2015)GhostRiderACM SIGARCH Computer Architecture News10.1145/2786763.269438543:1(87-101)Online publication date: 14-Mar-2015
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media