skip to main content
10.1145/1501434.1501481acmotherconferencesArticle/Chapter ViewAbstractPublication PagespstConference Proceedingsconference-collections
research-article

Embedding verifiable information flow analysis

Published: 30 October 2006 Publication History

Abstract

Pervasive computing is the next generation of computing environments. As a result more and more applications are dynamically deployed on a growing set of small safe devices. Applications delivered by different vendors may share code and data while they may not trust one another. We present an information flow analysis for full Java bytecode adapted for applications dedicated to embedded systems. Existing techniques are not well adapted to this domain and are often too complex. To ease embedded operations and reduce overhead, an external static analysis is performed initially, and the results are embedded as annotations within the code and certified at loading time. In contrast with other analysis techniques, our model supports dynamic class loading. We evaluated our model on a business case study involving an electronic wallet for air miles storage and management from the literature. We obtained the same results as the other papers but under more restrictive conditions related to inherent characteristics of embedded environments.

References

[1]
Aonix Inc. Perc products.
[2]
G. Barthe, A. Basu, and T. Rezk. Security types preserving compilation: (extended abstract). In Verification, Model Checking, and Abstract Interpretation, 5th International Conference, VMCAI 2004, volume 2937 of Lecture Notes in Computer Science, pages 2--15. Springer, 2004.
[3]
G. Barthe, P. D'Argenio, and T. Rezk. Secure Information Flow by Self-Composition. In Computer Security Fundation Workshop (CSFW'17), pages 100--114. IEEE Press, 2004.
[4]
C. Bernardeschi, N. D. Francesco, G. Lettieri, and L. Martini. Checking secure information flow in java bytecode by code transformation and standard bytecode verification. Softw., Pract. Exper., 34(13):1225--1255, 2004.
[5]
P. Bieber, J. Cazin, P. Girard, J.-L. Lanet, V. Wiels, and G. Zanon. Checking secure interactions of smart card applets: extended version. J. Comput. Secur., 10(4):369--398, 2002.
[6]
P. Bieber, J. Cazin, A. E. Marouani, P. Girard, J. L. Lanet, V. Wiels, and G. Zanon. The pacap prototype: A tool for detecting java card illegal flow. In JavaCard '00: Revised Papers from the First International Workshop on Java on Smart Cards: Programming and Security, pages 25--37, London, UK, 2001. Springer-Verlag.
[7]
D. F. C. Brewer and M. J. Nash. The chinese wall security policy. In IEEE Symposium on Security and Privacy, pages 206--214, 1989.
[8]
D. E. Denning. A lattice model of secure information flow. Commun. ACM, 19(5):236--243, 1976.
[9]
D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Commun. ACM, 20(7):504--513, 1977.
[10]
D. Deville and G. Grimaud. Building an 'impossible" verifier on a Java card. In Proc. 2nd USENIX Workshop on Industrial Experiences with Systems Software (WIESS'02), Boston, USA, 2002.
[11]
S. Genaim and F. Spoto. Information Flow Analysis for Java Bytecode. In R. Cousot, editor, Proc. of the Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of LNCS, pages 346--362, Paris, France, January 2005. Springer-Verlag.
[12]
N. Heintze and J. G. Riecke. The slam calculus: programming with secrecy and integrity. In POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 365--377. ACM Press, 1998.
[13]
S. Hunt and D. Sands. On flow-sensitive security types. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, pages 79--90. ACM, 2006.
[14]
Java In The Small. http://www.lifl.fr/RD2P/JITS/.
[15]
N. Kobayashi and K. Shirane. Type-based information flow analysis for low-level languages. Computer Software 20(2), pages 2--21, 2003.
[16]
T. Lengauer and R. E. Tarjan. A fast algorithm for finding dominators in a flowgraph. ACM Trans. Program. Lang. Syst., 1(1):121--141, 1979.
[17]
T. Lindholm and F. Yellin. Java Virtual Machine Specification. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1999.
[18]
A. Myers. Mostly-Static Decentralized Information Flow Control. PhD thesis, Massachusetts Institute of Technology, Cambridge, 1999.
[19]
A. C. Myers. Jflow: practical mostly-static information flow control. In POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 228--241. ACM Press, 1999.
[20]
A. C. Myers and B. Liskov. A decentralized model for information flow control. In SOSP '97: Proceedings of the sixteenth ACM symposium on Operating systems principles, pages 129--142. ACM Press, 1997.
[21]
G. C. Necula. Proof-carrying code. In POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 106--119, New York, NY, USA, 1997. ACM Press.
[22]
E. Rose and K. H. Rose. Lightweight bytecode verification. In Workshop "Formal Underpinnings of the Java Paradigm", OOPSLA'98, 1998.
[23]
A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1), 2003., 21(1), january 2003.
[24]
G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative language. In POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 355--364, 1998.
[25]
STatic Alias aNalyser. http://www.lifl.fr/~ghindici/STAN/
[26]
Sun Microsystem. Connected Limited Device Configuration and K Virtual Machine. http://java.sun.com/products/cldc/
[27]
T. Terauchi and A. Aiken. Secure information flow as a safety problem. In Static Analysis, 12th International Symposium, SAS 2005, volume 3672 of Lecture Notes in Computer Science, pages 352--367. Springer, 2005.
[28]
D. Volpano, C. Irvine, and G. Smith. A sound type system for secure flow analysis. J. Comput. Secur., 4(2--3):167--187, 1996.
[29]
S. Zdancewic. Challenges for information-flow security. PLID'04 The First International Workshop on Programming Language Interference and Dependence, August 25 2004, Verona, Italy, August 2004.

