More Web Proxy on the site http://driver.im/

research-article

Composing polymorphic information flow systems with reference immutability

Authors:

Wei HuangAuthors Info & Claims

FTfJP '13: Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs

Article No.: 5, Pages 1 - 7

https://doi.org/10.1145/2489804.2489809

Published: 01 July 2013 Publication History

Abstract

Information flow type systems, such as EnerJ (a type system for energy efficiency), and integrity and confidentiality, are unsound if subtyping for references is allowed because of the presence of mutable references. The standard approach is to disallow subtyping for references, or in other words, replace subtyping constraints with equality constraints. Unfortunately, this often leads to imprecision, causing the type system to reject valid programs.

We observe that subtyping is safe when the left-hand-side of the assignment is immutable. Therefore, we compose information flow systems with reference immutability, which allows for limited subtyping for references. We infer types with the standard approach (i.e., no subtyping for references), and with the composition approach on 13 Java web applications. The composition approach achieves at least 20% precision improvement over the standard approach.

References

[1]

The Checker Framework. http://types.cs.washington.edu/checker-framework/, 2013.

[2]

L. O. Andersen. Program analysis and specialization for the C programming language. PhD thesis, DIKU, University of Copenhagen, 1994.

[3]

A. Banerjee and D. A. Naumann. Secure information flow and pointer confinement in a Java-like language. In CSFW, pages 253--, 2002.

Digital Library

[4]

D. Clarke, J. M. Potter, and J. Noble. Ownership types for flexible alias protection. In OOPSLA, pages 48--64, 1998.

Digital Library

[5]

W. Dietl and P. Müller. Universes: Lightweight ownership for JML. Journal of Object Technology, 4(8):5--32, 2005.

[6]

J. S. Foster, M. Fähndrich, and A. Aiken. A theory of type qualifiers. In PLDI, pages 192--203, May 1999.

Digital Library

[7]

C. Fritz, S. Arzt, S. Rasthofer, E. Bodden, A. Bartel, J. Klein, Y. le Traon, D. Octeau, and P. McDaniel. Highly precise taint analysis for Android applications. EC SPRIDE Technical Report TUD-CS-2013-0113. http://www.bodden.de/pubs/TUD-CS-2013-0113.pdf, 2013.

[8]

D. Greenfieldboyce and J. S. Foster. Type qualifier inference for Java. In OOPSLA, pages 321--336, 2007.

Digital Library

[9]

C. Hammer, J. Krinke, and G. Snelting. Information flow control based on path conditions in dependence graphs. In IEEE ISSSE, pages 87--96, 2006.

[10]

W. Huang and A. Milanova. Inferring AJ Types for Concurrent Libraries. In FOOL, 2012.

[11]

W. Huang, W. Dietl, A. Milanova, and M. D. Ernst. Inference and checking of object ownership. In ECOOP, pages 181--206, 2012.

Digital Library

[12]

W. Huang, A. Milanova, W. Dietl, and M. D. Ernst. ReIm & ReImInfer: Checking and inference of reference immutability and method purity. In OOPSLA, pages 879--896, 2012.

Digital Library

[13]

V. B. Livshits and M. S. Lam. Finding security vulnerabilities in Java applications with static analysis. In USENIX Security, 2005.

Digital Library

[14]

A. C. Myers. JFlow: Practical mostly-static information flow control. In POPL, pages 228--241, 1999.

Digital Library

[15]

A. C. Myers, J. A. Bank, and B. Liskov. Parameterized types for Java. In POPL, pages 132--145, 1997.

Digital Library

[16]

A. Sampson, W. Dietl, and E. Fortuna. EnerJ: Approximate data types for safe and general low-power computation. In PLDI, pages 164--174, 2011.

Digital Library

[17]

U. Shankar, K. Talwar, J. S. Foster, and D. Wagner. Detecting format string vulnerabilities with type qualifiers. In USENIX Security, 2001.

Digital Library

[18]

G. Snelting, T. Robschink, and J. Krinke. Efficient path conditions in dependence graphs for software safety analysis. ACM Trans. Softw. Eng. Methodol., 15(4):410--457, 2006.

Digital Library

[19]

M. Sridharan, S. Artzi, M. Pistoia, S. Guarnieri, O. Tripp, and R. Berg. F4F: Taint Analysis of Framework-based Web Applications. In OOPSLA, pages 1053--1068, 2011.

Digital Library

[20]

B. Steensgaard. Points-to analysis in almost linear time. In POPL, pages 32--41, 1996.

Digital Library

[21]

O. Tripp, M. Pistoia, S. J. Fink, M. Sridharan, and O. Weisman. TAJ: Effective taint analysis of web applications. In PLDI, pages 87--97, 2009.

Digital Library

[22]

O. Tripp, M. Pistoia, P. Cousot, R. Cousot, and S. Guarnieri. ANDROMEDA: accurate and scalable security analysis of web applications. In FASE, pages 210--225, 2013.

Digital Library

[23]

M. S. Tschantz and M. D. Ernst. Javari: Adding reference immutability to Java. In OOPSLA, pages 211--230, 2005.

Digital Library

[24]