Cited By

View all
  • (2012)Non-interference on UML state-chartsProceedings of the 50th international conference on Objects, Models, Components, Patterns10.1007/978-3-642-30561-0_16(219-235)Online publication date: 29-May-2012
  • (2009)A sound analysis for secure information flow using abstract memory graphsProceedings of the Third IPM international conference on Fundamentals of Software Engineering10.1007/978-3-642-11623-0_21(355-370)Online publication date: 15-Apr-2009
  • (2008)On Practical Information Flow Policies for Java-Enabled Multiapplication Smart CardsProceedings of the 8th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications10.1007/978-3-540-85893-5_3(32-47)Online publication date: 8-Sep-2008
  • Show More Cited By
  1. Embedding verifiable information flow analysis

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image ACM Other conferences
    PST '06: Proceedings of the 2006 International Conference on Privacy, Security and Trust: Bridge the Gap Between PST Technologies and Business Services
    October 2006
    389 pages
    ISBN:1595936041
    DOI:10.1145/1501434
    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]

    In-Cooperation

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 30 October 2006

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. confidentiality
    2. embedded systems
    3. information flow
    4. language-based security
    5. smart objects
    6. static analysis

    Qualifiers

    • Research-article

    Conference

    PST06
    PST06: International Conference on Privacy, Security and Trust
    October 30 - November 1, 2006
    Ontario, Markham, Canada

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)1
    • Downloads (Last 6 weeks)1
    Reflects downloads up to 20 Feb 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2012)Non-interference on UML state-chartsProceedings of the 50th international conference on Objects, Models, Components, Patterns10.1007/978-3-642-30561-0_16(219-235)Online publication date: 29-May-2012
    • (2009)A sound analysis for secure information flow using abstract memory graphsProceedings of the Third IPM international conference on Fundamentals of Software Engineering10.1007/978-3-642-11623-0_21(355-370)Online publication date: 15-Apr-2009
    • (2008)On Practical Information Flow Policies for Java-Enabled Multiapplication Smart CardsProceedings of the 8th IFIP WG 8.8/11.2 international conference on Smart Card Research and Advanced Applications10.1007/978-3-540-85893-5_3(32-47)Online publication date: 8-Sep-2008
    • (2007)An information flow verifier for small embedded systemsProceedings of the 1st IFIP TC6 /WG8.8 /WG11.2 international conference on Information security theory and practices: smart cards, mobile and ubiquitous computing systems10.5555/1763190.1763212(189-201)Online publication date: 9-May-2007
    • (2007)An Information Flow Verifier for Small Embedded SystemsInformation Security Theory and Practices. Smart Cards, Mobile and Ubiquitous Computing Systems10.1007/978-3-540-72354-7_16(189-201)Online publication date: 2007
    • (2006)Integrated Security Verification and Validation: Case StudyProceedings. 2006 31st IEEE Conference on Local Computer Networks10.1109/LCN.2006.322215(1000-1007)Online publication date: Nov-2006

    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