M. Vaziri, F. Tip, J. Dolby, C. Hammer, and J. Vitek. A type system for data-centric synchronization. In ECOOP, pages 304--328, 2010.

Digital Library

[25]

D. Volpano, G. Smith, and C. Irvine. A sound type system for secure flow analysis. Journal of Computer Security, pages 167--187, 1996.

Digital Library

[26]

M. Zanioli, P. Ferrara, and A. Cortesi. Sails: static analysis of information leakage with Sample. In SAC, pages 1308--1313, 2012.

Digital Library

Cited By

Runge TServetto MPotanin ASchaefer I(2022)Immutability and Encapsulation for Sound OO Information Flow ControlACM Transactions on Programming Languages and Systems10.1145/357327045:1(1-35)Online publication date: 2-Dec-2022
https://dl.acm.org/doi/10.1145/3573270
Milanova A(2020)FlowCFL: generalized type-based reachability analysis: graph reduction and equivalence of CFL-based and type-based reachabilityProceedings of the ACM on Programming Languages10.1145/34282464:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428246
Dong YMilanova ADolby JZheng YBinder WTůma P(2016)JCryptProceedings of the 13th International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools10.1145/2972206.2972209(1-12)Online publication date: 29-Aug-2016
https://dl.acm.org/doi/10.1145/2972206.2972209
Show More Cited By

Index Terms

Composing polymorphic information flow systems with reference immutability
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
      2. Language types
        Object oriented languages

Recommendations

Uniqueness and reference immutability for safe parallelism
OOPSLA '12

A key challenge for concurrent programming is that side-effects (memory operations) in one thread can affect the behavior of another thread. In this paper, we present a type system to restrict the updates to memory to prevent these unintended side-...
Uniqueness and reference immutability for safe parallelism
OOPSLA '12: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

A key challenge for concurrent programming is that side-effects (memory operations) in one thread can affect the behavior of another thread. In this paper, we present a type system to restrict the updates to memory to prevent these unintended side-...
Inference of Reference Immutability
ECOOP '08: Proceedings of the 22nd European conference on Object-Oriented Programming

Javari is an extension of Java that supports reference immutability constraints. Programmers write readonlytype qualifiers and other constraints, and the Javari typechecker detects mutation errors (incorrect side effects) or verifies their absence. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

FTfJP '13: Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs

July 2013

52 pages

ISBN:9781450320429

DOI:10.1145/2489804

Program Chair:
Werner Dietl
University of Washington

Copyright © 2013 ACM.

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

CNRS: Centre National De La Rechercue Scientifique
UM2: University Montpellier 2
AITO: Association Internationale pour les Technologies Objets

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 July 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

ECOOP '13

Sponsor:

CNRS
UM2
AITO

ECOOP '13: European Conference on Object-Oriented Programming

July 1, 2013

Montpellier, France

Acceptance Rates

FTfJP '13 Paper Acceptance Rate 7 of 14 submissions, 50%;

Overall Acceptance Rate 51 of 75 submissions, 68%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
101
Total Downloads

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

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Runge TServetto MPotanin ASchaefer I(2022)Immutability and Encapsulation for Sound OO Information Flow ControlACM Transactions on Programming Languages and Systems10.1145/357327045:1(1-35)Online publication date: 2-Dec-2022
https://dl.acm.org/doi/10.1145/3573270
Milanova A(2020)FlowCFL: generalized type-based reachability analysis: graph reduction and equivalence of CFL-based and type-based reachabilityProceedings of the ACM on Programming Languages10.1145/34282464:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428246
Dong YMilanova ADolby JZheng YBinder WTůma P(2016)JCryptProceedings of the 13th International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools10.1145/2972206.2972209(1-12)Online publication date: 29-Aug-2016
https://dl.acm.org/doi/10.1145/2972206.2972209
Huang WDong YMilanova ADolby JYoung MXie T(2015)Scalable and precise taint analysis for AndroidProceedings of the 2015 International Symposium on Software Testing and Analysis10.1145/2771783.2771803(106-117)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1145/2771783.2771803
Ernst MJust RMillstein SDietl WPernsteiner SRoesner FKoscher KBarros PBhoraskar RHan SVines PWu EAhn GYung MLi N(2014)Collaborative Verification of Information Flow for a High-Assurance App StoreProceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security10.1145/2660267.2660343(1092-1104)Online publication date: 3-Nov-2014
https://dl.acm.org/doi/10.1145/2660267.2660343
Milanova AHuang WDong YKolodziej JChilders B(2014)CFL-reachability and context-sensitive integrity typesProceedings of the 2014 International Conference on Principles and Practices of Programming on the Java platform: Virtual machines, Languages, and Tools10.1145/2647508.2647522(99-109)Online publication date: 23-Sep-2014
https://dl.acm.org/doi/10.1145/2647508.2647522
Huang WDong YMilanova A(2014)Type-Based Taint Analysis for Java Web ApplicationsProceedings of the 17th International Conference on Fundamental Approaches to Software Engineering - Volume 841110.1007/978-3-642-54804-8_10(140-154)Online publication date: 5-Apr-2014
https://dl.acm.org/doi/10.1007/978-3-642-54804-8_10

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents